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

Theorem dprd2da 15605
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 2438 . 2  |-  (Cntz `  G )  =  (Cntz `  G )
2 eqid 2438 . 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 15568 . . 3  |-  ( G dom DProd  ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) )  ->  G  e.  Grp )
64, 5syl 16 . 2  |-  ( ph  ->  G  e.  Grp )
7 resiun2 5169 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  U_ i  e.  I  ( A  |`  { i } )
8 iunid 4148 . . . . . 6  |-  U_ i  e.  I  { i }  =  I
98reseq2i 5146 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  ( A  |`  I )
107, 9eqtr3i 2460 . . . 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 5186 . . . . 5  |-  ( ( Rel  A  /\  dom  A 
C_  I )  -> 
( A  |`  I )  =  A )
1411, 12, 13syl2anc 644 . . . 4  |-  ( ph  ->  ( A  |`  I )  =  A )
1510, 14syl5eq 2482 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  =  A )
16 ovex 6109 . . . . . 6  |-  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) )  e.  _V
17 eqid 2438 . . . . . 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 5577 . . . . 5  |-  dom  (
i  e.  I  |->  ( G DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) ) )  =  I
19 reldmdprd 15563 . . . . . . 7  |-  Rel  dom DProd
2019brrelex2i 4922 . . . . . 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 5133 . . . . . 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 19 . . . . 5  |-  ( ph  ->  dom  ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) )  e.  _V )
2318, 22syl5eqelr 2523 . . . 4  |-  ( ph  ->  I  e.  _V )
24 ressn 5411 . . . . . 6  |-  ( A  |`  { i } )  =  ( { i }  X.  ( A
" { i } ) )
25 snex 4408 . . . . . . 7  |-  { i }  e.  _V
26 ovex 6109 . . . . . . . . 9  |-  ( i S j )  e. 
_V
27 eqid 2438 . . . . . . . . 9  |-  ( j  e.  ( A " { i } ) 
|->  ( i S j ) )  =  ( j  e.  ( A
" { i } )  |->  ( i S j ) )
2826, 27dmmpti 5577 . . . . . . . 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 4922 . . . . . . . . 9  |-  ( G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  e.  _V )
31 dmexg 5133 . . . . . . . . 9  |-  ( ( j  e.  ( A
" { i } )  |->  ( i S j ) )  e. 
_V  ->  dom  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  e.  _V )
3229, 30, 313syl 19 . . . . . . . 8  |-  ( (
ph  /\  i  e.  I )  ->  dom  ( j  e.  ( A " { i } )  |->  ( i S j ) )  e.  _V )
3328, 32syl5eqelr 2523 . . . . . . 7  |-  ( (
ph  /\  i  e.  I )  ->  ( A " { i } )  e.  _V )
34 xpexg 4992 . . . . . . 7  |-  ( ( { i }  e.  _V  /\  ( A " { i } )  e.  _V )  -> 
( { i }  X.  ( A " { i } ) )  e.  _V )
3525, 33, 34sylancr 646 . . . . . 6  |-  ( (
ph  /\  i  e.  I )  ->  ( { i }  X.  ( A " { i } ) )  e. 
_V )
3624, 35syl5eqel 2522 . . . . 5  |-  ( (
ph  /\  i  e.  I )  ->  ( A  |`  { i } )  e.  _V )
3736ralrimiva 2791 . . . 4  |-  ( ph  ->  A. i  e.  I 
( A  |`  { i } )  e.  _V )
38 iunexg 5990 . . . 4  |-  ( ( I  e.  _V  /\  A. i  e.  I  ( A  |`  { i } )  e.  _V )  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
3923, 37, 38syl2anc 644 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
4015, 39eqeltrrd 2513 . 2  |-  ( ph  ->  A  e.  _V )
41 dprd2d.2 . 2  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
4212adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  dom  A 
C_  I )
43 1stdm 6397 . . . . . . . . . 10  |-  ( ( Rel  A  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4411, 43sylan 459 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4542, 44sseldd 3351 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e.  I )
4629ralrimiva 2791 . . . . . . . . 9  |-  ( ph  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) )
4746adantr 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A
" { i } )  |->  ( i S j ) ) )
48 sneq 3827 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  x
)  ->  { i }  =  { ( 1st `  x ) } )
4948imaeq2d 5206 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( A " { i } )  =  ( A " { ( 1st `  x
) } ) )
50 oveq1 6091 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( i S j )  =  ( ( 1st `  x
) S j ) )
5149, 50mpteq12dv 4290 . . . . . . . . . 10  |-  ( i  =  ( 1st `  x
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5251breq2d 4227 . . . . . . . . 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 3050 . . . . . . . 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 59 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  G dom DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )
55543ad2antr1 1123 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5655adantr 453 . . . . 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 6109 . . . . . . 7  |-  ( ( 1st `  x ) S j )  e. 
_V
58 eqid 2438 . . . . . . 7  |-  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )
5957, 58dmmpti 5577 . . . . . 6  |-  dom  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) )  =  ( A
" { ( 1st `  x ) } )
6059a1i 11 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  dom  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) )  =  ( A " { ( 1st `  x
) } ) )
61 1st2nd 6396 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
6211, 61sylan 459 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
63 simpr 449 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
6462, 63eqeltrrd 2513 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  <. ( 1st `  x ) ,  ( 2nd `  x
) >.  e.  A )
65 df-br 4216 . . . . . . . . 9  |-  ( ( 1st `  x ) A ( 2nd `  x
)  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  A
)
6664, 65sylibr 205 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x ) A ( 2nd `  x
) )
6711adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  Rel  A )
68 elrelimasn 5231 . . . . . . . . 9  |-  ( Rel 
A  ->  ( ( 2nd `  x )  e.  ( A " {
( 1st `  x
) } )  <->  ( 1st `  x ) A ( 2nd `  x ) ) )
6967, 68syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } )  <-> 
( 1st `  x
) A ( 2nd `  x ) ) )
7066, 69mpbird 225 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( 2nd `  x )  e.  ( A " {
( 1st `  x
) } ) )
71703ad2antr1 1123 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7271adantr 453 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7311adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  Rel  A )
74 simpr2 965 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  e.  A )
75 1st2nd 6396 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  y  e.  A )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
7673, 74, 75syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
7776, 74eqeltrrd 2513 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
78 df-br 4216 . . . . . . . . 9  |-  ( ( 1st `  y ) A ( 2nd `  y
)  <->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
7977, 78sylibr 205 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
) A ( 2nd `  y ) )
80 elrelimasn 5231 . . . . . . . . 9  |-  ( Rel 
A  ->  ( ( 2nd `  y )  e.  ( A " {
( 1st `  y
) } )  <->  ( 1st `  y ) A ( 2nd `  y ) ) )
8173, 80syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } )  <-> 
( 1st `  y
) A ( 2nd `  y ) ) )
8279, 81mpbird 225 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
8382adantr 453 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
84 simpr 449 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 1st `  x
)  =  ( 1st `  y ) )
8584sneqd 3829 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  { ( 1st `  x
) }  =  {
( 1st `  y
) } )
8685imaeq2d 5206 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( A " {
( 1st `  x
) } )  =  ( A " {
( 1st `  y
) } ) )
8783, 86eleqtrrd 2515 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  x ) } ) )
88 simplr3 1002 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  x  =/=  y )
89 simpr1 964 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  e.  A )
9073, 89, 61syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
9190, 76eqeq12d 2452 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. ) )
92 fvex 5745 . . . . . . . . . 10  |-  ( 1st `  x )  e.  _V
93 fvex 5745 . . . . . . . . . 10  |-  ( 2nd `  x )  e.  _V
9492, 93opth 4438 . . . . . . . . 9  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. 
<->  ( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) )
9591, 94syl6bb 254 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <-> 
( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) ) )
9695baibd 877 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =  y  <-> 
( 2nd `  x
)  =  ( 2nd `  y ) ) )
9796necon3bid 2638 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =/=  y  <->  ( 2nd `  x )  =/=  ( 2nd `  y
) ) )
9888, 97mpbid 203 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  =/=  ( 2nd `  y ) )
9956, 60, 72, 87, 98, 1dprdcntz 15571 . . . 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 6087 . . . . . 6  |-  ( ( 1st `  x ) S ( 2nd `  x
) )  =  ( S `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
101 oveq2 6092 . . . . . . . 8  |-  ( j  =  ( 2nd `  x
)  ->  ( ( 1st `  x ) S j )  =  ( ( 1st `  x
) S ( 2nd `  x ) ) )
102101, 58, 57fvmpt3i 5812 . . . . . . 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 16 . . . . . 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 5735 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  =  ( S `
 <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
105100, 103, 1043eqtr4a 2496 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) `  ( 2nd `  x ) )  =  ( S `  x
) )
106105adantr 453 . . . 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 6099 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( ( 1st `  x
) S j )  =  ( ( 1st `  y ) S j ) )
10886, 107mpteq12dv 4290 . . . . . . 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 5733 . . . . . 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 6087 . . . . . . . 8  |-  ( ( 1st `  y ) S ( 2nd `  y
) )  =  ( S `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
111 oveq2 6092 . . . . . . . . . 10  |-  ( j  =  ( 2nd `  y
)  ->  ( ( 1st `  y ) S j )  =  ( ( 1st `  y
) S ( 2nd `  y ) ) )
112 eqid 2438 . . . . . . . . . 10  |-  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )
113 ovex 6109 . . . . . . . . . 10  |-  ( ( 1st `  y ) S j )  e. 
_V
114111, 112, 113fvmpt3i 5812 . . . . . . . . 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 16 . . . . . . . 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 5735 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  y
)  =  ( S `
 <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
)
117110, 115, 1163eqtr4a 2496 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) `  ( 2nd `  y ) )  =  ( S `  y
) )
118117adantr 453 . . . . . 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 2470 . . . . 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 5735 . . . 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 3392 . . 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 15603 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) ) )
12351oveq2d 6100 . . . . . . . . 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 5812 . . . . . . . 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 16 . . . . . . 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 3387 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) ) `  ( 1st `  x ) ) )
1271263ad2antr1 1123 . . . . 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 453 . . . 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 708 . . . . . 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 11 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  ->  dom  ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " { i } ) 
|->  ( i S j ) ) ) )  =  I )
131453ad2antr1 1123 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  x
)  e.  I )
132131adantr 453 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  e.  I )
13312adantr 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  dom  A  C_  I )
134 1stdm 6397 . . . . . . . . 9  |-  ( ( Rel  A  /\  y  e.  A )  ->  ( 1st `  y )  e. 
dom  A )
13573, 74, 134syl2anc 644 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  dom  A
)
136133, 135sseldd 3351 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  I )
137136adantr 453 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  y
)  e.  I )
138 simpr 449 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  =/=  ( 1st `  y ) )
139129, 130, 132, 137, 138, 1dprdcntz 15571 . . . . 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 3827 . . . . . . . . . . . . 13  |-  ( i  =  ( 1st `  y
)  ->  { i }  =  { ( 1st `  y ) } )
141140imaeq2d 5206 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( A " { i } )  =  ( A " { ( 1st `  y
) } ) )
142 oveq1 6091 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( i S j )  =  ( ( 1st `  y
) S j ) )
143141, 142mpteq12dv 4290 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  y
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
144143oveq2d 6100 . . . . . . . . . 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 5812 . . . . . . . . 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 16 . . . . . . . 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 5735 . . . . . . 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 2438 . . . . . . . . 9  |-  ( Base `  G )  =  (
Base `  G )
149148dprdssv 15579 . . . . . . . 8  |-  ( G DProd 
( j  e.  ( A " { ( 1st `  y ) } )  |->  ( ( 1st `  y ) S j ) ) )  C_  ( Base `  G )
15046adantr 453 . . . . . . . . . . 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 4227 . . . . . . . . . . . 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 3050 . . . . . . . . . . 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 59 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
154113, 112dmmpti 5577 . . . . . . . . . . 11  |-  dom  (
j  e.  ( A
" { ( 1st `  y ) } ) 
|->  ( ( 1st `  y
) S j ) )  =  ( A
" { ( 1st `  y ) } )
155154a1i 11 . . . . . . . . . 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 15588 . . . . . . . . 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 3385 . . . . . . . 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 15136 . . . . . . . 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 646 . . . . . . 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 3384 . . . . . 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 453 . . . . 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 3360 . . . 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 3360 . . 3  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
164121, 163pm2.61dane 2684 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
1656adantr 453 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  G  e.  Grp )
166148subgacs 14980 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
167 acsmre 13882 . . . . . 6  |-  ( (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
168165, 166, 1673syl 19 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
16914adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  A )
170 undif2 3706 . . . . . . . . . . . . . . . . . 18  |-  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) )  =  ( { ( 1st `  x
) }  u.  I
)
17145snssd 3945 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  { ( 1st `  x ) }  C_  I )
172 ssequn1 3519 . . . . . . . . . . . . . . . . . . 19  |-  ( { ( 1st `  x
) }  C_  I  <->  ( { ( 1st `  x
) }  u.  I
)  =  I )
173171, 172sylib 190 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  u.  I
)  =  I )
174170, 173syl5req 2483 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  I  =  ( { ( 1st `  x ) }  u.  ( I 
\  { ( 1st `  x ) } ) ) )
175174reseq2d 5149 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
176169, 175eqtr3d 2472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
177 resundi 5163 . . . . . . . . . . . . . . 15  |-  ( A  |`  ( { ( 1st `  x ) }  u.  ( I  \  { ( 1st `  x ) } ) ) )  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
178176, 177syl6eq 2486 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
179178difeq1d 3466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } ) )
180 difundir 3596 . . . . . . . . . . . . 13  |-  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } )  =  ( ( ( A  |`  { ( 1st `  x
) } )  \  { x } )  u.  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
181179, 180syl6eq 2486 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( ( A  |`  ( I  \  { ( 1st `  x ) } ) )  \  { x } ) ) )
182 neirr 2608 . . . . . . . . . . . . . . . . 17  |-  -.  ( 1st `  x )  =/=  ( 1st `  x
)
18362eleq1d 2504 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )
184 df-br 4216 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  <. ( 1st `  x ) ,  ( 2nd `  x )
>.  e.  ( A  |`  ( I  \  { ( 1st `  x ) } ) ) )
18593brres 5155 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  ( ( 1st `  x ) A ( 2nd `  x
)  /\  ( 1st `  x )  e.  ( I  \  { ( 1st `  x ) } ) ) )
186185simprbi 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  ->  ( 1st `  x )  e.  ( I  \  {
( 1st `  x
) } ) )
187 eldifsni 3930 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x )  e.  ( I  \  { ( 1st `  x
) } )  -> 
( 1st `  x
)  =/=  ( 1st `  x ) )
188186, 187syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  ->  ( 1st `  x )  =/=  ( 1st `  x
) )
189184, 188sylbir 206 . . . . . . . . . . . . . . . . . 18  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) )
190183, 189syl6bi 221 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) ) )
191182, 190mtoi 172 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  -.  x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )
192 disjsn 3870 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  -.  x  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )
193191, 192sylibr 205 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) )
194 disj3 3674 . . . . . . . . . . . . . . 15  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  ( A  |`  (
I  \  { ( 1st `  x ) } ) )  =  ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } ) )
195193, 194sylib 190 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  =  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
196195eqcomd 2443 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } )  =  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
197196uneq2d 3503 . . . . . . . . . . . 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 2470 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
199198imaeq2d 5206 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
200 imaundi 5287 . . . . . . . . . 10  |-  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )  =  ( ( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
201199, 200syl6eq 2486 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u.  ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
202201unieqd 4028 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  U. (
( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
203 uniun 4036 . . . . . . . 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 2486 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  ( U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u. 
U. ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
205 imassrn 5219 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  S
206 frn 5600 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  ran  S 
C_  (SubGrp `  G )
)
20741, 206syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  S  C_  (SubGrp `  G ) )
208207adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  (SubGrp `  G )
)
209 mresspw 13822 . . . . . . . . . . . . 13  |-  ( (SubGrp `  G )  e.  (Moore `  ( Base `  G
) )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
210168, 209syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
211208, 210sstrd 3360 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  ~P ( Base `  G
) )
212205, 211syl5ss 3361 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ~P ( Base `  G ) )
213 sspwuni 4179 . . . . . . . . . 10  |-  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  C_  ~P ( Base `  G
)  <->  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
214212, 213sylib 190 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
215168, 3, 214mrcssidd 13855 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( K `  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) )
216 imassrn 5219 . . . . . . . . . . 11  |-  ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ran  S
217216, 211syl5ss 3361 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ~P ( Base `  G
) )
218 sspwuni 4179 . . . . . . . . . 10  |-  ( ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )  C_  ~P ( Base `  G )  <->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
219217, 218sylib 190 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
220168, 3, 219mrcssidd 13855 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( K `  U. ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
221 unss12 3521 . . . . . . . 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 ) } ) ) ) ) ) )
222215, 220, 221syl2anc 644 . . . . . . 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 ) } ) ) ) ) ) )
223204, 222eqsstrd 3384 . . . . . 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 ) } ) ) ) ) ) )
2243mrccl 13841 . . . . . . . 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 ) )
225168, 214, 224syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  e.  (SubGrp `  G ) )
2263mrccl 13841 . . . . . . . 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 ) )
227168, 219, 226syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) )  e.  (SubGrp `  G ) )
228 eqid 2438 . . . . . . . 8  |-  ( LSSum `  G )  =  (
LSSum `  G )
229228lsmunss 15297 . . . . . . 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
) } ) ) ) ) ) )
230225, 227, 229syl2anc 644 . . . . . 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
) } ) ) ) ) ) )
231223, 230sstrd 3360 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  C_  ( ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) ( LSSum `  G ) ( K `
 U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) ) ) )
232 difss 3476 . . . . . . . . . . . . 13  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( A  |`  { ( 1st `  x ) } )
233 ressn 5411 . . . . . . . . . . . . 13  |-  ( A  |`  { ( 1st `  x
) } )  =  ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) )
234232, 233sseqtri 3382 . . . . . . . . . . . 12  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )
235 imass2 5243 . . . . . . . . . . . 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 ) } ) ) ) )
236234, 235ax-mp 5 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( S " ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) ) )
237 ovex 6109 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) S i )  e. 
_V
238 oveq2 6092 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
( 1st `  x
) S j )  =  ( ( 1st `  x ) S i ) )
23958, 238elrnmpt1s 5121 . . . . . . . . . . . . . . . 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 ) ) )
240237, 239mpan2 654 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( A " { ( 1st `  x
) } )  -> 
( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
241240rgen 2773 . . . . . . . . . . . . . 14  |-  A. i  e.  ( A " {
( 1st `  x
) } ) ( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )
242241a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  A. i  e.  ( A " {
( 1st `  x
) } ) ( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
243 oveq1 6091 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( 1st `  x
)  ->  ( y S i )  =  ( ( 1st `  x
) S i ) )
244243eleq1d 2504 . . . . . . . . . . . . . . 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 ) ) ) )
245244ralbidv 2727 . . . . . . . . . . . . . 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 ) ) ) )
24692, 245ralsn 3851 . . . . . . . . . . . . 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 ) ) )
247242, 246sylibr 205 . . . . . . . . . . . 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 ) ) )
24841adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  S : A --> (SubGrp `  G )
)
249 ffun 5596 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  Fun  S )
250248, 249syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  Fun  S )
251 resss 5173 . . . . . . . . . . . . . . 15  |-  ( A  |`  { ( 1st `  x
) } )  C_  A
252233, 251eqsstr3i 3381 . . . . . . . . . . . . . 14  |-  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  A
253 fdm 5598 . . . . . . . . . . . . . . 15  |-  ( S : A --> (SubGrp `  G )  ->  dom  S  =  A )
254248, 253syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  dom  S  =  A )
255252, 254syl5sseqr 3399 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  dom  S )
256 funimassov 6226 . . . . . . . . . . . . 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 ) ) ) )
257250, 255, 256syl2anc 644 . . . . . . . . . . . 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 ) ) ) )
258247, 257mpbird 225 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( { ( 1st `  x ) }  X.  ( A
" { ( 1st `  x ) } ) ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )
259236, 258syl5ss 3361 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
260259unissd 4041 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  U. ran  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) )
261 df-ov 6087 . . . . . . . . . . . . . 14  |-  ( ( 1st `  x ) S j )  =  ( S `  <. ( 1st `  x ) ,  j >. )
26241ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  S : A --> (SubGrp `  G ) )
263 elrelimasn 5231 . . . . . . . . . . . . . . . . . 18  |-  ( Rel 
A  ->  ( j  e.  ( A " {
( 1st `  x
) } )  <->  ( 1st `  x ) A j ) )
26467, 263syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
j  e.  ( A
" { ( 1st `  x ) } )  <-> 
( 1st `  x
) A j ) )
265264biimpa 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( 1st `  x
) A j )
266 df-br 4216 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) A j  <->  <. ( 1st `  x ) ,  j
>.  e.  A )
267265, 266sylib 190 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  <. ( 1st `  x
) ,  j >.  e.  A )
268262, 267ffvelrnd 5874 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( S `  <. ( 1st `  x
) ,  j >.
)  e.  (SubGrp `  G ) )
269261, 268syl5eqel 2522 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( ( 1st `  x ) S j )  e.  (SubGrp `  G ) )
270269, 58fmptd 5896 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) : ( A
" { ( 1st `  x ) } ) --> (SubGrp `  G )
)
271 frn 5600 . . . . . . . . . . . 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
) )
272270, 271syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  (SubGrp `  G )
)
273272, 210sstrd 3360 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ~P ( Base `  G
) )
274 sspwuni 4179 . . . . . . . . . 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 ) )
275273, 274sylib 190 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ( Base `  G
) )
276168, 3, 260, 275mrcssd 13854 . . . . . . . 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 ) ) ) )
2773dprdspan 15590 . . . . . . . . 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 ) ) ) )
27854, 277syl 16 . . . . . . . 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 ) ) ) )
279276, 278sseqtr4d 3387 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) ) )
28016, 17fnmpti 5576 . . . . . . . . . . . . 13  |-  ( i  e.  I  |->  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) ) )  Fn  I
281 fnressn 5921 . . . . . . . . . . . . 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 ) ) >. } )
282280, 45, 281sylancr 646 . . . . . . . . . . . 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 ) ) >. } )
283125opeq2d 3993 . . . . . . . . . . . . 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 ) ) ) >. )
284283sneqd 3829 . . . . . . . . . . . 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 ) ) ) >. } )
285282, 284eqtrd 2470 . . . . . . . . . . 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 ) ) ) >. } )
286285oveq2d 6100 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( G DProd  ( ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) )  |`  { ( 1st `  x ) } ) )  =  ( G DProd  { <. ( 1st `  x
) ,  ( G DProd 
( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) ) >. } ) )
287 dprdsubg 15587 . . . . . . . . . . . . 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 ) )
28854, 287syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )  e.  (SubGrp `  G ) )
289 dprdsn 15599 . . . . . . . . . . . 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 ) ) ) ) )
29045, 288, 289syl2anc 644 . . . . . . . . . . 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 ) ) ) ) )
291290simprd 451 . . . . . . . . . 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 ) ) ) )
292286, 291eqtrd 2470 . . . . . . . . 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 ) ) ) )
2934adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  G dom DProd  ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " { i } ) 
|->  ( i S j ) ) ) ) )
29418a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  dom  ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " { i } ) 
|->  ( i S j ) ) ) )  =  I )
295 difss 3476 . . . . . . . . . . 11  |-  ( I 
\  { ( 1st `  x ) } ) 
C_  I
296295a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
I  \  { ( 1st `  x ) } )  C_  I )
297 disjdif 3702 . . . . . . . . . . 11  |-  ( { ( 1st `  x
) }  i^i  (
I  \  { ( 1st `  x ) } ) )  =  (/)
298297a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  i^i  (
I  \  { ( 1st `  x ) } ) )  =  (/) )
299293, 294, 171, 296, 298, 1dprdcntz2 15601 . . . . . . . . 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 ) } ) ) ) ) )
300292, 299eqsstr3d 3385 . . . . . . . 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
) } ) ) ) ) )
30129adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  i  e.  I )  ->  G dom DProd  ( j  e.  ( A " { i } )  |->  ( i S j ) ) )
30267, 248, 42, 301, 293, 3, 296dprd2dlem1 15604 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) )  =  ( G DProd 
( i  e.  ( I  \  { ( 1st `  x ) } )  |->  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) ) ) ) )
303 resmpt 5194 . . . . . . . . . . . 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 ) ) ) ) )
304295, 303ax-mp 5 . . . . . . . . . . 11  |-  ( ( i  e.  I  |->  ( G DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) ) )  |`  ( I  \  { ( 1st `  x ) } ) )  =  ( i  e.  ( I  \  { ( 1st `  x ) } )  |->  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) ) )
305304oveq2i 6095 . . . . . . . . . 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 ) ) ) ) )
306302, 305syl6eqr 2488 . . . . . . . . 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
) } ) ) ) )
307306fveq2d 5735 . . . . . . . 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
) } ) ) ) ) )
308300, 307sseqtr4d 3387 . . . . . . 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 ) } ) ) ) ) ) )
309279, 308sstrd 3360 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  (
(Cntz `  G ) `  ( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) ) )
310228, 1lsmsubg 15293 . . . . . 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 ) )
311225, 227, 309, 310syl3anc 1185 . . . . 5  |-  ( (
ph  /\  x  e.  A )  ->  (
( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) ) ( LSSum `  G )
( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) )  e.  (SubGrp `  G )
)
3123mrcsscl 13850 . . . . 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 ) } ) ) ) ) ) )
313168, 231, 311, 312syl3anc 1185 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  \  { x } ) ) )  C_  (
( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) ) ( LSSum `  G )
( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) ) )
314 sslin 3569 . . . 4  |-  ( ( K `  U. ( S " ( A  \  { x } ) ) )  C_  (
( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) ) ( LSSum `  G )
( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) )  -> 
( ( S `  x )  i^i  ( K `  U. ( S
" ( A  \  { x } ) ) ) )  C_  ( ( S `  x )  i^i  (
( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) ) ( LSSum `  G )
( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) ) ) )
315313, 314syl 16 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
( S `  x
)  i^i  ( K `  U. ( S "
( A  \  {
x } ) ) ) )  C_  (
( S `  x
)  i^i  ( ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) ( LSSum `  G ) ( K `
 U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) ) ) ) )
31641ffvelrnda 5873 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  e.  (SubGrp `  G )
)
317228lsmlub 15302 . . . . . . . . . 10  |-  ( ( ( K `  U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) ) )  e.  (SubGrp `  G
)  /\  ( S `  x )  e.  (SubGrp `  G )  /\  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )  e.  (SubGrp `  G ) )  -> 
( ( ( K `
 U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )  /\  ( S `
 x )  C_  ( G DProd  ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) ) )  <->  ( ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) ( LSSum `  G ) ( S `
 x ) ) 
C_  ( G DProd  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) ) ) )
318225, 316, 288, 317syl3anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A