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

Theorem dprd2da 15555
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 2404 . 2  |-  (Cntz `  G )  =  (Cntz `  G )
2 eqid 2404 . 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 15518 . . 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 5125 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  U_ i  e.  I  ( A  |`  { i } )
8 iunid 4106 . . . . . 6  |-  U_ i  e.  I  { i }  =  I
98reseq2i 5102 . . . . 5  |-  ( A  |`  U_ i  e.  I  { i } )  =  ( A  |`  I )
107, 9eqtr3i 2426 . . . 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 5142 . . . . 5  |-  ( ( Rel  A  /\  dom  A 
C_  I )  -> 
( A  |`  I )  =  A )
1411, 12, 13syl2anc 643 . . . 4  |-  ( ph  ->  ( A  |`  I )  =  A )
1510, 14syl5eq 2448 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  =  A )
16 ovex 6065 . . . . . 6  |-  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) )  e.  _V
17 eqid 2404 . . . . . 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 5533 . . . . 5  |-  dom  (
i  e.  I  |->  ( G DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) ) )  =  I
19 reldmdprd 15513 . . . . . . 7  |-  Rel  dom DProd
2019brrelex2i 4878 . . . . . 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 5089 . . . . . 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 2489 . . . 4  |-  ( ph  ->  I  e.  _V )
24 ressn 5367 . . . . . 6  |-  ( A  |`  { i } )  =  ( { i }  X.  ( A
" { i } ) )
25 snex 4365 . . . . . . 7  |-  { i }  e.  _V
26 ovex 6065 . . . . . . . . 9  |-  ( i S j )  e. 
_V
27 eqid 2404 . . . . . . . . 9  |-  ( j  e.  ( A " { i } ) 
|->  ( i S j ) )  =  ( j  e.  ( A
" { i } )  |->  ( i S j ) )
2826, 27dmmpti 5533 . . . . . . . 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 4878 . . . . . . . . 9  |-  ( G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  e.  _V )
31 dmexg 5089 . . . . . . . . 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 2489 . . . . . . 7  |-  ( (
ph  /\  i  e.  I )  ->  ( A " { i } )  e.  _V )
34 xpexg 4948 . . . . . . 7  |-  ( ( { i }  e.  _V  /\  ( A " { i } )  e.  _V )  -> 
( { i }  X.  ( A " { i } ) )  e.  _V )
3525, 33, 34sylancr 645 . . . . . 6  |-  ( (
ph  /\  i  e.  I )  ->  ( { i }  X.  ( A " { i } ) )  e. 
_V )
3624, 35syl5eqel 2488 . . . . 5  |-  ( (
ph  /\  i  e.  I )  ->  ( A  |`  { i } )  e.  _V )
3736ralrimiva 2749 . . . 4  |-  ( ph  ->  A. i  e.  I 
( A  |`  { i } )  e.  _V )
38 iunexg 5946 . . . 4  |-  ( ( I  e.  _V  /\  A. i  e.  I  ( A  |`  { i } )  e.  _V )  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
3923, 37, 38syl2anc 643 . . 3  |-  ( ph  ->  U_ i  e.  I 
( A  |`  { i } )  e.  _V )
4015, 39eqeltrrd 2479 . 2  |-  ( ph  ->  A  e.  _V )
41 dprd2d.2 . 2  |-  ( ph  ->  S : A --> (SubGrp `  G ) )
4212adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  dom  A 
C_  I )
43 1stdm 6353 . . . . . . . . . 10  |-  ( ( Rel  A  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4411, 43sylan 458 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e. 
dom  A )
4542, 44sseldd 3309 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x )  e.  I )
4629ralrimiva 2749 . . . . . . . . 9  |-  ( ph  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A " {
i } )  |->  ( i S j ) ) )
4746adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  A. i  e.  I  G dom DProd  ( j  e.  ( A
" { i } )  |->  ( i S j ) ) )
48 sneq 3785 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  x
)  ->  { i }  =  { ( 1st `  x ) } )
4948imaeq2d 5162 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( A " { i } )  =  ( A " { ( 1st `  x
) } ) )
50 oveq1 6047 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  x
)  ->  ( i S j )  =  ( ( 1st `  x
) S j ) )
5149, 50mpteq12dv 4247 . . . . . . . . . 10  |-  ( i  =  ( 1st `  x
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5251breq2d 4184 . . . . . . . . 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 3008 . . . . . . . 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 58 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  G dom DProd  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) )
55543ad2antr1 1122 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
5655adantr 452 . . . . 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 6065 . . . . . . 7  |-  ( ( 1st `  x ) S j )  e. 
_V
58 eqid 2404 . . . . . . 7  |-  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )  =  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) )
5957, 58dmmpti 5533 . . . . . 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 6352 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
6211, 61sylan 458 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  =  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
63 simpr 448 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
6462, 63eqeltrrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  <. ( 1st `  x ) ,  ( 2nd `  x
) >.  e.  A )
65 df-br 4173 . . . . . . . . 9  |-  ( ( 1st `  x ) A ( 2nd `  x
)  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  A
)
6664, 65sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( 1st `  x ) A ( 2nd `  x
) )
6711adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  Rel  A )
68 elrelimasn 5187 . . . . . . . . 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 224 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( 2nd `  x )  e.  ( A " {
( 1st `  x
) } ) )
71703ad2antr1 1122 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7271adantr 452 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  e.  ( A
" { ( 1st `  x ) } ) )
7311adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  Rel  A )
74 simpr2 964 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  e.  A )
75 1st2nd 6352 . . . . . . . . . . 11  |-  ( ( Rel  A  /\  y  e.  A )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
7673, 74, 75syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
y  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
7776, 74eqeltrrd 2479 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
78 df-br 4173 . . . . . . . . 9  |-  ( ( 1st `  y ) A ( 2nd `  y
)  <->  <. ( 1st `  y
) ,  ( 2nd `  y ) >.  e.  A
)
7977, 78sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
) A ( 2nd `  y ) )
80 elrelimasn 5187 . . . . . . . . 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 224 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
8382adantr 452 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  y ) } ) )
84 simpr 448 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 1st `  x
)  =  ( 1st `  y ) )
8584sneqd 3787 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  { ( 1st `  x
) }  =  {
( 1st `  y
) } )
8685imaeq2d 5162 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( A " {
( 1st `  x
) } )  =  ( A " {
( 1st `  y
) } ) )
8783, 86eleqtrrd 2481 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  y
)  e.  ( A
" { ( 1st `  x ) } ) )
88 simplr3 1001 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  ->  x  =/=  y )
89 simpr1 963 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  e.  A )
9073, 89, 61syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
9190, 76eqeq12d 2418 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. ) )
92 fvex 5701 . . . . . . . . . 10  |-  ( 1st `  x )  e.  _V
93 fvex 5701 . . . . . . . . . 10  |-  ( 2nd `  x )  e.  _V
9492, 93opth 4395 . . . . . . . . 9  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  =  <. ( 1st `  y ) ,  ( 2nd `  y
) >. 
<->  ( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) )
9591, 94syl6bb 253 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( x  =  y  <-> 
( ( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x )  =  ( 2nd `  y
) ) ) )
9695baibd 876 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =  y  <-> 
( 2nd `  x
)  =  ( 2nd `  y ) ) )
9796necon3bid 2602 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( x  =/=  y  <->  ( 2nd `  x )  =/=  ( 2nd `  y
) ) )
9888, 97mpbid 202 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( 2nd `  x
)  =/=  ( 2nd `  y ) )
9956, 60, 72, 87, 98, 1dprdcntz 15521 . . . 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 6043 . . . . . 6  |-  ( ( 1st `  x ) S ( 2nd `  x
) )  =  ( S `  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
101 oveq2 6048 . . . . . . . 8  |-  ( j  =  ( 2nd `  x
)  ->  ( ( 1st `  x ) S j )  =  ( ( 1st `  x
) S ( 2nd `  x ) ) )
102101, 58, 57fvmpt3i 5768 . . . . . . 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 5691 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  =  ( S `
 <. ( 1st `  x
) ,  ( 2nd `  x ) >. )
)
105100, 103, 1043eqtr4a 2462 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) `  ( 2nd `  x ) )  =  ( S `  x
) )
106105adantr 452 . . . 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 6055 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =  ( 1st `  y ) )  -> 
( ( 1st `  x
) S j )  =  ( ( 1st `  y ) S j ) )
10886, 107mpteq12dv 4247 . . . . . . 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 5689 . . . . . 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 6043 . . . . . . . 8  |-  ( ( 1st `  y ) S ( 2nd `  y
) )  =  ( S `  <. ( 1st `  y ) ,  ( 2nd `  y
) >. )
111 oveq2 6048 . . . . . . . . . 10  |-  ( j  =  ( 2nd `  y
)  ->  ( ( 1st `  y ) S j )  =  ( ( 1st `  y
) S ( 2nd `  y ) ) )
112 eqid 2404 . . . . . . . . . 10  |-  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) )
113 ovex 6065 . . . . . . . . . 10  |-  ( ( 1st `  y ) S j )  e. 
_V
114111, 112, 113fvmpt3i 5768 . . . . . . . . 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 5691 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  y
)  =  ( S `
 <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
)
117110, 115, 1163eqtr4a 2462 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) `  ( 2nd `  y ) )  =  ( S `  y
) )
118117adantr 452 . . . . . 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 2436 . . . . 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 5691 . . . 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 3350 . . 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 15553 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( G DProd  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) ) )
12351oveq2d 6056 . . . . . . . . 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 5768 . . . . . . . 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 3345 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  C_  ( ( i  e.  I  |->  ( G DProd  (
j  e.  ( A
" { i } )  |->  ( i S j ) ) ) ) `  ( 1st `  x ) ) )
1271263ad2antr1 1122 . . . . 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 452 . . . 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 707 . . . . . 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 1122 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  x
)  e.  I )
132131adantr 452 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  e.  I )
13312adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  dom  A  C_  I )
134 1stdm 6353 . . . . . . . . 9  |-  ( ( Rel  A  /\  y  e.  A )  ->  ( 1st `  y )  e. 
dom  A )
13573, 74, 134syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  dom  A
)
136133, 135sseldd 3309 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( 1st `  y
)  e.  I )
137136adantr 452 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  y
)  e.  I )
138 simpr 448 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( 1st `  x
)  =/=  ( 1st `  y ) )
139129, 130, 132, 137, 138, 1dprdcntz 15521 . . . . 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 3785 . . . . . . . . . . . . 13  |-  ( i  =  ( 1st `  y
)  ->  { i }  =  { ( 1st `  y ) } )
141140imaeq2d 5162 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( A " { i } )  =  ( A " { ( 1st `  y
) } ) )
142 oveq1 6047 . . . . . . . . . . . 12  |-  ( i  =  ( 1st `  y
)  ->  ( i S j )  =  ( ( 1st `  y
) S j ) )
143141, 142mpteq12dv 4247 . . . . . . . . . . 11  |-  ( i  =  ( 1st `  y
)  ->  ( j  e.  ( A " {
i } )  |->  ( i S j ) )  =  ( j  e.  ( A " { ( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
144143oveq2d 6056 . . . . . . . . . 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 5768 . . . . . . . . 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 5691 . . . . . . 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 2404 . . . . . . . . 9  |-  ( Base `  G )  =  (
Base `  G )
149148dprdssv 15529 . . . . . . . 8  |-  ( G DProd 
( j  e.  ( A " { ( 1st `  y ) } )  |->  ( ( 1st `  y ) S j ) ) )  C_  ( Base `  G )
15046adantr 452 . . . . . . . . . . 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 4184 . . . . . . . . . . . 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 3008 . . . . . . . . . . 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 58 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  ->  G dom DProd  ( j  e.  ( A " {
( 1st `  y
) } )  |->  ( ( 1st `  y
) S j ) ) )
154113, 112dmmpti 5533 . . . . . . . . . . 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 15538 . . . . . . . . 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 3343 . . . . . . . 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 15086 . . . . . . . 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 645 . . . . . . 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 3342 . . . . . 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 452 . . . . 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 3318 . . . 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 3318 . . 3  |-  ( ( ( ph  /\  (
x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  /\  ( 1st `  x
)  =/=  ( 1st `  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
164121, 163pm2.61dane 2645 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A  /\  x  =/=  y ) )  -> 
( S `  x
)  C_  ( (Cntz `  G ) `  ( S `  y )
) )
1656adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  G  e.  Grp )
166148subgacs 14930 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
167 acsmre 13832 . . . . . 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 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  A )
170 undif2 3664 . . . . . . . . . . . . . . . . . 18  |-  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) )  =  ( { ( 1st `  x
) }  u.  I
)
17145snssd 3903 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  { ( 1st `  x ) }  C_  I )
172 ssequn1 3477 . . . . . . . . . . . . . . . . . . 19  |-  ( { ( 1st `  x
) }  C_  I  <->  ( { ( 1st `  x
) }  u.  I
)  =  I )
173171, 172sylib 189 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  u.  I
)  =  I )
174170, 173syl5req 2449 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  I  =  ( { ( 1st `  x ) }  u.  ( I 
\  { ( 1st `  x ) } ) ) )
175174reseq2d 5105 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  I )  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
176169, 175eqtr3d 2438 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( A  |`  ( { ( 1st `  x
) }  u.  (
I  \  { ( 1st `  x ) } ) ) ) )
177 resundi 5119 . . . . . . . . . . . . . . 15  |-  ( A  |`  ( { ( 1st `  x ) }  u.  ( I  \  { ( 1st `  x ) } ) ) )  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
178176, 177syl6eq 2452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  A  =  ( ( A  |`  { ( 1st `  x
) } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
179178difeq1d 3424 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } ) )
180 difundir 3554 . . . . . . . . . . . . 13  |-  ( ( ( A  |`  { ( 1st `  x ) } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )  \  { x } )  =  ( ( ( A  |`  { ( 1st `  x
) } )  \  { x } )  u.  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
181179, 180syl6eq 2452 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( ( A  |`  ( I  \  { ( 1st `  x ) } ) )  \  { x } ) ) )
182 neirr 2572 . . . . . . . . . . . . . . . . 17  |-  -.  ( 1st `  x )  =/=  ( 1st `  x
)
18362eleq1d 2470 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  <->  <. ( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )
184 df-br 4173 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  <. ( 1st `  x ) ,  ( 2nd `  x )
>.  e.  ( A  |`  ( I  \  { ( 1st `  x ) } ) ) )
18593brres 5111 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  <->  ( ( 1st `  x ) A ( 2nd `  x
)  /\  ( 1st `  x )  e.  ( I  \  { ( 1st `  x ) } ) ) )
186185simprbi 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  x ) ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ( 2nd `  x )  ->  ( 1st `  x )  e.  ( I  \  {
( 1st `  x
) } ) )
187 eldifsni 3888 . . . . . . . . . . . . . . . . . . . 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 205 . . . . . . . . . . . . . . . . . 18  |-  ( <.
( 1st `  x
) ,  ( 2nd `  x ) >.  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) )
190183, 189syl6bi 220 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) )  ->  ( 1st `  x
)  =/=  ( 1st `  x ) ) )
191182, 190mtoi 171 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  -.  x  e.  ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )
192 disjsn 3828 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  -.  x  e.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) )
193191, 192sylibr 204 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) )
194 disj3 3632 . . . . . . . . . . . . . . 15  |-  ( ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  i^i  {
x } )  =  (/) 
<->  ( A  |`  (
I  \  { ( 1st `  x ) } ) )  =  ( ( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } ) )
195193, 194sylib 189 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  ( A  |`  ( I  \  { ( 1st `  x
) } ) )  =  ( ( A  |`  ( I  \  {
( 1st `  x
) } ) ) 
\  { x }
) )
196195eqcomd 2409 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( A  |`  (
I  \  { ( 1st `  x ) } ) )  \  {
x } )  =  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) )
197196uneq2d 3461 . . . . . . . . . . . 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 2436 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ( A  \  { x }
)  =  ( ( ( A  |`  { ( 1st `  x ) } )  \  {
x } )  u.  ( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
199198imaeq2d 5162 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
200 imaundi 5243 . . . . . . . . . 10  |-  ( S
" ( ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  u.  ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) )  =  ( ( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) )
201199, 200syl6eq 2452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  \  { x } ) )  =  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u.  ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
202201unieqd 3986 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  U. (
( S " (
( A  |`  { ( 1st `  x ) } )  \  {
x } ) )  u.  ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
203 uniun 3994 . . . . . . . 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 2452 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  \  { x } ) )  =  ( U. ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  u. 
U. ( S "
( A  |`  (
I  \  { ( 1st `  x ) } ) ) ) ) )
205 imassrn 5175 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  S
206 frn 5556 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  ran  S 
C_  (SubGrp `  G )
)
20741, 206syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  S  C_  (SubGrp `  G ) )
208207adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  (SubGrp `  G )
)
209 mresspw 13772 . . . . . . . . . . . . 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 3318 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  ran  S 
C_  ~P ( Base `  G
) )
212205, 211syl5ss 3319 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ~P ( Base `  G ) )
213 sspwuni 4136 . . . . . . . . . 10  |-  ( ( S " ( ( A  |`  { ( 1st `  x ) } )  \  { x } ) )  C_  ~P ( Base `  G
)  <->  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
214212, 213sylib 189 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( Base `  G ) )
215168, 3, 214mrcssidd 13805 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( K `  U. ( S "
( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) ) )
216 imassrn 5175 . . . . . . . . . . 11  |-  ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ran  S
217216, 211syl5ss 3319 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ~P ( Base `  G
) )
218 sspwuni 4136 . . . . . . . . . 10  |-  ( ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) )  C_  ~P ( Base `  G )  <->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
219217, 218sylib 189 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( Base `  G
) )
220168, 3, 219mrcssidd 13805 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  U. ( S " ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) 
C_  ( K `  U. ( S " ( A  |`  ( I  \  { ( 1st `  x
) } ) ) ) ) )
221 unss12 3479 . . . . . . . 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 643 . . . . . . 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 3342 . . . . . 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 13791 . . . . . . . 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 643 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  e.  (SubGrp `  G ) )
2263mrccl 13791 . . . . . . . 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 643 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( A  |`  ( I  \  { ( 1st `  x ) } ) ) ) )  e.  (SubGrp `  G ) )
228 eqid 2404 . . . . . . . 8  |-  ( LSSum `  G )  =  (
LSSum `  G )
229228lsmunss 15247 . . . . . . 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 643 . . . . . 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 3318 . . . . 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 3434 . . . . . . . . . . . . 13  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( A  |`  { ( 1st `  x ) } )
233 ressn 5367 . . . . . . . . . . . . 13  |-  ( A  |`  { ( 1st `  x
) } )  =  ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) )
234232, 233sseqtri 3340 . . . . . . . . . . . 12  |-  ( ( A  |`  { ( 1st `  x ) } )  \  { x } )  C_  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )
235 imass2 5199 . . . . . . . . . . . 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 8 . . . . . . . . . . 11  |-  ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ( S " ( { ( 1st `  x ) }  X.  ( A " { ( 1st `  x ) } ) ) )
237 ovex 6065 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) S i )  e. 
_V
238 oveq2 6048 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
( 1st `  x
) S j )  =  ( ( 1st `  x ) S i ) )
23958, 238elrnmpt1s 5077 . . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( A " { ( 1st `  x
) } )  -> 
( ( 1st `  x
) S i )  e.  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
241240rgen 2731 . . . . . . . . . . . . . 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 6047 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( 1st `  x
)  ->  ( y S i )  =  ( ( 1st `  x
) S i ) )
244243eleq1d 2470 . . . . . . . . . . . . . . 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 2686 . . . . . . . . . . . . . 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 3809 . . . . . . . . . . . . 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 204 . . . . . . . . . . . 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 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  S : A --> (SubGrp `  G )
)
249 ffun 5552 . . . . . . . . . . . . . 14  |-  ( S : A --> (SubGrp `  G )  ->  Fun  S )
250248, 249syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  Fun  S )
251 resss 5129 . . . . . . . . . . . . . . 15  |-  ( A  |`  { ( 1st `  x
) } )  C_  A
252233, 251eqsstr3i 3339 . . . . . . . . . . . . . 14  |-  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  A
253 fdm 5554 . . . . . . . . . . . . . . 15  |-  ( S : A --> (SubGrp `  G )  ->  dom  S  =  A )
254248, 253syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  dom  S  =  A )
255252, 254syl5sseqr 3357 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  ( { ( 1st `  x
) }  X.  ( A " { ( 1st `  x ) } ) )  C_  dom  S )
256 funimassov 6182 . . . . . . . . . . . . 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 643 . . . . . . . . . . . 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 224 . . . . . . . . . . 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 3319 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ( S " ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) )  C_  ran  ( j  e.  ( A " { ( 1st `  x
) } )  |->  ( ( 1st `  x
) S j ) ) )
260259unissd 3999 . . . . . . . . 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 6043 . . . . . . . . . . . . . 14  |-  ( ( 1st `  x ) S j )  =  ( S `  <. ( 1st `  x ) ,  j >. )
26241ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  S : A --> (SubGrp `  G ) )
263 elrelimasn 5187 . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( 1st `  x
) A j )
266 df-br 4173 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  x ) A j  <->  <. ( 1st `  x ) ,  j
>.  e.  A )
267265, 266sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  <. ( 1st `  x
) ,  j >.  e.  A )
268262, 267ffvelrnd 5830 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( S `  <. ( 1st `  x
) ,  j >.
)  e.  (SubGrp `  G ) )
269261, 268syl5eqel 2488 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  A )  /\  j  e.  ( A " {
( 1st `  x
) } ) )  ->  ( ( 1st `  x ) S j )  e.  (SubGrp `  G ) )
270269, 58fmptd 5852 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
j  e.  ( A
" { ( 1st `  x ) } ) 
|->  ( ( 1st `  x
) S j ) ) : ( A
" { ( 1st `  x ) } ) --> (SubGrp `  G )
)
271 frn 5556 . . . . . . . . . . . 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 3318 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ~P ( Base `  G
) )
274 sspwuni 4136 . . . . . . . . . 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 189 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  U. ran  ( j  e.  ( A " { ( 1st `  x ) } )  |->  ( ( 1st `  x ) S j ) ) 
C_  ( Base `  G
) )
276168, 3, 260, 275mrcssd 13804 . . . . . . . 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 15540 . . . . . . . . 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 3345 . . . . . . 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 5532 . . . . . . . . . . . . 13  |-  ( i  e.  I  |->  ( G DProd 
( j  e.  ( A " { i } )  |->  ( i S j ) ) ) )  Fn  I
281 fnressn 5877 . . . . . . . . . . . . 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 645 . . . . . . . . . . . 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 3951 . . . . . . . . . . . . 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 3787 . . . . . . . . . . . 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 2436 . . . . . . . . . . 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 6056 . . . . . . . . . 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 15537 . . . . . . . . . . . . 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 15549 . . . . . . . . . . . 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 643 . . . . . . . . . . 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 450 . . . . . . . . . 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 2436 . . . . . . . . 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 452 . . . . . . . . . 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 3434 . . . . . . . . . . 11  |-  ( I 
\  { ( 1st `  x ) } ) 
C_  I
296295a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
I  \  { ( 1st `  x ) } )  C_  I )
297 disjdif 3660 . . . . . . . . . . 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 15551 . . . . . . . . 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 3343 . . . . . . . 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 696 . . . . . . . . . . 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 15554 . . . . . . . . . 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 5150 . . . . . . . . . . . 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 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 ) ) ) )
305304oveq2i 6051 . . . . . . . . . 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 2454 . . . . . . . . 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 5691 . . . . . . . 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 3345 . . . . . . 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 3318 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( K `  U. ( S
" ( ( A  |`  { ( 1st `  x
) } )  \  { x } ) ) )  C_  (
(Cntz `  G ) `  ( K `  U. ( S " ( A  |`  ( I  \  {
( 1st `  x
) } ) ) ) ) ) )
310228, 1lsmsubg 15243 . . . . . 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 1184 . . . . 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 13800 . . . . 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 1184 . . . 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 3527 . . . 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 5829 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( S `  x )  e.  (SubGrp `  G )
)
317228lsmlub 15252 . . . . . . . . . 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 1184 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )