MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprd2da Unicode version

Theorem dprd2da 15277
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.
StepHypRef Expression
1 eqid 2283 . 2  |-  (Cntz `  G )  =  (Cntz `  G )
2 eqid 2283 . 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 15240 . . 3  |-  ( G dom DProd  ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) )  ->  G  e.  Grp )
64, 5syl 15 . 2  |-  ( ph  ->  G  e.  Grp )
7 resiun2 4975 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  U_ i  e.  I  ( A  |`  { i } )
8 iunid 3957 . . . . . 6  |-  U_ i  e.  I  { i }  =  I
98reseq2i 4952 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  ( A  |`  I )
107, 9eqtr3i 2305 . . . 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 4992 . . . . 5  |-  ( ( Rel  A  /\  dom  A 
C_  I )  -> 
( A  |`  I )  =  A )
1411, 12, 13syl2anc 642 . . . 4  |-  ( ph  ->  ( A  |`  I )  =  A )
1510, 14syl5eq 2327 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  =  A )
16 ovex 5883 . . . . . 6  |-  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) )  e.  _V
17 eqid 2283 . . . . . 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 ) ) ) )
1816, 17dmmpti 5373 . . . . 5  |-  dom  (
i  e.  I  |->  ( G DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) ) )  =  I
19 reldmdprd 15235 . . . . . . 7  |-  Rel  dom DProd
2019brrelex2i 4730 . . . . . 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 4939 . . . . . 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 )
224, 20, 213syl 18 . . . . 5  |-  ( ph  ->  dom  ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) )  e.  _V )
2318, 22syl5eqelr 2368 . . . 4  |-  ( ph  ->  I  e.  _V )
24 ressn 5211 . . . . . 6  |-  ( A  |`  { i } )  =  ( { i }  X.  ( A
" { i } ) )
25 snex 4216 . . . . . . 7  |-  { i }  e.  _V
26 ovex 5883 . . . . . . . . 9  |-  ( i S j )  e. 
_V
27 eqid 2283 . . . . . . . . 9  |-  ( j  e.  ( A " { i } ) 
|->  ( i S j ) )  =  ( j  e.  ( A
" { i } )  |->  ( i S j ) )
2826, 27dmmpti 5373 . . . . . . . 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 ) ) )
3019brrelex2i 4730 . . . . . . . . 9  |-  ( G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  e.  _V )
31 dmexg 4939 . . . . . . . . 9  |-  ( ( j  e.  ( A
" { i } )  |->  ( i S j ) )  e. 
_V  ->  dom  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  e.  _V )
3229, 30, 313syl 18 . . . . . . . 8  |-  ( (
ph  /\  i  e.  I )  ->  dom  ( j  e.  ( A " { i } )  |->  ( i S j ) )  e.  _V )
3328, 32syl5eqelr 2368 . . . . . . 7  |-  ( (
ph  /\  i  e.  I )  ->  ( A " { i } )  e.  _V )
34 xpexg 4800 . . . . . . 7  |-  ( ( { i }  e.  _V  /\  ( A " { i } )  e.  _V )  -> 
( { i }  X.  ( A " { i } ) )  e.  _V )
3525, 33, 34sylancr 644 . . . . . 6  |-  ( (
ph  /\  i  e.  I )  ->  ( { i }  X.  ( A " { i } ) )  e. 
_V )
3624, 35syl5eqel 2367 . . . . 5  |-  ( (
ph  /\  i  e.  I )  ->  ( A  |`  { i } )  e.  _V )
3736ralrimiva 2626 . . . 4  |-  ( ph  ->  A. i  e.  I 
( A  |`  { i } )  e.  _V )
38 iunexg 5767 . . . 4  |-  ( ( I  e.  _V  /\  A. i  e.  I  ( A  |`  { i } )  e.  _V )  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
3923, 37, 38syl2anc 642 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
4015, 39eqeltrrd 2358 . 2  |-  ( ph  ->  A  e.  _V )
41 dprd2d.2 . 2  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
4212adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  dom  A 
C_  I )
43 1stdm 6167 . . . . . . . . . 10  |-  ( ( Rel  A  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4411, 43sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4542, 44sseldd 3181 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e.  I )
4629ralrimiva 2626 . . . . . . . . 9  |-  ( ph  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) )
4746adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A
" { i } )  |->  ( i S j ) ) )
48 sneq 3651 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  x
)  ->  { i }  =  { ( 1st `  x ) } )
4948imaeq2d 5012 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( A " { i } )  =  ( A " { ( 1st `  x
) } ) )
50 oveq1 5865 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( i S j )  =  ( ( 1st `  x
) S j ) )
5149, 50mpteq12dv 4098 . . . . . . . . . 10  |-  ( i  =  ( 1st `  x
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5251breq2d 4035 . . . . . . . . 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 ) ) ) )
5352rspcv 2880 . . . . . . . 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 ) ) ) )
5445, 47, 53sylc 56 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  G dom DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )
55543ad2antr1 1120 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5655adantr 451 . . . . 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 5883 . . . . . . 7  |-  ( ( 1st `  x ) S j )  e. 
_V
58 eqid 2283 . . . . . . 7  |-  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )
5957, 58dmmpti 5373 . . . . . 6  |-  dom  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) )  =  ( A
" { ( 1st `  x ) } )
6059a1i 10 . . . . 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 6166 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
6211, 61sylan 457 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
63 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
6462, 63eqeltrrd 2358 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  <. ( 1st `  x ) ,  ( 2nd `  x
) >.  e.  A )
65 df-br 4024 . . . . . . . . 9  |-  ( ( 1st `  x ) A ( 2nd `  x
)  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  A
)
6664, 65sylibr 203 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x ) A ( 2nd `  x
) )
6711adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  Rel  A )
68 elrelimasn 5037 . . . . . . . . 9  |-  ( Rel 
A  ->  ( ( 2nd `  x )  e.  ( A " {
( 1st `  x
) } )  <->  ( 1st `  x ) A ( 2nd `  x ) ) )
6967, 68syl 15 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } )  <-> 
( 1st `  x
) A ( 2nd `  x ) ) )
7066, 69mpbird 223 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( 2nd `  x )  e.  ( A " {
( 1st `  x
) } ) )
71703ad2antr1 1120 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7271adantr 451 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7311adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  Rel  A )
74 simpr2 962 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  e.  A )
75 1st2nd 6166 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  y  e.  A )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
7673, 74, 75syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
7776, 74eqeltrrd 2358 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
78 df-br 4024 . . . . . . . . 9  |-  ( ( 1st `  y ) A ( 2nd `  y
)  <->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
7977, 78sylibr 203 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
) A ( 2nd `  y ) )
80 elrelimasn 5037 . . . . . . . . 9  |-  ( Rel 
A  ->  ( ( 2nd `  y )  e.  ( A " {
( 1st `  y
) } )  <->  ( 1st `  y ) A ( 2nd `  y ) ) )
8173, 80syl 15 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } )  <-> 
( 1st `  y
) A ( 2nd `  y ) ) )
8279, 81mpbird 223 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
8382adantr 451 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
84 simpr 447 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 1st `  x
)  =  ( 1st `  y ) )
8584sneqd 3653 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  { ( 1st `  x
) }  =  {
( 1st `  y
) } )
8685imaeq2d 5012 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( A " {
( 1st `  x
) } )  =  ( A " {
( 1st `  y
) } ) )
8783, 86eleqtrrd 2360 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  x ) } ) )
88 simplr3 999 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  x  =/=  y )
89 simpr1 961 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  e.  A )
9073, 89, 61syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
9190, 76eqeq12d 2297 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. ) )
92 fvex 5539 . . . . . . . . . 10  |-  ( 1st `  x )  e.  _V
93 fvex 5539 . . . . . . . . . 10  |-  ( 2nd `  x )  e.  _V
9492, 93opth 4245 . . . . . . . . 9  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. 
<->  ( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) )
9591, 94syl6bb 252 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <-> 
( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) ) )
9695baibd 875 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =  y  <-> 
( 2nd `  x
)  =  ( 2nd `  y ) ) )
9796necon3bid 2481 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =/=  y  <->  ( 2nd `  x )  =/=  ( 2nd `  y
) ) )
9888, 97mpbid 201 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  =/=  ( 2nd `  y ) )
9956, 60, 72, 87, 98, 1dprdcntz 15243 . . . 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 5861 . . . . . 6  |-  ( ( 1st `  x ) S ( 2nd `  x
) )  =  ( S `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
101 oveq2 5866 . . . . . . . 8  |-  ( j  =  ( 2nd `  x
)  ->  ( ( 1st `  x ) S j )  =  ( ( 1st `  x
) S ( 2nd `  x ) ) )
102101, 58, 57fvmpt3i 5605 . . . . . . 7  |-  ( ( 2nd `  x )  e.  ( A " { ( 1st `  x
) } )  -> 
( ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) `  ( 2nd `  x ) )  =  ( ( 1st `  x
) S ( 2nd `  x ) ) )
10371, 102syl 15 . . . . . 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 ) ) )
10490fveq2d 5529 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  =  ( S `
 <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
105100, 103, 1043eqtr4a 2341 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) `  ( 2nd `  x ) )  =  ( S `  x
) )
106105adantr 451 . . . 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
) )
10784oveq1d 5873 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( ( 1st `  x
) S j )  =  ( ( 1st `  y ) S j ) )
10886, 107mpteq12dv 4098 . . . . . . 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 ) ) )
109108fveq1d 5527 . . . . . 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 5861 . . . . . . . 8  |-  ( ( 1st `  y ) S ( 2nd `  y
) )  =  ( S `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
111 oveq2 5866 . . . . . . . . . 10  |-  ( j  =  ( 2nd `  y
)  ->  ( ( 1st `  y ) S j )  =  ( ( 1st `  y
) S ( 2nd `  y ) ) )
112 eqid 2283 . . . . . . . . . 10  |-  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )
113 ovex 5883 . . . . . . . . . 10  |-  ( ( 1st `  y ) S j )  e. 
_V
114111, 112, 113fvmpt3i 5605 . . . . . . . . 9  |-  ( ( 2nd `  y )  e.  ( A " { ( 1st `  y
) } )  -> 
( ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) `  ( 2nd `  y ) )  =  ( ( 1st `  y
) S ( 2nd `  y ) ) )
11582, 114syl 15 . . . . . . . 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 ) ) )
11676fveq2d 5529 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  y
)  =  ( S `
 <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
)
117110, 115, 1163eqtr4a 2341 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) `  ( 2nd `  y ) )  =  ( S `  y
) )
118117adantr 451 . . . . . 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
) )
119109, 118eqtrd 2315 . . . . 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
) )
120119fveq2d 5529 . . . 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 )
) )
12199, 106, 1203sstr3d 3220 . . 3  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
12211, 41, 12, 29, 4, 3dprd2dlem2 15275 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) ) )
12351oveq2d 5874 . . . . . . . . 9  |-  ( i  =  ( 1st `  x
)  ->  ( G DProd  ( j  e.  ( A
" { i } )  |->  ( i S j ) ) )  =  ( G DProd  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) ) )
124123, 17, 16fvmpt3i 5605 . . . . . . . 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 ) ) ) )
12545, 124syl 15 . . . . . . 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 ) ) ) )
126122, 125sseqtr4d 3215 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) ) `  ( 1st `  x ) ) )
1271263ad2antr1 1120 . . . . 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 ) ) )
128127adantr 451 . . . 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 ) ) )
1294ad2antrr 706 . . . . . 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 ) ) ) ) )
13018a1i 10 . . . . . 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 )
131453ad2antr1 1120 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  x
)  e.  I )
132131adantr 451 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  e.  I )
13312adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  dom  A  C_  I )
134 1stdm 6167 . . . . . . . . 9  |-  ( ( Rel  A  /\  y  e.  A )  ->  ( 1st `  y )  e. 
dom  A )
13573, 74, 134syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  dom  A
)
136133, 135sseldd 3181 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  I )
137136adantr 451 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  y
)  e.  I )
138 simpr 447 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  =/=  ( 1st `  y ) )
139129, 130, 132, 137, 138, 1dprdcntz 15243 . . . . 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 3651 . . . . . . . . . . . . 13  |-  ( i  =  ( 1st `  y
)  ->  { i }  =  { ( 1st `  y ) } )
141140imaeq2d 5012 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( A " { i } )  =  ( A " { ( 1st `  y
) } ) )
142 oveq1 5865 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( i S j )  =  ( ( 1st `  y
) S j ) )
143141, 142mpteq12dv 4098 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  y
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
144143oveq2d 5874 . . . . . . . . . 10  |-  ( i  =  ( 1st `  y
)  ->  ( G DProd  ( j  e.  ( A
" { i } )  |->  ( i S j ) ) )  =  ( G DProd  (
j  e.  ( A
" { ( 1st `  y ) } ) 
|->  ( ( 1st `  y
) S j ) ) ) )
145144, 17, 16fvmpt3i 5605 . . . . . . . . 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 ) ) ) )
146136, 145syl 15 . . . . . . . 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 ) ) ) )
147146fveq2d 5529 . . . . . . 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 2283 . . . . . . . . 9  |-  ( Base `  G )  =  (
Base `  G )
149148dprdssv 15251 . . . . . . . 8  |-  ( G DProd 
( j  e.  ( A " { ( 1st `  y ) } )  |->  ( ( 1st `  y ) S j ) ) )  C_  ( Base `  G )
15046adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) )
151143breq2d 4035 . . . . . . . . . . . 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 ) ) ) )
152151rspcv 2880 . . . . . . . . . . 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 ) ) ) )
153136, 150, 152sylc 56 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
154113, 112dmmpti 5373 . . . . . . . . . . 11  |-  dom  (
j  e.  ( A
" { ( 1st `  y ) } ) 
|->  ( ( 1st `  y
) S j ) )  =  ( A
" { ( 1st `  y ) } )
155154a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  dom  ( j  e.  ( A " { ( 1st `  y ) } )  |->  ( ( 1st `  y ) S j ) )  =  ( A " { ( 1st `  y
) } ) )
156153, 155, 82dprdub 15260 . . . . . . . . 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 ) ) ) )
157117, 156eqsstr3d 3213 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  y
)  C_  ( G DProd  ( j  e.  ( A
" { ( 1st `  y ) } ) 
|->  ( ( 1st `  y
) S j ) ) ) )
158148, 1cntz2ss 14808 . . . . . . . 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
) ) )
159149, 157, 158sylancr 644 . . . . . . 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
) ) )
160147, 159eqsstrd 3212 . . . . . 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
) ) )
161160adantr 451 . . . . 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
) ) )
162139, 161sstrd 3189 . . . 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
) ) )
163128, 162sstrd 3189 . . 3  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
164121, 163pm2.61dane 2524 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
1656adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  G  e.  Grp )
166148subgacs 14652 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
167 acsmre 13554 . . . . . 6  |-  ( (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
168165, 166, 1673syl 18 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
16914adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  A )
170 undif2 3530 . . . . . . . . . . . . . . . . . 18  |-  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) )  =  ( { ( 1st `  x
) }  u.  I
)
17145snssd 3760 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  { ( 1st `  x ) }  C_  I )
172 ssequn1 3345 . . . . . . . . . . . . . . . . . . 19  |-  ( { ( 1st `  x
) }  C_  I  <->  ( { ( 1st `  x
) }  u.  I
)  =  I )
173171, 172sylib 188 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  u.  I
)  =  I )
174170, 173syl5req 2328 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  I  =  ( { ( 1st `  x ) }  u.  ( I 
\  { ( 1st `  x ) } ) ) )
175174reseq2d 4955 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
176169, 175eqtr3d 2317 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
177 resundi 4969 . . . . . . . . . . . . . . 15  |-  ( A  |`  ( { ( 1st `  x ) }  u.  ( I  \  { ( 1st `  x ) } ) ) )  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
178176, 177syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
179178difeq1d 3293 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } ) )
180 difundir 3422 . . . . . . . . . . . . 13  |-  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } )  =  ( ( ( A  |`  { ( 1st `  x
) } )  \  { x } )  u.  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
181179, 180syl6eq 2331 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( ( A  |`  ( I  \  { ( 1st `  x ) } ) )  \  { x } ) ) )
182 neirr 2451 . . . . . . . . . . . . . . . . 17  |-  -.  ( 1st `  x )  =/=  ( 1st `  x
)
18362eleq1d 2349 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )
184 df-br 4024 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  <. ( 1st `  x ) ,  ( 2nd `  x )
>.  e.  ( A  |`  ( I  \  { ( 1st `  x ) } ) ) )
18593brres 4961 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  ( ( 1st `  x ) A ( 2nd `  x
)  /\  ( 1st `  x )  e.  ( I  \  { ( 1st `  x ) } ) ) )
186185simprbi 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  ->  ( 1st `  x )  e.  ( I  \  {
( 1st `  x
) } ) )
187 eldifsni 3750 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x )  e.  ( I  \  { ( 1st `  x
) } )  -> 
( 1st `  x
)  =/=  ( 1st `  x ) )
188186, 187syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  ->  ( 1st `  x )  =/=  ( 1st `  x
) )
189184, 188sylbir 204 . . . . . . . . . . . . . . . . . 18  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) )
190183, 189syl6bi 219 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) ) )
191182, 190mtoi 169 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  -.  x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )
192 disjsn 3693 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  -.  x  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )
193191, 192sylibr 203 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) )
194 disj3 3499 . . . . . . . . . . . . . . 15  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  ( A  |`  (
I  \  { ( 1st `  x ) } ) )  =  ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } ) )
195193, 194sylib 188 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  =  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
196195eqcomd 2288 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } )  =  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
197196uneq2d 3329 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( A  |`  { ( 1st `  x
) } )  \  { x } )  u.  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )  =  ( ( ( A  |`  { ( 1st `  x
) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) )
198181, 197eqtrd 2315 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
199198imaeq2d 5012 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
200 imaundi 5093 . . . . . . . . . 10  |-  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )  =  ( ( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
201199, 200syl6eq 2331 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u.  ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
202201unieqd 3838 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  U. (
( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
203 uniun 3846 . . . . . . . 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 ) } ) ) ) )
204202, 203syl6eq 2331 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  ( U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u. 
U. ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
205 imassrn 5025 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  S
206 frn 5395 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  ran  S 
C_  (SubGrp `  G )
)
20741, 206syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  S  C_  (SubGrp `  G ) )
208207adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  (SubGrp `  G )
)
209 mresspw 13494 . . . . . . . . . . . . 13  |-  ( (SubGrp `  G )  e.  (Moore `  ( Base `  G
) )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
210168, 209syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
211208, 210sstrd 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  ~P ( Base `  G
) )
212205, 211syl5ss 3190 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ~P ( Base `  G ) )
213 sspwuni 3987 . . . . . . . . . 10  |-  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  C_  ~P ( Base `  G
)  <->  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
214212, 213sylib 188 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
2153mrcssid 13519 . . . . . . . . 9  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) ) 
C_  ( Base `  G
) )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( K `  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) )
216168, 214, 215syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( K `  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) )
217 imassrn 5025 . . . . . . . . . . 11  |-  ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ran  S
218217, 211syl5ss 3190 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ~P ( Base `  G
) )
219 sspwuni 3987 . . . . . . . . . 10  |-  ( ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )  C_  ~P ( Base `  G )  <->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
220218, 219sylib 188 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
2213mrcssid 13519 . . . . . . . . 9  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  C_  ( Base `  G ) )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  C_  ( K `  U. ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
222168, 220, 221syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( K `  U. ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
223 unss12 3347 . . . . . . . 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 ) } ) ) ) ) ) )
224216, 222, 223syl2anc 642 . . . . . . 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 ) } ) ) ) ) ) )
225204, 224eqsstrd 3212 . . . . . 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 ) } ) ) ) ) ) )
2263mrccl 13513 . . . . . . . 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 ) )
227168, 214, 226syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  e.  (SubGrp `  G ) )
2283mrccl 13513 . . . . . . . 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 ) )
229168, 220, 228syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) )  e.  (SubGrp `  G ) )
230 eqid 2283 . . . . . . . 8  |-  ( LSSum `  G )  =  (
LSSum `  G )
231230lsmunss 14969 . . . . . . 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
) } ) ) ) ) ) )
232227, 229, 231syl2anc 642 . . . . . 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
) } ) ) ) ) ) )
233225, 232sstrd 3189 . . . . 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 ) } ) ) ) ) ) )
234 difss 3303 . . . . . . . . . . . . 13  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( A  |`  { ( 1st `  x ) } )
235 ressn 5211 . . . . . . . . . . . . 13  |-  ( A  |`  { ( 1st `  x
) } )  =  ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) )
236234, 235sseqtri 3210 . . . . . . . . . . . 12  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )
237 imass2 5049 . . . . . . . . . . . 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 ) } ) ) ) )
238236, 237ax-mp 8 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( S " ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) ) )
239 ovex 5883 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) S i )  e. 
_V
240 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
( 1st `  x
) S j )  =  ( ( 1st `  x ) S i ) )
24158, 240elrnmpt1s 4927 . . . . . . . . . . . . . . . 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 ) ) )
242239, 241mpan2 652 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( A " { ( 1st `  x
) } )  -> 
( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
243242rgen 2608 . . . . . . . . . . . . . 14  |-  A. i  e.  ( A " {
( 1st `  x
) } ) ( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )
244243a1i 10 . . . . . . . . . . . . 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 ) ) )
245 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( 1st `  x
)  ->  ( y S i )  =  ( ( 1st `  x
) S i ) )
246245eleq1d 2349 . . . . . . . . . . . . . . 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 ) ) ) )
247246ralbidv 2563 . . . . . . . . . . . . . 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 ) ) ) )
24892, 247ralsn 3674 . . . . . . . . . . . . 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 ) ) )
249244, 248sylibr 203 . . . . . . . . . . . 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 ) ) )
25041adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  S : A --> (SubGrp `  G )
)
251 ffun 5391 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  Fun  S )
252250, 251syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  Fun  S )
253 resss 4979 . . . . . . . . . . . . . . 15  |-  ( A  |`  { ( 1st `  x
) } )  C_  A
254235, 253eqsstr3i 3209 . . . . . . . . . . . . . 14  |-  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  A
255 fdm 5393 . . . . . . . . . . . . . . 15  |-  ( S : A --> (SubGrp `  G )  ->  dom  S  =  A )
256250, 255syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  dom  S  =  A )
257254, 256syl5sseqr 3227 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  dom  S )
258 funimassov 5997 . . . . . . . . . . . . 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 ) ) ) )
259252, 257, 258syl2anc 642 . . . . . . . . . . . 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 ) ) ) )
260249, 259mpbird 223 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( { ( 1st `  x ) }  X.  ( A
" { ( 1st `  x ) } ) ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )
261238, 260syl5ss 3190 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
262 uniss 3848 . . . . . . . . . 10  |-  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) )  ->  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  U. ran  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) )
263261, 262syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  U. ran  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) )
264 df-ov 5861 . . . . . . . . . . . . . 14  |-  ( ( 1st `  x ) S j )  =  ( S `  <. ( 1st `  x ) ,  j >. )
26541ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  S : A --> (SubGrp `  G ) )
266 elrelimasn 5037 . . . . . . . . . . . . . . . . . 18  |-  ( Rel 
A  ->  ( j  e.  ( A " {
( 1st `  x
) } )  <->  ( 1st `  x ) A j ) )
26767, 266syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
j  e.  ( A
" { ( 1st `  x ) } )  <-> 
( 1st `  x
) A j ) )
268267biimpa 470 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( 1st `  x
) A j )
269 df-br 4024 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) A j  <->  <. ( 1st `  x ) ,  j
>.  e.  A )
270268, 269sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  <. ( 1st `  x
) ,  j >.  e.  A )
271 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( S : A --> (SubGrp `  G )  /\  <. ( 1st `  x ) ,  j >.  e.  A
)  ->  ( S `  <. ( 1st `  x
) ,  j >.
)  e.  (SubGrp `  G ) )
272265, 270, 271syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( S `  <. ( 1st `  x
) ,  j >.
)  e.  (SubGrp `  G ) )
273264, 272syl5eqel 2367 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( ( 1st `  x ) S j )  e.  (SubGrp `  G ) )
274273, 58fmptd 5684 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) : ( A
" { ( 1st `  x ) } ) --> (SubGrp `  G )
)
275 frn 5395 . . . . . . . . . . . 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
) )
276274, 275syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  (SubGrp `  G )
)
277276, 210sstrd 3189 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ~P ( Base `  G
) )
278 sspwuni 3987 . . . . . . . . . 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 ) )
279277, 278sylib 188 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ( Base `  G
) )
2803mrcss 13518 . . . . . . . . 9  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) ) 
C_  U. ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )  /\  U. ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ( Base `  G
) )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  ( K `  U. ran  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) ) )
281168, 263, 279, 280syl3anc 1182 . . . . . . . 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 ) ) ) )
2823dprdspan 15262 . . . . . . . . 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 ) ) ) )
28354, 282syl 15 . . . . . . . 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 ) ) ) )
284281, 283sseqtr4d 3215 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) ) )
28516, 17fnmpti 5372 . . . . . . . . . . . . 13  |-  ( i  e.  I  |->  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) ) )  Fn  I
286 fnressn 5705 . . . . . . . . . . . . 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 ) ) >. } )
287285, 45, 286sylancr 644 . . . . . . . . . . . 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 ) ) >. } )
288125opeq2d 3803 . . . . . . . . . . . . 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 ) ) ) >. )
289288sneqd 3653 . . . . . . . . . . . 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 ) ) ) >. } )
290287, 289eqtrd 2315 . . . . . . . . . . 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 ) ) ) >. } )
291290oveq2d 5874 . . . . . . . . . 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 ) ) ) >. } ) )
292 dprdsubg 15259 . . . . . . . . . . . . 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 ) )
29354, 292syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )  e.  (SubGrp `  G ) )
294 dprdsn 15271 . . . . . . . . . . . 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 ) ) ) ) )
29545, 293, 294syl2anc 642 . . . . . . . . . . 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 ) ) ) ) )
296295simprd 449 . . . . . . . . . 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 ) ) ) )
297291, 296eqtrd 2315 . . . . . . . . 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 ) ) ) )
2984adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  G dom DProd  ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " { i } ) 
|->  ( i S j ) ) ) ) )
29918a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  dom  ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " { i } ) 
|->  ( i S j ) ) ) )  =  I )
300 difss 3303 . . . . . . . . . . 11  |-  ( I 
\  { ( 1st `  x ) } ) 
C_  I
301300a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
I  \  { ( 1st `  x ) } )  C_  I )
302 disjdif 3526 . . . . . . . . . . 11  |-  ( { ( 1st `  x
) }  i^i  (
I  \  { ( 1st `  x ) } ) )  =  (/)
303302a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  i^i  (
I  \  { ( 1st `  x ) } ) )  =  (/) )
304298, 299, 171, 301, 303, 1dprdcntz2 15273 . . . . . . . . 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 ) } ) ) ) ) )
305297, 304eqsstr3d 3213 . . . . . . . 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
) } ) ) ) ) )
30629adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  i  e.  I )  ->  G dom DProd  ( j  e.  ( A " { i } )  |->  ( i S j ) ) )
30767, 250, 42, 306, 298, 3, 301dprd2dlem1 15276 . . . . . . . . . 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 ) ) ) ) ) )
308 resmpt 5000 . . . . . . . . . . . 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 ) ) ) ) )
309300, 308ax-mp 8 . . . . . . . . . . 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 ) ) ) )
310309oveq2i 5869 . . . . . . . . . 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 ) ) ) ) )
311307, 310syl6eqr 2333 . . . . . . . . 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
) } ) ) ) )
312311fveq2d 5529 . . . . . . . 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
) } ) ) ) ) )
313305, 312sseqtr4d 3215 . . . . . . 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 ) } ) ) ) ) ) )
314284, 313sstrd 3189 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  (
(Cntz `  G ) `  ( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) ) )
315230, 1lsmsubg 14965 . . . . . 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 ) )
316227, 229, 314, 315syl3anc 1182 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) ) ( LSSum `  G )
( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) )  e.  (SubGrp `  G )
)
3173mrcsscl 13522 . . . . 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 ) } ) ) ) ) ) )
318168, 233, 316, 317syl3anc 1182 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  \  { x } ) ) )  C_  (
( K `  U. ( S