Metamath Proof Explorer

Theorem dprd2da

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

Ref Expression
Hypotheses 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 dprd2da 
|- ( ph -> G dom DProd S )

Proof

Step Hyp Ref Expression
1 dprd2d.1 
 |-  ( ph -> Rel A )
2 dprd2d.2 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
3 dprd2d.3 
 |-  ( ph -> dom A C_ I )
4 dprd2d.4 
 |-  ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
5 dprd2d.5 
 |-  ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
6 dprd2d.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
7 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 dprdgrp 
 |-  ( G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) -> G e. Grp )
10 5 9 syl 
 |-  ( ph -> G e. Grp )
11 resiun2 
 |-  ( A |` U_ i e. I { i } ) = U_ i e. I ( A |` { i } )
12 iunid 
 |-  U_ i e. I { i } = I
13 12 reseq2i 
 |-  ( A |` U_ i e. I { i } ) = ( A |` I )
14 11 13 eqtr3i 
 |-  U_ i e. I ( A |` { i } ) = ( A |` I )
15 relssres 
 |-  ( ( Rel A /\ dom A C_ I ) -> ( A |` I ) = A )
16 1 3 15 syl2anc 
 |-  ( ph -> ( A |` I ) = A )
17 14 16 eqtrid 
 |-  ( ph -> U_ i e. I ( A |` { i } ) = A )
18 ovex 
 |-  ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) e. _V
19 eqid 
 |-  ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) )
20 18 19 dmmpti 
 |-  dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I
21 reldmdprd 
 |-  Rel dom DProd
22 21 brrelex2i 
 |-  ( 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 )
23 dmexg 
 |-  ( ( 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 )
24 5 22 23 3syl 
 |-  ( ph -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) e. _V )
25 20 24 eqeltrrid 
 |-  ( ph -> I e. _V )
26 ressn 
 |-  ( A |` { i } ) = ( { i } X. ( A " { i } ) )
27 snex 
 |-  { i } e. _V
28 ovex 
 |-  ( i S j ) e. _V
29 eqid 
 |-  ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { i } ) |-> ( i S j ) )
30 28 29 dmmpti 
 |-  dom ( j e. ( A " { i } ) |-> ( i S j ) ) = ( A " { i } )
31 21 brrelex2i 
 |-  ( G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
32 dmexg 
 |-  ( ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V -> dom ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
33 4 31 32 3syl 
 |-  ( ( ph /\ i e. I ) -> dom ( j e. ( A " { i } ) |-> ( i S j ) ) e. _V )
34 30 33 eqeltrrid 
 |-  ( ( ph /\ i e. I ) -> ( A " { i } ) e. _V )
35 xpexg 
 |-  ( ( { i } e. _V /\ ( A " { i } ) e. _V ) -> ( { i } X. ( A " { i } ) ) e. _V )
36 27 34 35 sylancr 
 |-  ( ( ph /\ i e. I ) -> ( { i } X. ( A " { i } ) ) e. _V )
37 26 36 eqeltrid 
 |-  ( ( ph /\ i e. I ) -> ( A |` { i } ) e. _V )
38 37 ralrimiva 
 |-  ( ph -> A. i e. I ( A |` { i } ) e. _V )
39 iunexg 
 |-  ( ( I e. _V /\ A. i e. I ( A |` { i } ) e. _V ) -> U_ i e. I ( A |` { i } ) e. _V )
40 25 38 39 syl2anc 
 |-  ( ph -> U_ i e. I ( A |` { i } ) e. _V )
41 17 40 eqeltrrd 
 |-  ( ph -> A e. _V )
42 sneq 
 |-  ( i = ( 1st ` x ) -> { i } = { ( 1st ` x ) } )
43 42 imaeq2d 
 |-  ( i = ( 1st ` x ) -> ( A " { i } ) = ( A " { ( 1st ` x ) } ) )
44 oveq1 
 |-  ( i = ( 1st ` x ) -> ( i S j ) = ( ( 1st ` x ) S j ) )
45 43 44 mpteq12dv 
 |-  ( i = ( 1st ` x ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
46 45 breq2d 
 |-  ( 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 ) ) ) )
47 4 ralrimiva 
 |-  ( ph -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
48 47 adantr 
 |-  ( ( ph /\ x e. A ) -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
49 3 adantr 
 |-  ( ( ph /\ x e. A ) -> dom A C_ I )
50 1stdm 
 |-  ( ( Rel A /\ x e. A ) -> ( 1st ` x ) e. dom A )
51 1 50 sylan 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` x ) e. dom A )
52 49 51 sseldd 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` x ) e. I )
53 46 48 52 rspcdva 
 |-  ( ( ph /\ x e. A ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
54 53 3ad2antr1 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> G dom DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
55 54 adantr 
 |-  ( ( ( 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 ) ) )
56 ovex 
 |-  ( ( 1st ` x ) S j ) e. _V
57 eqid 
 |-  ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) )
58 56 57 dmmpti 
 |-  dom ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( A " { ( 1st ` x ) } )
59 58 a1i 
 |-  ( ( ( 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 ) } ) )
60 1st2nd 
 |-  ( ( Rel A /\ x e. A ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
61 1 60 sylan 
 |-  ( ( ph /\ x e. A ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
62 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
63 61 62 eqeltrrd 
 |-  ( ( ph /\ x e. A ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. A )
64 df-br 
 |-  ( ( 1st ` x ) A ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. A )
65 63 64 sylibr 
 |-  ( ( ph /\ x e. A ) -> ( 1st ` x ) A ( 2nd ` x ) )
66 1 adantr 
 |-  ( ( ph /\ x e. A ) -> Rel A )
67 elrelimasn 
 |-  ( Rel A -> ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A ( 2nd ` x ) ) )
68 66 67 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A ( 2nd ` x ) ) )
69 65 68 mpbird 
 |-  ( ( ph /\ x e. A ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
70 69 3ad2antr1 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
71 70 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) )
72 1 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> Rel A )
73 simpr2 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> y e. A )
74 1st2nd 
 |-  ( ( Rel A /\ y e. A ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
75 72 73 74 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
76 75 73 eqeltrrd 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. A )
77 df-br 
 |-  ( ( 1st ` y ) A ( 2nd ` y ) <-> <. ( 1st ` y ) , ( 2nd ` y ) >. e. A )
78 76 77 sylibr 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) A ( 2nd ` y ) )
79 elrelimasn 
 |-  ( Rel A -> ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) <-> ( 1st ` y ) A ( 2nd ` y ) ) )
80 72 79 syl 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) <-> ( 1st ` y ) A ( 2nd ` y ) ) )
81 78 80 mpbird 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) )
82 81 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) )
83 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 1st ` x ) = ( 1st ` y ) )
84 83 sneqd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> { ( 1st ` x ) } = { ( 1st ` y ) } )
85 84 imaeq2d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( A " { ( 1st ` x ) } ) = ( A " { ( 1st ` y ) } ) )
86 82 85 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
87 simplr3 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> x =/= y )
88 simpr1 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> x e. A )
89 72 88 60 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
90 89 75 eqeq12d 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( x = y <-> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
91 fvex 
 |-  ( 1st ` x ) e. _V
92 fvex 
 |-  ( 2nd ` x ) e. _V
93 91 92 opth 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
94 90 93 bitrdi 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( x = y <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) ) )
95 94 baibd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( x = y <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
96 95 necon3bid 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( x =/= y <-> ( 2nd ` x ) =/= ( 2nd ` y ) ) )
97 87 96 mpbid 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( 2nd ` x ) =/= ( 2nd ` y ) )
98 55 59 71 86 97 7 dprdcntz 
 |-  ( ( ( 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 ) ) ) )
99 df-ov 
 |-  ( ( 1st ` x ) S ( 2nd ` x ) ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
100 oveq2 
 |-  ( j = ( 2nd ` x ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
101 100 57 56 fvmpt3i 
 |-  ( ( 2nd ` x ) e. ( A " { ( 1st ` x ) } ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
102 70 101 syl 
 |-  ( ( 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 ) ) )
103 89 fveq2d 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` x ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
104 99 102 103 3eqtr4a 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) )
105 104 adantr 
 |-  ( ( ( 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 ) )
106 83 oveq1d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` y ) S j ) )
107 85 106 mpteq12dv 
 |-  ( ( ( 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 ) ) )
108 107 fveq1d 
 |-  ( ( ( 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 ) ) )
109 df-ov 
 |-  ( ( 1st ` y ) S ( 2nd ` y ) ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. )
110 oveq2 
 |-  ( j = ( 2nd ` y ) -> ( ( 1st ` y ) S j ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
111 eqid 
 |-  ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) )
112 ovex 
 |-  ( ( 1st ` y ) S j ) e. _V
113 110 111 112 fvmpt3i 
 |-  ( ( 2nd ` y ) e. ( A " { ( 1st ` y ) } ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
114 81 113 syl 
 |-  ( ( 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 ) ) )
115 75 fveq2d 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` y ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
116 109 114 115 3eqtr4a 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ` ( 2nd ` y ) ) = ( S ` y ) )
117 116 adantr 
 |-  ( ( ( 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 ) )
118 108 117 eqtrd 
 |-  ( ( ( 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 ) )
119 118 fveq2d 
 |-  ( ( ( 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 ) ) )
120 98 105 119 3sstr3d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) = ( 1st ` y ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
121 1 2 3 4 5 6 dprd2dlem2 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
122 45 oveq2d 
 |-  ( i = ( 1st ` x ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) = ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
123 122 19 18 fvmpt3i 
 |-  ( ( 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 ) ) ) )
124 52 123 syl 
 |-  ( ( 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 ) ) ) )
125 121 124 sseqtrrd 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ` ( 1st ` x ) ) )
126 125 3ad2antr1 
 |-  ( ( 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 ) ) )
127 126 adantr 
 |-  ( ( ( 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 ) ) )
128 5 ad2antrr 
 |-  ( ( ( 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 ) ) ) ) )
129 20 a1i 
 |-  ( ( ( 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 )
130 52 3ad2antr1 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` x ) e. I )
131 130 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) e. I )
132 3 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> dom A C_ I )
133 1stdm 
 |-  ( ( Rel A /\ y e. A ) -> ( 1st ` y ) e. dom A )
134 72 73 133 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) e. dom A )
135 132 134 sseldd 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( 1st ` y ) e. I )
136 135 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` y ) e. I )
137 simpr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( 1st ` x ) =/= ( 1st ` y ) )
138 128 129 131 136 137 7 dprdcntz 
 |-  ( ( ( 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 ) ) ) )
139 sneq 
 |-  ( i = ( 1st ` y ) -> { i } = { ( 1st ` y ) } )
140 139 imaeq2d 
 |-  ( i = ( 1st ` y ) -> ( A " { i } ) = ( A " { ( 1st ` y ) } ) )
141 oveq1 
 |-  ( i = ( 1st ` y ) -> ( i S j ) = ( ( 1st ` y ) S j ) )
142 140 141 mpteq12dv 
 |-  ( i = ( 1st ` y ) -> ( j e. ( A " { i } ) |-> ( i S j ) ) = ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) )
143 142 oveq2d 
 |-  ( i = ( 1st ` y ) -> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) = ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
144 143 19 18 fvmpt3i 
 |-  ( ( 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 ) ) ) )
145 135 144 syl 
 |-  ( ( 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 ) ) ) )
146 145 fveq2d 
 |-  ( ( 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 ) ) ) ) )
147 eqid 
 |-  ( Base ` G ) = ( Base ` G )
148 147 dprdssv 
 |-  ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) C_ ( Base ` G )
149 142 breq2d 
 |-  ( 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 ) ) ) )
150 47 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> A. i e. I G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
151 149 150 135 rspcdva 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> G dom DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) )
152 112 111 dmmpti 
 |-  dom ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( A " { ( 1st ` y ) } )
153 152 a1i 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> dom ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) = ( A " { ( 1st ` y ) } ) )
154 151 153 81 dprdub 
 |-  ( ( 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 ) ) ) )
155 116 154 eqsstrrd 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` y ) C_ ( G DProd ( j e. ( A " { ( 1st ` y ) } ) |-> ( ( 1st ` y ) S j ) ) ) )
156 147 7 cntz2ss 
 |-  ( ( ( 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 ) ) )
157 148 155 156 sylancr 
 |-  ( ( 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 ) ) )
158 146 157 eqsstrd 
 |-  ( ( 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 ) ) )
159 158 adantr 
 |-  ( ( ( 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 ) ) )
160 138 159 sstrd 
 |-  ( ( ( 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 ) ) )
161 127 160 sstrd 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) /\ ( 1st ` x ) =/= ( 1st ` y ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
162 120 161 pm2.61dane 
 |-  ( ( ph /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> ( S ` x ) C_ ( ( Cntz ` G ) ` ( S ` y ) ) )
163 10 adantr 
 |-  ( ( ph /\ x e. A ) -> G e. Grp )
164 147 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
165 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
166 163 164 165 3syl 
 |-  ( ( ph /\ x e. A ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
167 16 adantr 
 |-  ( ( ph /\ x e. A ) -> ( A |` I ) = A )
168 undif2 
 |-  ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) = ( { ( 1st ` x ) } u. I )
169 52 snssd 
 |-  ( ( ph /\ x e. A ) -> { ( 1st ` x ) } C_ I )
170 ssequn1 
 |-  ( { ( 1st ` x ) } C_ I <-> ( { ( 1st ` x ) } u. I ) = I )
171 169 170 sylib 
 |-  ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } u. I ) = I )
172 168 171 eqtr2id 
 |-  ( ( ph /\ x e. A ) -> I = ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) )
173 172 reseq2d 
 |-  ( ( ph /\ x e. A ) -> ( A |` I ) = ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) )
174 167 173 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> A = ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) )
175 resundi 
 |-  ( A |` ( { ( 1st ` x ) } u. ( I \ { ( 1st ` x ) } ) ) ) = ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) )
176 174 175 eqtrdi 
 |-  ( ( ph /\ x e. A ) -> A = ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
177 176 difeq1d 
 |-  ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) \ { x } ) )
178 difundir 
 |-  ( ( ( A |` { ( 1st ` x ) } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
179 177 178 eqtrdi 
 |-  ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) ) )
180 neirr 
 |-  -. ( 1st ` x ) =/= ( 1st ` x )
181 61 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( x e. ( A |` ( I \ { ( 1st ` x ) } ) ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
182 df-br 
 |-  ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
183 92 brresi 
 |-  ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) <-> ( ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) /\ ( 1st ` x ) A ( 2nd ` x ) ) )
184 183 simplbi 
 |-  ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) -> ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) )
185 eldifsni 
 |-  ( ( 1st ` x ) e. ( I \ { ( 1st ` x ) } ) -> ( 1st ` x ) =/= ( 1st ` x ) )
186 184 185 syl 
 |-  ( ( 1st ` x ) ( A |` ( I \ { ( 1st ` x ) } ) ) ( 2nd ` x ) -> ( 1st ` x ) =/= ( 1st ` x ) )
187 182 186 sylbir 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( A |` ( I \ { ( 1st ` x ) } ) ) -> ( 1st ` x ) =/= ( 1st ` x ) )
188 181 187 syl6bi 
 |-  ( ( ph /\ x e. A ) -> ( x e. ( A |` ( I \ { ( 1st ` x ) } ) ) -> ( 1st ` x ) =/= ( 1st ` x ) ) )
189 180 188 mtoi 
 |-  ( ( ph /\ x e. A ) -> -. x e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
190 disjsn 
 |-  ( ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) <-> -. x e. ( A |` ( I \ { ( 1st ` x ) } ) ) )
191 189 190 sylibr 
 |-  ( ( ph /\ x e. A ) -> ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) )
192 disj3 
 |-  ( ( ( A |` ( I \ { ( 1st ` x ) } ) ) i^i { x } ) = (/) <-> ( A |` ( I \ { ( 1st ` x ) } ) ) = ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
193 191 192 sylib 
 |-  ( ( ph /\ x e. A ) -> ( A |` ( I \ { ( 1st ` x ) } ) ) = ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) )
194 193 eqcomd 
 |-  ( ( ph /\ x e. A ) -> ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) = ( A |` ( I \ { ( 1st ` x ) } ) ) )
195 194 uneq2d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( ( A |` ( I \ { ( 1st ` x ) } ) ) \ { x } ) ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
196 179 195 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( A \ { x } ) = ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
197 196 imaeq2d 
 |-  ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) = ( S " ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
198 imaundi 
 |-  ( S " ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) u. ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) = ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) )
199 197 198 eqtrdi 
 |-  ( ( ph /\ x e. A ) -> ( S " ( A \ { x } ) ) = ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
200 199 unieqd 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) = U. ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
201 uniun 
 |-  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 ) } ) ) ) )
202 200 201 eqtrdi 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) = ( U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) u. U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
203 imassrn 
 |-  ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ran S
204 2 frnd 
 |-  ( ph -> ran S C_ ( SubGrp ` G ) )
205 204 adantr 
 |-  ( ( ph /\ x e. A ) -> ran S C_ ( SubGrp ` G ) )
206 mresspw 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
207 166 206 syl 
 |-  ( ( ph /\ x e. A ) -> ( SubGrp ` G ) C_ ~P ( Base ` G ) )
208 205 207 sstrd 
 |-  ( ( ph /\ x e. A ) -> ran S C_ ~P ( Base ` G ) )
209 203 208 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ~P ( Base ` G ) )
210 sspwuni 
 |-  ( ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( Base ` G ) )
211 209 210 sylib 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( Base ` G ) )
212 166 6 211 mrcssidd 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
213 imassrn 
 |-  ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ran S
214 213 208 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ~P ( Base ` G ) )
215 sspwuni 
 |-  ( ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ~P ( Base ` G ) <-> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( Base ` G ) )
216 214 215 sylib 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( Base ` G ) )
217 166 6 216 mrcssidd 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) C_ ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
218 unss12 
 |-  ( ( 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 ) } ) ) ) ) ) )
219 212 217 218 syl2anc 
 |-  ( ( 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 ) } ) ) ) ) ) )
220 202 219 eqsstrd 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( A \ { x } ) ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) u. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
221 6 mrccl 
 |-  ( ( ( 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 ) )
222 166 211 221 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. ( SubGrp ` G ) )
223 6 mrccl 
 |-  ( ( ( 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 ) )
224 166 216 223 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. ( SubGrp ` G ) )
225 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
226 225 lsmunss 
 |-  ( ( ( 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 ) } ) ) ) ) ) )
227 222 224 226 syl2anc 
 |-  ( ( 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 ) } ) ) ) ) ) )
228 220 227 sstrd 
 |-  ( ( 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 ) } ) ) ) ) ) )
229 difss 
 |-  ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( A |` { ( 1st ` x ) } )
230 ressn 
 |-  ( A |` { ( 1st ` x ) } ) = ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) )
231 229 230 sseqtri 
 |-  ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) )
232 imass2 
 |-  ( ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) )
233 231 232 ax-mp 
 |-  ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) )
234 ovex 
 |-  ( ( 1st ` x ) S i ) e. _V
235 oveq2 
 |-  ( j = i -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S i ) )
236 57 235 elrnmpt1s 
 |-  ( ( 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 ) ) )
237 234 236 mpan2 
 |-  ( i e. ( A " { ( 1st ` x ) } ) -> ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
238 237 rgen 
 |-  A. i e. ( A " { ( 1st ` x ) } ) ( ( 1st ` x ) S i ) e. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) )
239 238 a1i 
 |-  ( ( 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 ) ) )
240 oveq1 
 |-  ( y = ( 1st ` x ) -> ( y S i ) = ( ( 1st ` x ) S i ) )
241 240 eleq1d 
 |-  ( 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 ) ) ) )
242 241 ralbidv 
 |-  ( 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 ) ) ) )
243 91 242 ralsn 
 |-  ( 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 ) ) )
244 239 243 sylibr 
 |-  ( ( 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 ) ) )
245 2 adantr 
 |-  ( ( ph /\ x e. A ) -> S : A --> ( SubGrp ` G ) )
246 245 ffund 
 |-  ( ( ph /\ x e. A ) -> Fun S )
247 resss 
 |-  ( A |` { ( 1st ` x ) } ) C_ A
248 230 247 eqsstrri 
 |-  ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) C_ A
249 245 fdmd 
 |-  ( ( ph /\ x e. A ) -> dom S = A )
250 248 249 sseqtrrid 
 |-  ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) C_ dom S )
251 funimassov 
 |-  ( ( 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 ) ) ) )
252 246 250 251 syl2anc 
 |-  ( ( 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 ) ) ) )
253 244 252 mpbird 
 |-  ( ( ph /\ x e. A ) -> ( S " ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
254 233 253 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
255 254 unissd 
 |-  ( ( ph /\ x e. A ) -> U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) )
256 df-ov 
 |-  ( ( 1st ` x ) S j ) = ( S ` <. ( 1st ` x ) , j >. )
257 2 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> S : A --> ( SubGrp ` G ) )
258 elrelimasn 
 |-  ( Rel A -> ( j e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A j ) )
259 66 258 syl 
 |-  ( ( ph /\ x e. A ) -> ( j e. ( A " { ( 1st ` x ) } ) <-> ( 1st ` x ) A j ) )
260 259 biimpa 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( 1st ` x ) A j )
261 df-br 
 |-  ( ( 1st ` x ) A j <-> <. ( 1st ` x ) , j >. e. A )
262 260 261 sylib 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> <. ( 1st ` x ) , j >. e. A )
263 257 262 ffvelrnd 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( S ` <. ( 1st ` x ) , j >. ) e. ( SubGrp ` G ) )
264 256 263 eqeltrid 
 |-  ( ( ( ph /\ x e. A ) /\ j e. ( A " { ( 1st ` x ) } ) ) -> ( ( 1st ` x ) S j ) e. ( SubGrp ` G ) )
265 264 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) : ( A " { ( 1st ` x ) } ) --> ( SubGrp ` G ) )
266 265 frnd 
 |-  ( ( ph /\ x e. A ) -> ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ( SubGrp ` G ) )
267 266 207 sstrd 
 |-  ( ( ph /\ x e. A ) -> ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ~P ( Base ` G ) )
268 sspwuni 
 |-  ( 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 ) )
269 267 268 sylib 
 |-  ( ( ph /\ x e. A ) -> U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) C_ ( Base ` G ) )
270 166 6 255 269 mrcssd 
 |-  ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( K ` U. ran ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
271 6 dprdspan 
 |-  ( 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 ) ) ) )
272 53 271 syl 
 |-  ( ( 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 ) ) ) )
273 270 272 sseqtrrd 
 |-  ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) )
274 18 19 fnmpti 
 |-  ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) Fn I
275 fnressn 
 |-  ( ( ( 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 ) ) >. } )
276 274 52 275 sylancr 
 |-  ( ( 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 ) ) >. } )
277 124 opeq2d 
 |-  ( ( 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 ) ) ) >. )
278 277 sneqd 
 |-  ( ( 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 ) ) ) >. } )
279 276 278 eqtrd 
 |-  ( ( 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 ) ) ) >. } )
280 279 oveq2d 
 |-  ( ( 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 ) ) ) >. } ) )
281 dprdsubg 
 |-  ( 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 ) )
282 53 281 syl 
 |-  ( ( ph /\ x e. A ) -> ( G DProd ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ) e. ( SubGrp ` G ) )
283 dprdsn 
 |-  ( ( ( 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 ) ) ) ) )
284 52 282 283 syl2anc 
 |-  ( ( 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 ) ) ) ) )
285 284 simprd 
 |-  ( ( 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 ) ) ) )
286 280 285 eqtrd 
 |-  ( ( 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 ) ) ) )
287 5 adantr 
 |-  ( ( ph /\ x e. A ) -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )
288 20 a1i 
 |-  ( ( ph /\ x e. A ) -> dom ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) = I )
289 difss 
 |-  ( I \ { ( 1st ` x ) } ) C_ I
290 289 a1i 
 |-  ( ( ph /\ x e. A ) -> ( I \ { ( 1st ` x ) } ) C_ I )
291 disjdif 
 |-  ( { ( 1st ` x ) } i^i ( I \ { ( 1st ` x ) } ) ) = (/)
292 291 a1i 
 |-  ( ( ph /\ x e. A ) -> ( { ( 1st ` x ) } i^i ( I \ { ( 1st ` x ) } ) ) = (/) )
293 287 288 169 290 292 7 dprdcntz2 
 |-  ( ( 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 ) } ) ) ) ) )
294 286 293 eqsstrrd 
 |-  ( ( 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 ) } ) ) ) ) )
295 4 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )
296 66 245 49 295 287 6 290 dprd2dlem1 
 |-  ( ( 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 ) ) ) ) ) )
297 resmpt 
 |-  ( ( 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 ) ) ) ) )
298 289 297 ax-mp 
 |-  ( ( 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 ) ) ) )
299 298 oveq2i 
 |-  ( 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 ) ) ) ) )
300 296 299 eqtr4di 
 |-  ( ( 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 ) } ) ) ) )
301 300 fveq2d 
 |-  ( ( 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 ) } ) ) ) ) )
302 294 301 sseqtrrd 
 |-  ( ( 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 ) } ) ) ) ) ) )
303 273 302 sstrd 
 |-  ( ( ph /\ x e. A ) -> ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) C_ ( ( Cntz ` G ) ` ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) )
304 225 7 lsmsubg 
 |-  ( ( ( 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 ) )
305 222 224 303 304 syl3anc 
 |-  ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) ) e. ( SubGrp ` G ) )
306 6 mrcsscl 
 |-  ( ( ( 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 ) } ) ) ) ) ) )
307 166 228 305 306 syl3anc 
 |-  ( ( 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 ) } ) ) ) ) ) )
308 sslin 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
309 307 308 syl 
 |-  ( ( 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 ) } ) ) ) ) ) ) )
310 2 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) e. ( SubGrp ` G ) )
311 225 lsmlub 
 |-  ( ( ( 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 ) ) ) ) )
312 222 310 282 311 syl3anc 
 |-  ( ( 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 ) ) ) ) )
313 273 121 312 mpbi2and 
 |-  ( ( 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 ) ) ) )
314 313 124 sseqtrrd 
 |-  ( ( 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 ) ) )
315 287 288 290 dprdres 
 |-  ( ( 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 ) ) ) ) ) ) )
316 315 simpld 
 |-  ( ( ph /\ x e. A ) -> G dom DProd ( ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) |` ( I \ { ( 1st ` x ) } ) ) )
317 6 dprdspan 
 |-  ( 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 ) } ) ) ) )
318 316 317 syl 
 |-  ( ( 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 ) } ) ) ) )
319 df-ima 
 |-  ( ( 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 ) } ) )
320 319 unieqi 
 |-  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 ) } ) )
321 320 fveq2i 
 |-  ( 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 ) } ) ) )
322 318 321 eqtr4di 
 |-  ( ( 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 ) } ) ) ) )
323 300 322 eqtrd 
 |-  ( ( 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 ) } ) ) ) )
324 eqimss 
 |-  ( ( 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 ) } ) ) ) )
325 323 324 syl 
 |-  ( ( 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 ) } ) ) ) )
326 ss2in 
 |-  ( ( ( ( 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 ) } ) ) ) ) )
327 314 325 326 syl2anc 
 |-  ( ( 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 ) } ) ) ) ) )
328 287 288 52 8 6 dprddisj 
 |-  ( ( 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 ) } )
329 327 328 sseqtrd 
 |-  ( ( 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 ) } )
330 225 lsmub2 
 |-  ( ( ( 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 ) ) )
331 222 310 330 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) )
332 8 subg0cl 
 |-  ( ( S ` x ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( S ` x ) )
333 310 332 syl 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( S ` x ) )
334 331 333 sseldd 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ( LSSum ` G ) ( S ` x ) ) )
335 8 subg0cl 
 |-  ( ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
336 224 335 syl 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( K ` U. ( S " ( A |` ( I \ { ( 1st ` x ) } ) ) ) ) )
337 334 336 elind 
 |-  ( ( 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 ) } ) ) ) ) ) )
338 337 snssd 
 |-  ( ( 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 ) } ) ) ) ) ) )
339 329 338 eqssd 
 |-  ( ( 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 ) } )
340 incom 
 |-  ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) i^i ( S ` x ) ) = ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
341 69 101 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( ( 1st ` x ) S ( 2nd ` x ) ) )
342 61 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) = ( S ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
343 99 341 342 3eqtr4a 
 |-  ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) = ( S ` x ) )
344 eqimss2 
 |-  ( ( ( 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 ) ) )
345 343 344 syl 
 |-  ( ( ph /\ x e. A ) -> ( S ` x ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) ` ( 2nd ` x ) ) )
346 eldifsn 
 |-  ( y e. ( ( A |` { ( 1st ` x ) } ) \ { x } ) <-> ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) )
347 1 ad2antrr 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> Rel A )
348 simprl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. ( A |` { ( 1st ` x ) } ) )
349 247 348 sselid 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. A )
350 347 349 74 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
351 350 fveq2d 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( S ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
352 351 109 eqtr4di 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( ( 1st ` y ) S ( 2nd ` y ) ) )
353 350 348 eqeltrrd 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) )
354 fvex 
 |-  ( 2nd ` y ) e. _V
355 354 opelresi 
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) <-> ( ( 1st ` y ) e. { ( 1st ` x ) } /\ <. ( 1st ` y ) , ( 2nd ` y ) >. e. A ) )
356 355 simplbi 
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. ( A |` { ( 1st ` x ) } ) -> ( 1st ` y ) e. { ( 1st ` x ) } )
357 353 356 syl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 1st ` y ) e. { ( 1st ` x ) } )
358 elsni 
 |-  ( ( 1st ` y ) e. { ( 1st ` x ) } -> ( 1st ` y ) = ( 1st ` x ) )
359 357 358 syl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 1st ` y ) = ( 1st ` x ) )
360 359 oveq1d 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( ( 1st ` y ) S ( 2nd ` y ) ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
361 352 360 eqtrd 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( S ` y ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
362 348 230 eleqtrdi 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y e. ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) )
363 xp2nd 
 |-  ( y e. ( { ( 1st ` x ) } X. ( A " { ( 1st ` x ) } ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
364 362 363 syl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) )
365 simprr 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> y =/= x )
366 61 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
367 350 366 eqeq12d 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y = x <-> <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
368 fvex 
 |-  ( 1st ` y ) e. _V
369 368 354 opth 
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( ( 1st ` y ) = ( 1st ` x ) /\ ( 2nd ` y ) = ( 2nd ` x ) ) )
370 369 baib 
 |-  ( ( 1st ` y ) = ( 1st ` x ) -> ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
371 359 370 syl 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( <. ( 1st ` y ) , ( 2nd ` y ) >. = <. ( 1st ` x ) , ( 2nd ` x ) >. <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
372 367 371 bitrd 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y = x <-> ( 2nd ` y ) = ( 2nd ` x ) ) )
373 372 necon3bid 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( y =/= x <-> ( 2nd ` y ) =/= ( 2nd ` x ) ) )
374 365 373 mpbid 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) =/= ( 2nd ` x ) )
375 eldifsn 
 |-  ( ( 2nd ` y ) e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) <-> ( ( 2nd ` y ) e. ( A " { ( 1st ` x ) } ) /\ ( 2nd ` y ) =/= ( 2nd ` x ) ) )
376 364 374 375 sylanbrc 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. ( A |` { ( 1st ` x ) } ) /\ y =/= x ) ) -> ( 2nd ` y ) e. ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) )
377 ovex 
 |-  ( ( 1st ` x ) S ( 2nd ` y ) ) e. _V
378 difss 
 |-  ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) C_ ( A " { ( 1st ` x ) } )
379 resmpt 
 |-  ( ( ( 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 ) ) )
380 378 379 ax-mp 
 |-  ( ( 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 ) )
381 oveq2 
 |-  ( j = ( 2nd ` y ) -> ( ( 1st ` x ) S j ) = ( ( 1st ` x ) S ( 2nd ` y ) ) )
382 380 381 elrnmpt1s 
 |-  ( ( ( 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 ) } ) ) )
383 376 377 382 sylancl 
 |-  ( ( ( 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 ) } ) ) )
384 361 383 eqeltrd 
 |-  ( ( ( 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 ) } ) ) )
385 df-ima 
 |-  ( ( 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 ) } ) )
386 384 385 eleqtrrdi 
 |-  ( ( ( 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 ) } ) ) )
387 386 ex 
 |-  ( ( 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 ) } ) ) ) )
388 346 387 syl5bi 
 |-  ( ( 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 ) } ) ) ) )
389 388 ralrimiv 
 |-  ( ( 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 ) } ) ) )
390 231 250 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( ( A |` { ( 1st ` x ) } ) \ { x } ) C_ dom S )
391 funimass4 
 |-  ( ( 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 ) } ) ) ) )
392 246 390 391 syl2anc 
 |-  ( ( 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 ) } ) ) ) )
393 389 392 mpbird 
 |-  ( ( ph /\ x e. A ) -> ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) C_ ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) )
394 393 unissd 
 |-  ( ( 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 ) } ) ) )
395 imassrn 
 |-  ( ( 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 ) )
396 395 267 sstrid 
 |-  ( ( ph /\ x e. A ) -> ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ~P ( Base ` G ) )
397 sspwuni 
 |-  ( ( ( 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 ) )
398 396 397 sylib 
 |-  ( ( ph /\ x e. A ) -> U. ( ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) " ( ( A " { ( 1st ` x ) } ) \ { ( 2nd ` x ) } ) ) C_ ( Base ` G ) )
399 166 6 394 398 mrcssd 
 |-  ( ( 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 ) } ) ) ) )
400 ss2in 
 |-  ( ( ( 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 ) } ) ) ) ) )
401 345 399 400 syl2anc 
 |-  ( ( 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 ) } ) ) ) ) )
402 58 a1i 
 |-  ( ( ph /\ x e. A ) -> dom ( j e. ( A " { ( 1st ` x ) } ) |-> ( ( 1st ` x ) S j ) ) = ( A " { ( 1st ` x ) } ) )
403 53 402 69 8 6 dprddisj 
 |-  ( ( 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 ) } )
404 401 403 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
405 8 subg0cl 
 |-  ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
406 222 405 syl 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) )
407 333 406 elind 
 |-  ( ( ph /\ x e. A ) -> ( 0g ` G ) e. ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) )
408 407 snssd 
 |-  ( ( ph /\ x e. A ) -> { ( 0g ` G ) } C_ ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) )
409 404 408 eqssd 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) ) = { ( 0g ` G ) } )
410 340 409 eqtrid 
 |-  ( ( ph /\ x e. A ) -> ( ( K ` U. ( S " ( ( A |` { ( 1st ` x ) } ) \ { x } ) ) ) i^i ( S ` x ) ) = { ( 0g ` G ) } )
411 225 222 310 224 8 339 410 lsmdisj2 
 |-  ( ( 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 ) } )
412 309 411 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( S ` x ) i^i ( K ` U. ( S " ( A \ { x } ) ) ) ) C_ { ( 0g ` G ) } )
413 7 8 6 10 41 2 162 412 dmdprdd 
 |-  ( ph -> G dom DProd S )