Theorem dprd2da 18441

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)

Hypotheses

Ref	Expression
dprd2d.1	|- ( ph -> Rel A )
dprd2d.2	|- ( ph -> S : A --> (SubGrp ` G ) )
dprd2d.3	|- ( ph -> dom A C_ I )
dprd2d.4	|- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
dprd2d.5	|- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
dprd2d.k	|- K = (mrCls ` (SubGrp ` G ) )

Assertion

Ref	Expression
dprd2da	|- ( ph -> G dom DProd S )

Distinct variable groups:   i, j, A   i, G, j   i, I   i, K   ph, i, j   S, i, j

Allowed substitution hints:   I( j)   K( j)

Proof of Theorem dprd2da

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. 2 |- (Cntz ` G ) = (Cntz ` G )
2		eqid 2622	. 2 |- ( 0g ` G ) = ( 0g ` G )
3		dprd2d.k	. 2 |- K = (mrCls ` (SubGrp ` G ) )
4		dprd2d.5	. . 3 |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
5		dprdgrp 18404	. . 3 |- ( G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> G e. Grp )
6	4, 5	syl 17	. 2 |- ( ph -> G e. Grp )
7		resiun2 5418	. . . . 5 |- ( A |` U_ i e. I { i } ) = U_ i e. I ( A |` { i } )
8		iunid 4575	. . . . . 6 |- U_ i e. I { i } = I
9	8	reseq2i 5393	. . . . 5 |- ( A |` U_ i e. I { i } ) = ( A |` I )
10	7, 9	eqtr3i 2646	. . . 4 |- U_ i e. I ( A |` { i } ) = ( A |` I )
11		dprd2d.1	. . . . 5 |- ( ph -> Rel A )
12		dprd2d.3	. . . . 5 |- ( ph -> dom A C_ I )
13		relssres 5437	. . . . 5 |- ( ( Rel A /\ dom A C_ I ) -> ( A |` I ) = A )
14	11, 12, 13	syl2anc 693	. . . 4 |- ( ph -> ( A |` I ) = A )
15	10, 14	syl5eq 2668	. . 3 |- ( ph -> U_ i e. I ( A |` { i } ) = A )
16		ovex 6678	. . . . . 6 |- ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) e. _V
17		eqid 2622	. . . . . 6 |- ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) )
18	16, 17	dmmpti 6023	. . . . 5 |- dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I
19		reldmdprd 18396	. . . . . . 7 |- Rel dom DProd
20	19	brrelex2i 5159	. . . . . 6 |- ( G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) e. _V )
21		dmexg 7097	. . . . . 6 |- ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) e. _V -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) e. _V )
22	4, 20, 21	3syl 18	. . . . 5 |- ( ph -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) e. _V )
23	18, 22	syl5eqelr 2706	. . . 4 |- ( ph -> I e. _V )
24		ressn 5671	. . . . . 6 |- ( A |` { i } ) = ( { i } X. ( A " { i } ) )
25		snex 4908	. . . . . . 7 |- { i } e. _V
26		ovex 6678	. . . . . . . . 9 |- ( i S j ) e. _V
27		eqid 2622	. . . . . . . . 9 |- ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { i } ) |-> ( i S j ) )
28	26, 27	dmmpti 6023	. . . . . . . 8 |- dom ( j e. ( A " { i } ) |-> ( i S j ) ) = ( A " { i } )
29		dprd2d.4	. . . . . . . . 9 |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
30	19	brrelex2i 5159	. . . . . . . . 9 |- ( G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
31		dmexg 7097	. . . . . . . . 9 |- ( ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V -> dom ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
32	29, 30, 31	3syl 18	. . . . . . . 8 |- ( ( ph /\ i e. I ) -> dom ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
33	28, 32	syl5eqelr 2706	. . . . . . 7 |- ( ( ph /\ i e. I ) -> ( A " { i } ) e. _V )
34		xpexg 6960	. . . . . . 7 |- ( ( { i } e. _V /\ ( A " { i } ) e. _V ) -> ( { i } X. ( A " { i } ) ) e. _V )
35	25, 33, 34	sylancr 695	. . . . . 6 |- ( ( ph /\ i e. I ) -> ( { i } X. ( A " { i } ) ) e. _V )
36	24, 35	syl5eqel 2705	. . . . 5 |- ( ( ph /\ i e. I ) -> ( A |` { i } ) e. _V )
37	36	ralrimiva 2966	. . . 4 |- ( ph -> A. i e. I ( A |` { i } ) e. _V )
38		iunexg 7143	. . . 4 |- ( ( I e. _V /\ A. i e. I ( A |` { i } ) e. _V ) -> U_ i e. I ( A |` { i } ) e. _V )
39	23, 37, 38	syl2anc 693	. . 3 |- ( ph -> U_ i e. I ( A |` { i } ) e. _V )
40	15, 39	eqeltrrd 2702	. 2 |- ( ph -> A e. _V )
41		dprd2d.2	. 2 |- ( ph -> S : A --> (SubGrp ` G ) )
42	12	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> dom A C_ I )
43		1stdm 7215	. . . . . . . . . 10 |- ( ( Rel A /\ x e. A ) -> ( 1st ` x ) e. dom A )
44	11, 43	sylan 488	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 1st ` x ) e. dom A )
45	42, 44	sseldd 3604	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( 1st ` x ) e. I )
46	29	ralrimiva 2966	. . . . . . . . 9 |- ( ph -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
47	46	adantr 481	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
48		sneq 4187	. . . . . . . . . . . 12 |- ( i = ( 1st ` x ) -> { i } = { ( 1st ` x ) } )
49	48	imaeq2d 5466	. . . . . . . . . . 11 |- ( i = ( 1st ` x ) -> ( A " { i } ) = ( A " { ( 1st ` x ) } ) )
50		oveq1 6657	. . . . . . . . . . 11 |- ( i = ( 1st ` x ) -> ( i S j ) = ( ( 1st ` x ) S j ) )
51	49, 50	mpteq12dv 4733	. . . . . . . . . 10 |- ( i = ( 1st ` x ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
52	51	breq2d 4665	. . . . . . . . 9 |- ( i = ( 1st ` x ) -> ( G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) <-> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
53	52	rspcv 3305	. . . . . . . 8 |- ( ( 1st ` x ) e. I -> ( A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
54	45, 47, 53	sylc 65	. . . . . . 7 |- ( ( ph /\ x e. A ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
55	54	3ad2antr1 1226	. . . . . 6 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
56	55	adantr 481	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
57		ovex 6678	. . . . . . 7 |- ( ( 1st ` x ) S j ) e. _V
58		eqid 2622	. . . . . . 7 |- ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) )
59	57, 58	dmmpti 6023	. . . . . 6 |- dom ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( A " { ( 1st ` x ) } )
60	59	a1i 11	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> dom ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( A " { ( 1st ` x ) } ) )
61		1st2nd 7214	. . . . . . . . . . 11 |- ( ( Rel A /\ x e. A ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
62	11, 61	sylan 488	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
63		simpr 477	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> x e. A )
64	62, 63	eqeltrrd 2702	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. A )
65		df-br 4654	. . . . . . . . 9 |- ( ( 1st ` x ) A ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. A )
66	64, 65	sylibr 224	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( 1st ` x ) A ( 2nd ` x ) )
67	11	adantr 481	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> Rel A )
68		elrelimasn 5489	. . . . . . . . 9 |- ( Rel A -> ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A ( 2nd ` x ) ) )
69	67, 68	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A ( 2nd ` x ) ) )
70	66, 69	mpbird 247	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
71	70	3ad2antr1 1226	. . . . . 6 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
72	71	adantr 481	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
73	11	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> Rel A )
74		simpr2 1068	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> y e. A )
75		1st2nd 7214	. . . . . . . . . . 11 |- ( ( Rel A /\ y e. A ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
76	73, 74, 75	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
77	76, 74	eqeltrrd 2702	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. A )
78		df-br 4654	. . . . . . . . 9 |- ( ( 1st ` y ) A ( 2nd ` y ) <-> <. ( 1st ` y ) , ( 2nd ` y ) >. e. A )
79	77, 78	sylibr 224	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) A ( 2nd ` y ) )
80		elrelimasn 5489	. . . . . . . . 9 |- ( Rel A -> ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) <-> ( 1st ` y ) A ( 2nd ` y ) ) )
81	73, 80	syl 17	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) <-> ( 1st ` y ) A ( 2nd ` y ) ) )
82	79, 81	mpbird 247	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) )
83	82	adantr 481	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) )
84		simpr 477	. . . . . . . 8 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 1st ` x ) = ( 1st ` y ) )
85	84	sneqd 4189	. . . . . . 7 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> { ( 1st ` x ) } = { ( 1st ` y ) } )
86	85	imaeq2d 5466	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( A " { ( 1st ` x ) } ) = ( A " { ( 1st ` y ) } ) )
87	83, 86	eleqtrrd 2704	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
88		simplr3 1105	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> x =/= y )
89		simpr1 1067	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> x e. A )
90	73, 89, 61	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
91	90, 76	eqeq12d 2637	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( x = y <-> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
92		fvex 6201	. . . . . . . . . 10 |- ( 1st ` x ) e. _V
93		fvex 6201	. . . . . . . . . 10 |- ( 2nd ` x ) e. _V
94	92, 93	opth 4945	. . . . . . . . 9 |- ( <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
95	91, 94	syl6bb 276	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( x = y <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) ) )
96	95	baibd 948	. . . . . . 7 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( x = y <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
97	96	necon3bid 2838	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( x =/= y <-> ( 2nd ` x ) =/= ( 2nd ` y ) ) )
98	88, 97	mpbid 222	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` x ) =/= ( 2nd ` y ) )
99	56, 60, 72, 87, 98, 1	dprdcntz 18407	. . . 4 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) C_ ( (Cntz ` G ) ` ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` y ) ) ) )
100		df-ov 6653	. . . . . 6 |- ( ( 1st ` x ) S ( 2nd ` x ) ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
101		oveq2 6658	. . . . . . . 8 |- ( j = ( 2nd ` x ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
102	101, 58, 57	fvmpt3i 6287	. . . . . . 7 |- ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
103	71, 102	syl 17	. . . . . 6 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
104	90	fveq2d 6195	. . . . . 6 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` x ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
105	100, 103, 104	3eqtr4a 2682	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) )
106	105	adantr 481	. . . 4 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) )
107	84	oveq1d 6665	. . . . . . . 8 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` y ) S j ) )
108	86, 107	mpteq12dv 4733	. . . . . . 7 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) )
109	108	fveq1d 6193	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` y ) ) = ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) )
110		df-ov 6653	. . . . . . . 8 |- ( ( 1st ` y ) S ( 2nd ` y ) ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. )
111		oveq2 6658	. . . . . . . . . 10 |- ( j = ( 2nd ` y ) -> ( ( 1st ` y ) S j ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
112		eqid 2622	. . . . . . . . . 10 |- ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) )
113		ovex 6678	. . . . . . . . . 10 |- ( ( 1st ` y ) S j ) e. _V
114	111, 112, 113	fvmpt3i 6287	. . . . . . . . 9 |- ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
115	82, 114	syl 17	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
116	76	fveq2d 6195	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` y ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
117	110, 115, 116	3eqtr4a 2682	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( S ` y ) )
118	117	adantr 481	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( S ` y ) )
119	109, 118	eqtrd 2656	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` y ) ) = ( S ` y ) )
120	119	fveq2d 6195	. . . 4 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( (Cntz ` G ) ` ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` y ) ) ) = ( (Cntz ` G ) ` ( S ` y ) ) )
121	99, 106, 120	3sstr3d 3647	. . 3 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( S ` x ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
122	11, 41, 12, 29, 4, 3	dprd2dlem2 18439	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
123	51	oveq2d 6666	. . . . . . . . 9 |- ( i = ( 1st ` x ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
124	123, 17, 16	fvmpt3i 6287	. . . . . . . 8 |- ( ( 1st ` x ) e. I -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
125	45, 124	syl 17	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
126	122, 125	sseqtr4d 3642	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) )
127	126	3ad2antr1 1226	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` x ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) )
128	127	adantr 481	. . . 4 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( S ` x ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) )
129	4	ad2antrr 762	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
130	18	a1i 11	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I )
131	45	3ad2antr1 1226	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` x ) e. I )
132	131	adantr 481	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) e. I )
133	12	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> dom A C_ I )
134		1stdm 7215	. . . . . . . . 9 |- ( ( Rel A /\ y e. A ) -> ( 1st ` y ) e. dom A )
135	73, 74, 134	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) e. dom A )
136	133, 135	sseldd 3604	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) e. I )
137	136	adantr 481	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` y ) e. I )
138		simpr 477	. . . . . 6 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) =/= ( 1st ` y ) )
139	129, 130, 132, 137, 138, 1	dprdcntz 18407	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) C_ ( (Cntz ` G ) ` ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) ) )
140		sneq 4187	. . . . . . . . . . . . 13 |- ( i = ( 1st ` y ) -> { i } = { ( 1st ` y ) } )
141	140	imaeq2d 5466	. . . . . . . . . . . 12 |- ( i = ( 1st ` y ) -> ( A " { i } ) = ( A " { ( 1st ` y ) } ) )
142		oveq1 6657	. . . . . . . . . . . 12 |- ( i = ( 1st ` y ) -> ( i S j ) = ( ( 1st ` y ) S j ) )
143	141, 142	mpteq12dv 4733	. . . . . . . . . . 11 |- ( i = ( 1st ` y ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) )
144	143	oveq2d 6666	. . . . . . . . . 10 |- ( i = ( 1st ` y ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) = ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
145	144, 17, 16	fvmpt3i 6287	. . . . . . . . 9 |- ( ( 1st ` y ) e. I -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) = ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
146	136, 145	syl 17	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) = ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
147	146	fveq2d 6195	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( (Cntz ` G ) ` ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) ) = ( (Cntz ` G ) ` ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) ) )
148		eqid 2622	. . . . . . . . 9 |- ( Base ` G ) = ( Base ` G )
149	148	dprdssv 18415	. . . . . . . 8 |- ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) C_ ( Base ` G )
150	46	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
151	143	breq2d 4665	. . . . . . . . . . . 12 |- ( i = ( 1st ` y ) -> ( G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) <-> G dom DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
152	151	rspcv 3305	. . . . . . . . . . 11 |- ( ( 1st ` y ) e. I -> ( A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) -> G dom DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
153	136, 150, 152	sylc 65	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> G dom DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) )
154	113, 112	dmmpti 6023	. . . . . . . . . . 11 |- dom ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( A " { ( 1st ` y ) } )
155	154	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> dom ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( A " { ( 1st ` y ) } ) )
156	153, 155, 82	dprdub 18424	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
157	117, 156	eqsstr3d 3640	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` y ) C_ ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
158	148, 1	cntz2ss 17765	. . . . . . . 8 |- ( ( ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) C_ ( Base ` G ) /\ ( S ` y ) C_ ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) ) -> ( (Cntz ` G ) ` ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
159	149, 157, 158	sylancr 695	. . . . . . 7 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( (Cntz ` G ) ` ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
160	147, 159	eqsstrd 3639	. . . . . 6 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( (Cntz ` G ) ` ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
161	160	adantr 481	. . . . 5 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( (Cntz ` G ) ` ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` y ) ) ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
162	139, 161	sstrd 3613	. . . 4 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
163	128, 162	sstrd 3613	. . 3 |- ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( S ` x ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
164	121, 163	pm2.61dane 2881	. 2 |- ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` x ) C_ ( (Cntz ` G ) ` ( S ` y ) ) )
165	6	adantr 481	. . . . . 6 |- ( ( ph /\ x e. A ) -> G e. Grp )
166	148	subgacs 17629	. . . . . 6 |- ( G e. Grp -> (SubGrp ` G ) e. (ACS ` ( Base ` G ) ) )
167		acsmre 16313	. . . . . 6 |- ( (SubGrp ` G ) e. (ACS ` ( Base ` G ) ) -> (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) )
168	165, 166, 167	3syl 18	. . . . 5 |- ( ( ph /\ x e. A ) -> (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) )
169	14	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( A |` I ) = A )
170		undif2 4044	. . . . . . . . . . . . . . . . . 18 |- ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) = ( { ( 1st ` x ) } u. I )
171	45	snssd 4340	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> { ( 1st ` x ) } C_ I )
172		ssequn1 3783	. . . . . . . . . . . . . . . . . . 19 |- ( { ( 1st ` x ) } C_ I <-> ( { ( 1st ` x ) } u. I ) = I )
173	171, 172	sylib 208	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } u. I ) = I )
174	170, 173	syl5req 2669	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A ) -> I = ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) )
175	174	reseq2d 5396	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> ( A |` I ) = ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) )
176	169, 175	eqtr3d 2658	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A ) -> A = ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) )
177		resundi 5410	. . . . . . . . . . . . . . 15 |- ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) = ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) )
178	176, 177	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> A = ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
179	178	difeq1d 3727	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) \ { x } ) )
180		difundir 3880	. . . . . . . . . . . . 13 |- ( ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
181	179, 180	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) ) )
182		neirr 2803	. . . . . . . . . . . . . . . . 17 |- -. ( 1st ` x ) =/= ( 1st ` x )
183	62	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. A ) -> ( x e. ( A |` ( I \ { ( 1st ` x ) } ) ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
184		df-br 4654	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
185	93	brres 5402	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) <-> ( ( 1st ` x ) A ( 2nd ` x ) /\ ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) ) )
186	185	simprbi 480	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) -> ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) )
187		eldifsni 4320	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) -> ( 1st ` x ) =/= ( 1st ` x ) )
188	186, 187	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) -> ( 1st ` x ) =/= ( 1st ` x ) )
189	184, 188	sylbir 225	. . . . . . . . . . . . . . . . . 18 |- ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) -> ( 1st ` x ) =/= ( 1st ` x ) )
190	183, 189	syl6bi 243	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A ) -> ( x e. ( A |` ( I \ { ( 1st ` x ) } ) ) -> ( 1st ` x ) =/= ( 1st ` x ) ) )
191	182, 190	mtoi 190	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> -. x e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
192		disjsn 4246	. . . . . . . . . . . . . . . 16 |- ( ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) <-> -. x e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
193	191, 192	sylibr 224	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A ) -> ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) )
194		disj3 4021	. . . . . . . . . . . . . . 15 |- ( ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) <-> ( A |` ( I \ { ( 1st ` x ) } ) ) = ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
195	193, 194	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> ( A |` ( I \ { ( 1st ` x ) } ) ) = ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
196	195	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) = ( A |` ( I \ { ( 1st ` x ) } ) ) )
197	196	uneq2d 3767	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
198	181, 197	eqtrd 2656	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
199	198	imaeq2d 5466	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) = ( S " ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
200		imaundi 5545	. . . . . . . . . 10 |- ( S " ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
201	199, 200	syl6eq 2672	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) = ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
202	201	unieqd 4446	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) = U. ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
203		uniun 4456	. . . . . . . 8 |- U. ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
204	202, 203	syl6eq 2672	. . . . . . 7 |- ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) = ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
205		imassrn 5477	. . . . . . . . . . 11 |- ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ran S
206		frn 6053	. . . . . . . . . . . . . 14 |- ( S : A --> (SubGrp ` G ) -> ran S C_ (SubGrp ` G ) )
207	41, 206	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ran S C_ (SubGrp ` G ) )
208	207	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ran S C_ (SubGrp ` G ) )
209		mresspw 16252	. . . . . . . . . . . . 13 |- ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) -> (SubGrp ` G ) C_ ~P ( Base ` G ) )
210	168, 209	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> (SubGrp ` G ) C_ ~P ( Base ` G ) )
211	208, 210	sstrd 3613	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ran S C_ ~P ( Base ` G ) )
212	205, 211	syl5ss 3614	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ~P ( Base ` G ) )
213		sspwuni 4611	. . . . . . . . . 10 |- ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( Base ` G ) )
214	212, 213	sylib 208	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( Base ` G ) )
215	168, 3, 214	mrcssidd 16285	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
216		imassrn 5477	. . . . . . . . . . 11 |- ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ran S
217	216, 211	syl5ss 3614	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ~P ( Base ` G ) )
218		sspwuni 4611	. . . . . . . . . 10 |- ( ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( Base ` G ) )
219	217, 218	sylib 208	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( Base ` G ) )
220	168, 3, 219	mrcssidd 16285	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
221		unss12 3785	. . . . . . . 8 |- ( ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) /\ U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) -> ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
222	215, 220, 221	syl2anc 693	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
223	204, 222	eqsstrd 3639	. . . . . 6 |- ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
224	3	mrccl 16271	. . . . . . . 8 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) )
225	168, 214, 224	syl2anc 693	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) )
226	3	mrccl 16271	. . . . . . . 8 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( Base ` G ) ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. (SubGrp ` G ) )
227	168, 219, 226	syl2anc 693	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. (SubGrp ` G ) )
228		eqid 2622	. . . . . . . 8 |- ( LSSum ` G ) = ( LSSum ` G )
229	228	lsmunss 18073	. . . . . . 7 |- ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. (SubGrp ` G ) ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
230	225, 227, 229	syl2anc 693	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
231	223, 230	sstrd 3613	. . . . 5 |- ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
232		difss 3737	. . . . . . . . . . . . 13 |- ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( A |` { ( 1st ` x ) } )
233		ressn 5671	. . . . . . . . . . . . 13 |- ( A |` { ( 1st ` x ) } ) = ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) )
234	232, 233	sseqtri 3637	. . . . . . . . . . . 12 |- ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) )
235		imass2 5501	. . . . . . . . . . . 12 |- ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) )
236	234, 235	ax-mp 5	. . . . . . . . . . 11 |- ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) )
237		ovex 6678	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` x ) S i ) e. _V
238		oveq2 6658	. . . . . . . . . . . . . . . . 17 |- ( j = i -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S i ) )
239	58, 238	elrnmpt1s 5373	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( A " { ( 1st ` x ) } ) /\ ( ( 1st ` x ) S i ) e. _V ) -> ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
240	237, 239	mpan2 707	. . . . . . . . . . . . . . 15 |- ( i e. ( A " { ( 1st ` x ) } ) -> ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
241	240	rgen 2922	. . . . . . . . . . . . . 14 |- A. i e. ( A " { ( 1st ` x ) } ) ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) )
242	241	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> A. i e. ( A " { ( 1st ` x ) } ) ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
243		oveq1 6657	. . . . . . . . . . . . . . . 16 |- ( y = ( 1st ` x ) -> ( y S i ) = ( ( 1st ` x ) S i ) )
244	243	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( y = ( 1st ` x ) -> ( ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) <-> ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
245	244	ralbidv 2986	. . . . . . . . . . . . . 14 |- ( y = ( 1st ` x ) -> ( A. i e. ( A " { ( 1st ` x ) } ) ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) <-> A. i e. ( A " { ( 1st ` x ) } ) ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
246	92, 245	ralsn 4222	. . . . . . . . . . . . 13 |- ( A. y e. { ( 1st ` x ) } A. i e. ( A " { ( 1st ` x ) } ) ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) <-> A. i e. ( A " { ( 1st ` x ) } ) ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
247	242, 246	sylibr 224	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> A. y e. { ( 1st ` x ) } A. i e. ( A " { ( 1st ` x ) } ) ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
248	41	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> S : A --> (SubGrp ` G ) )
249		ffun 6048	. . . . . . . . . . . . . 14 |- ( S : A --> (SubGrp ` G ) -> Fun S )
250	248, 249	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> Fun S )
251		resss 5422	. . . . . . . . . . . . . . 15 |- ( A |` { ( 1st ` x ) } ) C_ A
252	233, 251	eqsstr3i 3636	. . . . . . . . . . . . . 14 |- ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) C_ A
253		fdm 6051	. . . . . . . . . . . . . . 15 |- ( S : A --> (SubGrp ` G ) -> dom S = A )
254	248, 253	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> dom S = A )
255	252, 254	syl5sseqr 3654	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) C_ dom S )
256		funimassov 6811	. . . . . . . . . . . . 13 |- ( ( Fun S /\ ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) C_ dom S ) -> ( ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) <-> A. y e. { ( 1st ` x ) } A. i e. ( A " { ( 1st ` x ) } ) ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
257	250, 255, 256	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) <-> A. y e. { ( 1st ` x ) } A. i e. ( A " { ( 1st ` x ) } ) ( y S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
258	247, 257	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
259	236, 258	syl5ss 3614	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
260	259	unissd 4462	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
261		df-ov 6653	. . . . . . . . . . . . . 14 |- ( ( 1st ` x ) S j ) = ( S ` <. ( 1st ` x ) , j >. )
262	41	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> S : A --> (SubGrp ` G ) )
263		elrelimasn 5489	. . . . . . . . . . . . . . . . . 18 |- ( Rel A -> ( j e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A j ) )
264	67, 263	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A ) -> ( j e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A j ) )
265	264	biimpa 501	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( 1st ` x ) A j )
266		df-br 4654	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` x ) A j <-> <. ( 1st ` x ) , j >. e. A )
267	265, 266	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> <. ( 1st ` x ) , j >. e. A )
268	262, 267	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( S ` <. ( 1st ` x ) , j >. ) e. (SubGrp ` G ) )
269	261, 268	syl5eqel 2705	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( ( 1st ` x ) S j ) e. (SubGrp ` G ) )
270	269, 58	fmptd 6385	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) : ( A " { ( 1st ` x ) } ) --> (SubGrp ` G ) )
271		frn 6053	. . . . . . . . . . . 12 |- ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) : ( A " { ( 1st ` x ) } ) --> (SubGrp ` G ) -> ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ (SubGrp ` G ) )
272	270, 271	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ (SubGrp ` G ) )
273	272, 210	sstrd 3613	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ~P ( Base ` G ) )
274		sspwuni 4611	. . . . . . . . . 10 |- ( ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ~P ( Base ` G ) <-> U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ( Base ` G ) )
275	273, 274	sylib 208	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ( Base ` G ) )
276	168, 3, 260, 275	mrcssd 16284	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( K ` U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
277	3	dprdspan 18426	. . . . . . . . 9 |- ( G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) = ( K ` U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
278	54, 277	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) = ( K ` U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
279	276, 278	sseqtr4d 3642	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
280	16, 17	fnmpti 6022	. . . . . . . . . . . . 13 |- ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) Fn I
281		fnressn 6425	. . . . . . . . . . . . 13 |- ( ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) Fn I /\ ( 1st ` x ) e. I ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) = { <. ( 1st ` x ) , ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) >. } )
282	280, 45, 281	sylancr 695	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) = { <. ( 1st ` x ) , ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) >. } )
283	125	opeq2d 4409	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> <. ( 1st ` x ) , ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) >. = <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. )
284	283	sneqd 4189	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> { <. ( 1st ` x ) , ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) >. } = { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } )
285	282, 284	eqtrd 2656	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) = { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } )
286	285	oveq2d 6666	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) ) = ( G DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } ) )
287		dprdsubg 18423	. . . . . . . . . . . . 13 |- ( G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. (SubGrp ` G ) )
288	54, 287	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. (SubGrp ` G ) )
289		dprdsn 18435	. . . . . . . . . . . 12 |- ( ( ( 1st ` x ) e. I /\ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. (SubGrp ` G ) ) -> ( G dom DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } /\ ( G DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) )
290	45, 288, 289	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( G dom DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } /\ ( G DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) )
291	290	simprd 479	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( G DProd { <. ( 1st ` x ) , ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) >. } ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
292	286, 291	eqtrd 2656	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
293	4	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
294	18	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I )
295		difss 3737	. . . . . . . . . . 11 |- ( I \ { ( 1st ` x ) } ) C_ I
296	295	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( I \ { ( 1st ` x ) } ) C_ I )
297		disjdif 4040	. . . . . . . . . . 11 |- ( { ( 1st ` x ) } i^i ( I \ { ( 1st ` x ) } ) ) = (/)
298	297	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } i^i ( I \ { ( 1st ` x ) } ) ) = (/) )
299	293, 294, 171, 296, 298, 1	dprdcntz2 18437	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` { ( 1st ` x ) } ) ) C_ ( (Cntz ` G ) ` ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) ) )
300	292, 299	eqsstr3d 3640	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) C_ ( (Cntz ` G ) ` ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) ) )
301	29	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. A ) /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
302	67, 248, 42, 301, 293, 3, 296	dprd2dlem1 18440	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( G DProd ( i e. ( I \ { ( 1st ` x ) } ) |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
303		resmpt 5449	. . . . . . . . . . . 12 |- ( ( I \ { ( 1st ` x ) } ) C_ I -> ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) = ( i e. ( I \ { ( 1st ` x ) } ) |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
304	295, 303	ax-mp 5	. . . . . . . . . . 11 |- ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) = ( i e. ( I \ { ( 1st ` x ) } ) |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) )
305	304	oveq2i 6661	. . . . . . . . . 10 |- ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) = ( G DProd ( i e. ( I \ { ( 1st ` x ) } ) |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
306	302, 305	syl6eqr 2674	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) )
307	306	fveq2d 6195	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( (Cntz ` G ) ` ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) = ( (Cntz ` G ) ` ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) ) )
308	300, 307	sseqtr4d 3642	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) C_ ( (Cntz ` G ) ` ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
309	279, 308	sstrd 3613	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( (Cntz ` G ) ` ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
310	228, 1	lsmsubg 18069	. . . . . 6 |- ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. (SubGrp ` G ) /\ ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( (Cntz ` G ) ` ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) e. (SubGrp ` G ) )
311	225, 227, 309, 310	syl3anc 1326	. . . . 5 |- ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) e. (SubGrp ` G ) )
312	3	mrcsscl 16280	. . . . 5 |- ( ( (SubGrp ` G ) e. (Moore ` ( Base ` G ) ) /\ U. ( S " ( A \ { x } ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) /\ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) e. (SubGrp ` G ) ) -> ( K ` U. ( S " ( A \ { x } ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
313	168, 231, 311, 312	syl3anc 1326	. . . 4 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A \ { x } ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
314		sslin 3839	. . . 4 |- ( ( K ` U. ( S " ( A \ { x } ) ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) ) )
315	313, 314	syl 17	. . 3 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( A \ { x } ) ) ) ) C_ ( ( S ` x ) i^i ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) ) )
316	41	ffvelrnda 6359	. . . 4 |- ( ( ph /\ x e. A ) -> ( S ` x ) e. (SubGrp ` G ) )
317	228	lsmlub 18078	. . . . . . . . . 10 |- ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) /\ ( S ` x ) e. (SubGrp ` G ) /\ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. (SubGrp ` G ) ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) /\ ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) <-> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) )
318	225, 316, 288, 317	syl3anc 1326	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) /\ ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) <-> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) ) )
319	279, 122, 318	mpbi2and 956	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
320	319, 125	sseqtr4d 3642	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) )
321	293, 294, 296	dprdres 18427	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) /\ ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) ) )
322	321	simpld 475	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) )
323	3	dprdspan 18426	. . . . . . . . . . 11 |- ( G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) = ( K ` U. ran ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) )
324	322, 323	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) = ( K ` U. ran ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) )
325		df-ima 5127	. . . . . . . . . . . 12 |- ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) = ran ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) )
326	325	unieqi 4445	. . . . . . . . . . 11 |- U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) = U. ran ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) )
327	326	fveq2i 6194	. . . . . . . . . 10 |- ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) = ( K ` U. ran ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) )
328	324, 327	syl6eqr 2674	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( G DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) ) = ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) )
329	306, 328	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) )
330		eqimss 3657	. . . . . . . 8 |- ( ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) C_ ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) )
331	329, 330	syl 17	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) C_ ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) )
332		ss2in 3840	. . . . . . 7 |- ( ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) /\ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) C_ ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) C_ ( ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) i^i ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) ) )
333	320, 331, 332	syl2anc 693	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) C_ ( ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) i^i ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) ) )
334	293, 294, 45, 2, 3	dprddisj 18408	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) i^i ( K ` U. ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) " ( I \ { ( 1st ` x ) } ) ) ) ) = { ( 0g ` G ) } )
335	333, 334	sseqtrd 3641	. . . . 5 |- ( ( ph /\ x e. A ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) C_ { ( 0g ` G ) } )
336	228	lsmub2 18072	. . . . . . . . 9 |- ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) /\ ( S ` x ) e. (SubGrp ` G ) ) -> ( S ` x ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) )
337	225, 316, 336	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) )
338	2	subg0cl 17602	. . . . . . . . 9 |- ( ( S ` x ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( S ` x ) )
339	316, 338	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( S ` x ) )
340	337, 339	sseldd 3604	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) )
341	2	subg0cl 17602	. . . . . . . 8 |- ( ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
342	227, 341	syl 17	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
343	340, 342	elind 3798	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
344	343	snssd 4340	. . . . 5 |- ( ( ph /\ x e. A ) -> { ( 0g ` G ) } C_ ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
345	335, 344	eqssd 3620	. . . 4 |- ( ( ph /\ x e. A ) -> ( ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) i^i ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) = { ( 0g ` G ) } )
346		incom 3805	. . . . 5 |- ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) i^i ( S ` x ) ) = ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
347	70, 102	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
348	62	fveq2d 6195	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S ` x ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
349	100, 347, 348	3eqtr4a 2682	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) )
350		eqimss2 3658	. . . . . . . . 9 |- ( ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) -> ( S ` x ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) )
351	349, 350	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) )
352		eldifsn 4317	. . . . . . . . . . . . 13 |- ( y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) <-> ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) )
353	11	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> Rel A )
354		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. ( A |` { ( 1st ` x ) } ) )
355	251, 354	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. A )
356	353, 355, 75	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
357	356	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
358	357, 110	syl6eqr 2674	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
359	356, 354	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) )
360		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2nd ` y ) e. _V
361	360	opelres 5401	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) <-> ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. A /\ ( 1st ` y ) e. { ( 1st ` x ) } ) )
362	361	simprbi 480	. . . . . . . . . . . . . . . . . . . 20 |- ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) -> ( 1st ` y ) e. { ( 1st ` x ) } )
363	359, 362	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 1st ` y ) e. { ( 1st ` x ) } )
364		elsni 4194	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` y ) e. { ( 1st ` x ) } -> ( 1st ` y ) = ( 1st ` x ) )
365	363, 364	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 1st ` y ) = ( 1st ` x ) )
366	365	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( ( 1st ` y ) S ( 2nd ` y ) ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
367	358, 366	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
368	354, 233	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) )
369		xp2nd 7199	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
370	368, 369	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
371		simprr 796	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y =/= x )
372	62	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
373	356, 372	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y = x <-> <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
374		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 1st ` y ) e. _V
375	374, 360	opth 4945	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( ( 1st ` y ) = ( 1st ` x ) /\ ( 2nd ` y ) = ( 2nd ` x ) ) )
376	375	baib 944	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1st ` y ) = ( 1st ` x ) -> ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
377	365, 376	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
378	373, 377	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y = x <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
379	378	necon3bid 2838	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y =/= x <-> ( 2nd ` y ) =/= ( 2nd ` x ) ) )
380	371, 379	mpbid 222	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) =/= ( 2nd ` x ) )
381		eldifsn 4317	. . . . . . . . . . . . . . . . . 18 |- ( ( 2nd ` y ) e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) <-> ( ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) /\ ( 2nd ` y ) =/= ( 2nd ` x ) ) )
382	370, 380, 381	sylanbrc 698	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) )
383		ovex 6678	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` x ) S ( 2nd ` y ) ) e. _V
384		difss 3737	. . . . . . . . . . . . . . . . . . 19 |- ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) C_ ( A " { ( 1st ` x ) } )
385		resmpt 5449	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) C_ ( A " { ( 1st ` x ) } ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) = ( j e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
386	384, 385	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) = ( j e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) |-> ( ( 1st ` x ) S j ) )
387		oveq2 6658	. . . . . . . . . . . . . . . . . 18 |- ( j = ( 2nd ` y ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
388	386, 387	elrnmpt1s 5373	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` y ) e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) /\ ( ( 1st ` x ) S ( 2nd ` y ) ) e. _V ) -> ( ( 1st ` x ) S ( 2nd ` y ) ) e. ran ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
389	382, 383, 388	sylancl 694	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( ( 1st ` x ) S ( 2nd ` y ) ) e. ran ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
390	367, 389	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) e. ran ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
391		df-ima 5127	. . . . . . . . . . . . . . 15 |- ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) = ran ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) |` ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) )
392	390, 391	syl6eleqr 2712	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
393	392	ex 450	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) -> ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) )
394	352, 393	syl5bi 232	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) -> ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) )
395	394	ralrimiv 2965	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> A. y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
396	234, 255	syl5ss 3614	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ dom S )
397		funimass4 6247	. . . . . . . . . . . 12 |- ( ( Fun S /\ ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ dom S ) -> ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) <-> A. y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) )
398	250, 396, 397	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) <-> A. y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) ( S ` y ) e. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) )
399	395, 398	mpbird 247	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
400	399	unissd 4462	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
401		imassrn 5477	. . . . . . . . . . 11 |- ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) )
402	401, 273	syl5ss 3614	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ~P ( Base ` G ) )
403		sspwuni 4611	. . . . . . . . . 10 |- ( ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ~P ( Base ` G ) <-> U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ( Base ` G ) )
404	402, 403	sylib 208	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ( Base ` G ) )
405	168, 3, 400, 404	mrcssd 16284	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( K ` U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) )
406		ss2in 3840	. . . . . . . 8 |- ( ( ( S ` x ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) /\ ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( K ` U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) C_ ( ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) i^i ( K ` U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) ) )
407	351, 405, 406	syl2anc 693	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) C_ ( ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) i^i ( K ` U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) ) )
408	59	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> dom ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( A " { ( 1st ` x ) } ) )
409	54, 408, 70, 2, 3	dprddisj 18408	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) i^i ( K ` U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) ) ) = { ( 0g ` G ) } )
410	407, 409	sseqtrd 3641	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
411	2	subg0cl 17602	. . . . . . . . 9 |- ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. (SubGrp ` G ) -> ( 0g ` G ) e. ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
412	225, 411	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
413	339, 412	elind 3798	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) )
414	413	snssd 4340	. . . . . 6 |- ( ( ph /\ x e. A ) -> { ( 0g ` G ) } C_ ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) )
415	410, 414	eqssd 3620	. . . . 5 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) = { ( 0g ` G ) } )
416	346, 415	syl5eq 2668	. . . 4 |- ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) i^i ( S ` x ) ) = { ( 0g ` G ) } )
417	228, 225, 316, 227, 2, 345, 416	lsmdisj2 18095	. . 3 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) ) = { ( 0g ` G ) } )
418	315, 417	sseqtrd 3641	. 2 |- ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( A \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
419	1, 2, 3, 6, 40, 41, 164, 418	dmdprdd 18398	1 |- ( ph -> G dom DProd S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   <.cop 4183   U.cuni 4436   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Rel wrel 5119   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   Basecbs 15857   0gc0g 16100  Moorecmre 16242  mrClscmrc 16243  ACScacs 16245   Grpcgrp 17422  SubGrpcsubg 17588  Cntzccntz 17748   LSSumclsm 18049   DProd cdprd 18392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-0g 16102  df-gsum 16103  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-gim 17701  df-cntz 17750  df-oppg 17776  df-lsm 18051  df-cmn 18195  df-dprd 18394

This theorem is referenced by:  dprd2db  18442  dprd2d2  18443