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

Theorem dmdprdsplit2lem 17678
Description: Lemma for dmdprdsplit 17680. (Contributed by Mario Carneiro, 26-Apr-2016.)
Hypotheses
Ref Expression
dprdsplit.2  |-  ( ph  ->  S : I --> (SubGrp `  G ) )
dprdsplit.i  |-  ( ph  ->  ( C  i^i  D
)  =  (/) )
dprdsplit.u  |-  ( ph  ->  I  =  ( C  u.  D ) )
dmdprdsplit.z  |-  Z  =  (Cntz `  G )
dmdprdsplit.0  |-  .0.  =  ( 0g `  G )
dmdprdsplit2.1  |-  ( ph  ->  G dom DProd  ( S  |`  C ) )
dmdprdsplit2.2  |-  ( ph  ->  G dom DProd  ( S  |`  D ) )
dmdprdsplit2.3  |-  ( ph  ->  ( G DProd  ( S  |`  C ) )  C_  ( Z `  ( G DProd 
( S  |`  D ) ) ) )
dmdprdsplit2.4  |-  ( ph  ->  ( ( G DProd  ( S  |`  C ) )  i^i  ( G DProd  ( S  |`  D ) ) )  =  {  .0.  } )
dmdprdsplit2lem.k  |-  K  =  (mrCls `  (SubGrp `  G
) )
Assertion
Ref Expression
dmdprdsplit2lem  |-  ( (
ph  /\  X  e.  C )  ->  (
( Y  e.  I  ->  ( X  =/=  Y  ->  ( S `  X
)  C_  ( Z `  ( S `  Y
) ) ) )  /\  ( ( S `
 X )  i^i  ( K `  U. ( S " ( I 
\  { X }
) ) ) ) 
C_  {  .0.  } ) )

Proof of Theorem dmdprdsplit2lem
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dprdsplit.u . . . . . 6  |-  ( ph  ->  I  =  ( C  u.  D ) )
21adantr 467 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  I  =  ( C  u.  D ) )
32eleq2d 2514 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( Y  e.  I  <->  Y  e.  ( C  u.  D
) ) )
4 elun 3574 . . . 4  |-  ( Y  e.  ( C  u.  D )  <->  ( Y  e.  C  \/  Y  e.  D ) )
53, 4syl6bb 265 . . 3  |-  ( (
ph  /\  X  e.  C )  ->  ( Y  e.  I  <->  ( Y  e.  C  \/  Y  e.  D ) ) )
6 dmdprdsplit2.1 . . . . . . . 8  |-  ( ph  ->  G dom DProd  ( S  |`  C ) )
76ad2antrr 732 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  G dom DProd  ( S  |`  C ) )
8 dprdsplit.2 . . . . . . . . . 10  |-  ( ph  ->  S : I --> (SubGrp `  G ) )
9 ssun1 3597 . . . . . . . . . . 11  |-  C  C_  ( C  u.  D
)
109, 1syl5sseqr 3481 . . . . . . . . . 10  |-  ( ph  ->  C  C_  I )
118, 10fssresd 5750 . . . . . . . . 9  |-  ( ph  ->  ( S  |`  C ) : C --> (SubGrp `  G ) )
12 fdm 5733 . . . . . . . . 9  |-  ( ( S  |`  C ) : C --> (SubGrp `  G )  ->  dom  ( S  |`  C )  =  C )
1311, 12syl 17 . . . . . . . 8  |-  ( ph  ->  dom  ( S  |`  C )  =  C )
1413ad2antrr 732 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  dom  ( S  |`  C )  =  C )
15 simplr 762 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  X  e.  C
)
16 simprl 764 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  Y  e.  C
)
17 simprr 766 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  X  =/=  Y
)
18 dmdprdsplit.z . . . . . . 7  |-  Z  =  (Cntz `  G )
197, 14, 15, 16, 17, 18dprdcntz 17640 . . . . . 6  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  ( ( S  |`  C ) `  X
)  C_  ( Z `  ( ( S  |`  C ) `  Y
) ) )
20 fvres 5879 . . . . . . 7  |-  ( X  e.  C  ->  (
( S  |`  C ) `
 X )  =  ( S `  X
) )
2120ad2antlr 733 . . . . . 6  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  ( ( S  |`  C ) `  X
)  =  ( S `
 X ) )
22 fvres 5879 . . . . . . . 8  |-  ( Y  e.  C  ->  (
( S  |`  C ) `
 Y )  =  ( S `  Y
) )
2322ad2antrl 734 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  ( ( S  |`  C ) `  Y
)  =  ( S `
 Y ) )
2423fveq2d 5869 . . . . . 6  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  ( Z `  ( ( S  |`  C ) `  Y
) )  =  ( Z `  ( S `
 Y ) ) )
2519, 21, 243sstr3d 3474 . . . . 5  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  C  /\  X  =/=  Y ) )  ->  ( S `  X )  C_  ( Z `  ( S `  Y ) ) )
2625exp32 610 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( Y  e.  C  ->  ( X  =/=  Y  -> 
( S `  X
)  C_  ( Z `  ( S `  Y
) ) ) ) )
2720ad2antlr 733 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( ( S  |`  C ) `  X
)  =  ( S `
 X ) )
286ad2antrr 732 . . . . . . . 8  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  G dom DProd  ( S  |`  C ) )
2913ad2antrr 732 . . . . . . . 8  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  dom  ( S  |`  C )  =  C )
30 simplr 762 . . . . . . . 8  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  X  e.  C
)
3128, 29, 30dprdub 17658 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( ( S  |`  C ) `  X
)  C_  ( G DProd  ( S  |`  C )
) )
3227, 31eqsstr3d 3467 . . . . . 6  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( S `  X )  C_  ( G DProd  ( S  |`  C ) ) )
33 dmdprdsplit2.3 . . . . . . . 8  |-  ( ph  ->  ( G DProd  ( S  |`  C ) )  C_  ( Z `  ( G DProd 
( S  |`  D ) ) ) )
3433ad2antrr 732 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( G DProd  ( S  |`  C ) ) 
C_  ( Z `  ( G DProd  ( S  |`  D ) ) ) )
35 eqid 2451 . . . . . . . . 9  |-  ( Base `  G )  =  (
Base `  G )
3635dprdssv 17649 . . . . . . . 8  |-  ( G DProd 
( S  |`  D ) )  C_  ( Base `  G )
37 fvres 5879 . . . . . . . . . 10  |-  ( Y  e.  D  ->  (
( S  |`  D ) `
 Y )  =  ( S `  Y
) )
3837ad2antrl 734 . . . . . . . . 9  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( ( S  |`  D ) `  Y
)  =  ( S `
 Y ) )
39 dmdprdsplit2.2 . . . . . . . . . . 11  |-  ( ph  ->  G dom DProd  ( S  |`  D ) )
4039ad2antrr 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  G dom DProd  ( S  |`  D ) )
41 ssun2 3598 . . . . . . . . . . . . . 14  |-  D  C_  ( C  u.  D
)
4241, 1syl5sseqr 3481 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  I )
438, 42fssresd 5750 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  |`  D ) : D --> (SubGrp `  G ) )
44 fdm 5733 . . . . . . . . . . . 12  |-  ( ( S  |`  D ) : D --> (SubGrp `  G )  ->  dom  ( S  |`  D )  =  D )
4543, 44syl 17 . . . . . . . . . . 11  |-  ( ph  ->  dom  ( S  |`  D )  =  D )
4645ad2antrr 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  dom  ( S  |`  D )  =  D )
47 simprl 764 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  Y  e.  D
)
4840, 46, 47dprdub 17658 . . . . . . . . 9  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( ( S  |`  D ) `  Y
)  C_  ( G DProd  ( S  |`  D )
) )
4938, 48eqsstr3d 3467 . . . . . . . 8  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( S `  Y )  C_  ( G DProd  ( S  |`  D ) ) )
5035, 18cntz2ss 16986 . . . . . . . 8  |-  ( ( ( G DProd  ( S  |`  D ) )  C_  ( Base `  G )  /\  ( S `  Y
)  C_  ( G DProd  ( S  |`  D )
) )  ->  ( Z `  ( G DProd  ( S  |`  D )
) )  C_  ( Z `  ( S `  Y ) ) )
5136, 49, 50sylancr 669 . . . . . . 7  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( Z `  ( G DProd  ( S  |`  D ) ) ) 
C_  ( Z `  ( S `  Y ) ) )
5234, 51sstrd 3442 . . . . . 6  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( G DProd  ( S  |`  C ) ) 
C_  ( Z `  ( S `  Y ) ) )
5332, 52sstrd 3442 . . . . 5  |-  ( ( ( ph  /\  X  e.  C )  /\  ( Y  e.  D  /\  X  =/=  Y ) )  ->  ( S `  X )  C_  ( Z `  ( S `  Y ) ) )
5453exp32 610 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( Y  e.  D  ->  ( X  =/=  Y  -> 
( S `  X
)  C_  ( Z `  ( S `  Y
) ) ) ) )
5526, 54jaod 382 . . 3  |-  ( (
ph  /\  X  e.  C )  ->  (
( Y  e.  C  \/  Y  e.  D
)  ->  ( X  =/=  Y  ->  ( S `  X )  C_  ( Z `  ( S `  Y ) ) ) ) )
565, 55sylbid 219 . 2  |-  ( (
ph  /\  X  e.  C )  ->  ( Y  e.  I  ->  ( X  =/=  Y  -> 
( S `  X
)  C_  ( Z `  ( S `  Y
) ) ) ) )
57 dprdgrp 17637 . . . . . . . 8  |-  ( G dom DProd  ( S  |`  C )  ->  G  e.  Grp )
586, 57syl 17 . . . . . . 7  |-  ( ph  ->  G  e.  Grp )
5958adantr 467 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  G  e.  Grp )
6035subgacs 16852 . . . . . 6  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
61 acsmre 15558 . . . . . 6  |-  ( (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
6259, 60, 613syl 18 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  (SubGrp `  G )  e.  (Moore `  ( Base `  G
) ) )
63 difundir 3696 . . . . . . . . . . 11  |-  ( ( C  u.  D ) 
\  { X }
)  =  ( ( C  \  { X } )  u.  ( D  \  { X }
) )
642difeq1d 3550 . . . . . . . . . . 11  |-  ( (
ph  /\  X  e.  C )  ->  (
I  \  { X } )  =  ( ( C  u.  D
)  \  { X } ) )
65 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  X  e.  C )  ->  X  e.  C )
6665snssd 4117 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  X  e.  C )  ->  { X }  C_  C )
67 sslin 3658 . . . . . . . . . . . . . . 15  |-  ( { X }  C_  C  ->  ( D  i^i  { X } )  C_  ( D  i^i  C ) )
6866, 67syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  X  e.  C )  ->  ( D  i^i  { X }
)  C_  ( D  i^i  C ) )
69 incom 3625 . . . . . . . . . . . . . . 15  |-  ( C  i^i  D )  =  ( D  i^i  C
)
70 dprdsplit.i . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  i^i  D
)  =  (/) )
7170adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  X  e.  C )  ->  ( C  i^i  D )  =  (/) )
7269, 71syl5eqr 2499 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  X  e.  C )  ->  ( D  i^i  C )  =  (/) )
73 sseq0 3766 . . . . . . . . . . . . . 14  |-  ( ( ( D  i^i  { X } )  C_  ( D  i^i  C )  /\  ( D  i^i  C )  =  (/) )  ->  ( D  i^i  { X }
)  =  (/) )
7468, 72, 73syl2anc 667 . . . . . . . . . . . . 13  |-  ( (
ph  /\  X  e.  C )  ->  ( D  i^i  { X }
)  =  (/) )
75 disj3 3809 . . . . . . . . . . . . 13  |-  ( ( D  i^i  { X } )  =  (/)  <->  D  =  ( D  \  { X } ) )
7674, 75sylib 200 . . . . . . . . . . . 12  |-  ( (
ph  /\  X  e.  C )  ->  D  =  ( D  \  { X } ) )
7776uneq2d 3588 . . . . . . . . . . 11  |-  ( (
ph  /\  X  e.  C )  ->  (
( C  \  { X } )  u.  D
)  =  ( ( C  \  { X } )  u.  ( D  \  { X }
) ) )
7863, 64, 773eqtr4a 2511 . . . . . . . . . 10  |-  ( (
ph  /\  X  e.  C )  ->  (
I  \  { X } )  =  ( ( C  \  { X } )  u.  D
) )
7978imaeq2d 5168 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  ( S " ( I  \  { X } ) )  =  ( S "
( ( C  \  { X } )  u.  D ) ) )
80 imaundi 5248 . . . . . . . . 9  |-  ( S
" ( ( C 
\  { X }
)  u.  D ) )  =  ( ( S " ( C 
\  { X }
) )  u.  ( S " D ) )
8179, 80syl6eq 2501 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( S " ( I  \  { X } ) )  =  ( ( S
" ( C  \  { X } ) )  u.  ( S " D ) ) )
8281unieqd 4208 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( I  \  { X } ) )  =  U. ( ( S " ( C 
\  { X }
) )  u.  ( S " D ) ) )
83 uniun 4217 . . . . . . 7  |-  U. (
( S " ( C  \  { X }
) )  u.  ( S " D ) )  =  ( U. ( S " ( C  \  { X } ) )  u.  U. ( S
" D ) )
8482, 83syl6eq 2501 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( I  \  { X } ) )  =  ( U. ( S " ( C  \  { X } ) )  u.  U. ( S
" D ) ) )
85 dmdprdsplit2lem.k . . . . . . . . 9  |-  K  =  (mrCls `  (SubGrp `  G
) )
86 difss 3560 . . . . . . . . . . 11  |-  ( C 
\  { X }
)  C_  C
87 imass2 5204 . . . . . . . . . . 11  |-  ( ( C  \  { X } )  C_  C  ->  ( S " ( C  \  { X }
) )  C_  ( S " C ) )
88 uniss 4219 . . . . . . . . . . 11  |-  ( ( S " ( C 
\  { X }
) )  C_  ( S " C )  ->  U. ( S " ( C  \  { X }
) )  C_  U. ( S " C ) )
8986, 87, 88mp2b 10 . . . . . . . . . 10  |-  U. ( S " ( C  \  { X } ) ) 
C_  U. ( S " C )
90 imassrn 5179 . . . . . . . . . . . 12  |-  ( S
" C )  C_  ran  S
91 frn 5735 . . . . . . . . . . . . . . 15  |-  ( S : I --> (SubGrp `  G )  ->  ran  S 
C_  (SubGrp `  G )
)
928, 91syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  S  C_  (SubGrp `  G ) )
9392adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  X  e.  C )  ->  ran  S 
C_  (SubGrp `  G )
)
94 mresspw 15498 . . . . . . . . . . . . . 14  |-  ( (SubGrp `  G )  e.  (Moore `  ( Base `  G
) )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
9562, 94syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  X  e.  C )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
9693, 95sstrd 3442 . . . . . . . . . . . 12  |-  ( (
ph  /\  X  e.  C )  ->  ran  S 
C_  ~P ( Base `  G
) )
9790, 96syl5ss 3443 . . . . . . . . . . 11  |-  ( (
ph  /\  X  e.  C )  ->  ( S " C )  C_  ~P ( Base `  G
) )
98 sspwuni 4367 . . . . . . . . . . 11  |-  ( ( S " C ) 
C_  ~P ( Base `  G
)  <->  U. ( S " C )  C_  ( Base `  G ) )
9997, 98sylib 200 . . . . . . . . . 10  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " C )  C_  ( Base `  G )
)
10089, 99syl5ss 3443 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( C  \  { X } ) ) 
C_  ( Base `  G
) )
10162, 85, 100mrcssidd 15531 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( C  \  { X } ) ) 
C_  ( K `  U. ( S " ( C  \  { X }
) ) ) )
102 imassrn 5179 . . . . . . . . . . . 12  |-  ( S
" D )  C_  ran  S
103102, 96syl5ss 3443 . . . . . . . . . . 11  |-  ( (
ph  /\  X  e.  C )  ->  ( S " D )  C_  ~P ( Base `  G
) )
104 sspwuni 4367 . . . . . . . . . . 11  |-  ( ( S " D ) 
C_  ~P ( Base `  G
)  <->  U. ( S " D )  C_  ( Base `  G ) )
105103, 104sylib 200 . . . . . . . . . 10  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " D )  C_  ( Base `  G )
)
10662, 85, 105mrcssidd 15531 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " D )  C_  ( K `  U. ( S " D ) ) )
10785dprdspan 17660 . . . . . . . . . . . 12  |-  ( G dom DProd  ( S  |`  D )  ->  ( G DProd  ( S  |`  D ) )  =  ( K `
 U. ran  ( S  |`  D ) ) )
10839, 107syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( G DProd  ( S  |`  D ) )  =  ( K `  U. ran  ( S  |`  D ) ) )
109 df-ima 4847 . . . . . . . . . . . . 13  |-  ( S
" D )  =  ran  ( S  |`  D )
110109unieqi 4207 . . . . . . . . . . . 12  |-  U. ( S " D )  = 
U. ran  ( S  |`  D )
111110fveq2i 5868 . . . . . . . . . . 11  |-  ( K `
 U. ( S
" D ) )  =  ( K `  U. ran  ( S  |`  D ) )
112108, 111syl6eqr 2503 . . . . . . . . . 10  |-  ( ph  ->  ( G DProd  ( S  |`  D ) )  =  ( K `  U. ( S " D ) ) )
113112adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  ( G DProd  ( S  |`  D ) )  =  ( K `
 U. ( S
" D ) ) )
114106, 113sseqtr4d 3469 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " D )  C_  ( G DProd  ( S  |`  D ) ) )
115 unss12 3606 . . . . . . . 8  |-  ( ( U. ( S "
( C  \  { X } ) )  C_  ( K `  U. ( S " ( C  \  { X } ) ) )  /\  U. ( S " D )  C_  ( G DProd  ( S  |`  D ) ) )  ->  ( U. ( S " ( C  \  { X } ) )  u.  U. ( S
" D ) ) 
C_  ( ( K `
 U. ( S
" ( C  \  { X } ) ) )  u.  ( G DProd 
( S  |`  D ) ) ) )
116101, 114, 115syl2anc 667 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  ( U. ( S " ( C  \  { X }
) )  u.  U. ( S " D ) )  C_  ( ( K `  U. ( S
" ( C  \  { X } ) ) )  u.  ( G DProd 
( S  |`  D ) ) ) )
11785mrccl 15517 . . . . . . . . 9  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " ( C  \  { X }
) )  C_  ( Base `  G ) )  ->  ( K `  U. ( S " ( C  \  { X }
) ) )  e.  (SubGrp `  G )
)
11862, 100, 117syl2anc 667 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  e.  (SubGrp `  G ) )
119 dprdsubg 17657 . . . . . . . . . 10  |-  ( G dom DProd  ( S  |`  D )  ->  ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G ) )
12039, 119syl 17 . . . . . . . . 9  |-  ( ph  ->  ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G )
)
121120adantr 467 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G ) )
122 eqid 2451 . . . . . . . . 9  |-  ( LSSum `  G )  =  (
LSSum `  G )
123122lsmunss 17310 . . . . . . . 8  |-  ( ( ( K `  U. ( S " ( C 
\  { X }
) ) )  e.  (SubGrp `  G )  /\  ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G )
)  ->  ( ( K `  U. ( S
" ( C  \  { X } ) ) )  u.  ( G DProd 
( S  |`  D ) ) )  C_  (
( K `  U. ( S " ( C 
\  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) ) )
124118, 121, 123syl2anc 667 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  (
( K `  U. ( S " ( C 
\  { X }
) ) )  u.  ( G DProd  ( S  |`  D ) ) ) 
C_  ( ( K `
 U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) ) )
125116, 124sstrd 3442 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  ( U. ( S " ( C  \  { X }
) )  u.  U. ( S " D ) )  C_  ( ( K `  U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) ) )
12684, 125eqsstrd 3466 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( I  \  { X } ) ) 
C_  ( ( K `
 U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) ) )
12789a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( C  \  { X } ) ) 
C_  U. ( S " C ) )
12862, 85, 127, 99mrcssd 15530 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  C_  ( K `  U. ( S " C ) ) )
12985dprdspan 17660 . . . . . . . . . . 11  |-  ( G dom DProd  ( S  |`  C )  ->  ( G DProd  ( S  |`  C ) )  =  ( K `
 U. ran  ( S  |`  C ) ) )
1306, 129syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( G DProd  ( S  |`  C ) )  =  ( K `  U. ran  ( S  |`  C ) ) )
131 df-ima 4847 . . . . . . . . . . . 12  |-  ( S
" C )  =  ran  ( S  |`  C )
132131unieqi 4207 . . . . . . . . . . 11  |-  U. ( S " C )  = 
U. ran  ( S  |`  C )
133132fveq2i 5868 . . . . . . . . . 10  |-  ( K `
 U. ( S
" C ) )  =  ( K `  U. ran  ( S  |`  C ) )
134130, 133syl6eqr 2503 . . . . . . . . 9  |-  ( ph  ->  ( G DProd  ( S  |`  C ) )  =  ( K `  U. ( S " C ) ) )
135134adantr 467 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( G DProd  ( S  |`  C ) )  =  ( K `
 U. ( S
" C ) ) )
136128, 135sseqtr4d 3469 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  C_  ( G DProd  ( S  |`  C )
) )
13733adantr 467 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  ( G DProd  ( S  |`  C ) )  C_  ( Z `  ( G DProd  ( S  |`  D ) ) ) )
138136, 137sstrd 3442 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  C_  ( Z `  ( G DProd  ( S  |`  D ) ) ) )
139122, 18lsmsubg 17306 . . . . . 6  |-  ( ( ( K `  U. ( S " ( C 
\  { X }
) ) )  e.  (SubGrp `  G )  /\  ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G )  /\  ( K `  U. ( S " ( C 
\  { X }
) ) )  C_  ( Z `  ( G DProd 
( S  |`  D ) ) ) )  -> 
( ( K `  U. ( S " ( C  \  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) )  e.  (SubGrp `  G
) )
140118, 121, 138, 139syl3anc 1268 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  (
( K `  U. ( S " ( C 
\  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) )  e.  (SubGrp `  G
) )
14185mrcsscl 15526 . . . . 5  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " (
I  \  { X } ) )  C_  ( ( K `  U. ( S " ( C  \  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) )  /\  ( ( K `
 U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) )  e.  (SubGrp `  G ) )  -> 
( K `  U. ( S " ( I 
\  { X }
) ) )  C_  ( ( K `  U. ( S " ( C  \  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) ) )
14262, 126, 140, 141syl3anc 1268 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( I  \  { X } ) ) )  C_  ( ( K `  U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) ) )
143 sslin 3658 . . . 4  |-  ( ( K `  U. ( S " ( I  \  { X } ) ) )  C_  ( ( K `  U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) )  ->  ( ( S `  X )  i^i  ( K `  U. ( S " ( I 
\  { X }
) ) ) ) 
C_  ( ( S `
 X )  i^i  ( ( K `  U. ( S " ( C  \  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) ) ) )
144142, 143syl 17 . . 3  |-  ( (
ph  /\  X  e.  C )  ->  (
( S `  X
)  i^i  ( K `  U. ( S "
( I  \  { X } ) ) ) )  C_  ( ( S `  X )  i^i  ( ( K `  U. ( S " ( C  \  { X }
) ) ) (
LSSum `  G ) ( G DProd  ( S  |`  D ) ) ) ) )
14510sselda 3432 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  X  e.  I )
1468ffvelrnda 6022 . . . . 5  |-  ( (
ph  /\  X  e.  I )  ->  ( S `  X )  e.  (SubGrp `  G )
)
147145, 146syldan 473 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( S `  X )  e.  (SubGrp `  G )
)
148 dmdprdsplit.0 . . . 4  |-  .0.  =  ( 0g `  G )
14920adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  (
( S  |`  C ) `
 X )  =  ( S `  X
) )
1506adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  X  e.  C )  ->  G dom DProd  ( S  |`  C ) )
15113adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  X  e.  C )  ->  dom  ( S  |`  C )  =  C )
152150, 151, 65dprdub 17658 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  (
( S  |`  C ) `
 X )  C_  ( G DProd  ( S  |`  C ) ) )
153149, 152eqsstr3d 3467 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( S `  X )  C_  ( G DProd  ( S  |`  C ) ) )
154 dprdsubg 17657 . . . . . . . . . . 11  |-  ( G dom DProd  ( S  |`  C )  ->  ( G DProd  ( S  |`  C ) )  e.  (SubGrp `  G ) )
1556, 154syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( G DProd  ( S  |`  C ) )  e.  (SubGrp `  G )
)
156155adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  X  e.  C )  ->  ( G DProd  ( S  |`  C ) )  e.  (SubGrp `  G ) )
157122lsmlub 17315 . . . . . . . . 9  |-  ( ( ( S `  X
)  e.  (SubGrp `  G )  /\  ( K `  U. ( S
" ( C  \  { X } ) ) )  e.  (SubGrp `  G )  /\  ( G DProd  ( S  |`  C ) )  e.  (SubGrp `  G ) )  -> 
( ( ( S `
 X )  C_  ( G DProd  ( S  |`  C ) )  /\  ( K `  U. ( S " ( C  \  { X } ) ) )  C_  ( G DProd  ( S  |`  C )
) )  <->  ( ( S `  X )
( LSSum `  G )
( K `  U. ( S " ( C 
\  { X }
) ) ) ) 
C_  ( G DProd  ( S  |`  C ) ) ) )
158147, 118, 156, 157syl3anc 1268 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S `  X )  C_  ( G DProd  ( S  |`  C ) )  /\  ( K `
 U. ( S
" ( C  \  { X } ) ) )  C_  ( G DProd  ( S  |`  C )
) )  <->  ( ( S `  X )
( LSSum `  G )
( K `  U. ( S " ( C 
\  { X }
) ) ) ) 
C_  ( G DProd  ( S  |`  C ) ) ) )
159153, 136, 158mpbi2and 932 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  (
( S `  X
) ( LSSum `  G
) ( K `  U. ( S " ( C  \  { X }
) ) ) ) 
C_  ( G DProd  ( S  |`  C ) ) )
160 ssrin 3657 . . . . . . 7  |-  ( ( ( S `  X
) ( LSSum `  G
) ( K `  U. ( S " ( C  \  { X }
) ) ) ) 
C_  ( G DProd  ( S  |`  C ) )  ->  ( ( ( S `  X ) ( LSSum `  G )
( K `  U. ( S " ( C 
\  { X }
) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) )  C_  ( ( G DProd  ( S  |`  C ) )  i^i  ( G DProd 
( S  |`  D ) ) ) )
161159, 160syl 17 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S `  X ) ( LSSum `  G ) ( K `
 U. ( S
" ( C  \  { X } ) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) )  C_  (
( G DProd  ( S  |`  C ) )  i^i  ( G DProd  ( S  |`  D ) ) ) )
162 dmdprdsplit2.4 . . . . . . 7  |-  ( ph  ->  ( ( G DProd  ( S  |`  C ) )  i^i  ( G DProd  ( S  |`  D ) ) )  =  {  .0.  } )
163162adantr 467 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  (
( G DProd  ( S  |`  C ) )  i^i  ( G DProd  ( S  |`  D ) ) )  =  {  .0.  }
)
164161, 163sseqtrd 3468 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S `  X ) ( LSSum `  G ) ( K `
 U. ( S
" ( C  \  { X } ) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) )  C_  {  .0.  } )
165122lsmub1 17308 . . . . . . . . 9  |-  ( ( ( S `  X
)  e.  (SubGrp `  G )  /\  ( K `  U. ( S
" ( C  \  { X } ) ) )  e.  (SubGrp `  G ) )  -> 
( S `  X
)  C_  ( ( S `  X )
( LSSum `  G )
( K `  U. ( S " ( C 
\  { X }
) ) ) ) )
166147, 118, 165syl2anc 667 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  ( S `  X )  C_  ( ( S `  X ) ( LSSum `  G ) ( K `
 U. ( S
" ( C  \  { X } ) ) ) ) )
167148subg0cl 16825 . . . . . . . . 9  |-  ( ( S `  X )  e.  (SubGrp `  G
)  ->  .0.  e.  ( S `  X ) )
168147, 167syl 17 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  .0.  e.  ( S `  X
) )
169166, 168sseldd 3433 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  .0.  e.  ( ( S `  X ) ( LSSum `  G ) ( K `
 U. ( S
" ( C  \  { X } ) ) ) ) )
170148subg0cl 16825 . . . . . . . 8  |-  ( ( G DProd  ( S  |`  D ) )  e.  (SubGrp `  G )  ->  .0.  e.  ( G DProd 
( S  |`  D ) ) )
171121, 170syl 17 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  .0.  e.  ( G DProd  ( S  |`  D ) ) )
172169, 171elind 3618 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  .0.  e.  ( ( ( S `
 X ) (
LSSum `  G ) ( K `  U. ( S " ( C  \  { X } ) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) ) )
173172snssd 4117 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  {  .0.  } 
C_  ( ( ( S `  X ) ( LSSum `  G )
( K `  U. ( S " ( C 
\  { X }
) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) ) )
174164, 173eqssd 3449 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S `  X ) ( LSSum `  G ) ( K `
 U. ( S
" ( C  \  { X } ) ) ) )  i^i  ( G DProd  ( S  |`  D ) ) )  =  {  .0.  } )
175 resima2 5138 . . . . . . . . 9  |-  ( ( C  \  { X } )  C_  C  ->  ( ( S  |`  C ) " ( C  \  { X }
) )  =  ( S " ( C 
\  { X }
) ) )
17686, 175mp1i 13 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  (
( S  |`  C )
" ( C  \  { X } ) )  =  ( S "
( C  \  { X } ) ) )
177176unieqd 4208 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  U. (
( S  |`  C )
" ( C  \  { X } ) )  =  U. ( S
" ( C  \  { X } ) ) )
178177fveq2d 5869 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( ( S  |`  C ) " ( C  \  { X } ) ) )  =  ( K `
 U. ( S
" ( C  \  { X } ) ) ) )
179149, 178ineq12d 3635 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S  |`  C ) `  X
)  i^i  ( K `  U. ( ( S  |`  C ) " ( C  \  { X }
) ) ) )  =  ( ( S `
 X )  i^i  ( K `  U. ( S " ( C 
\  { X }
) ) ) ) )
180150, 151, 65, 148, 85dprddisj 17641 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  (
( ( S  |`  C ) `  X
)  i^i  ( K `  U. ( ( S  |`  C ) " ( C  \  { X }
) ) ) )  =  {  .0.  }
)
181179, 180eqtr3d 2487 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  (
( S `  X
)  i^i  ( K `  U. ( S "
( C  \  { X } ) ) ) )  =  {  .0.  } )
1828adantr 467 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  S : I --> (SubGrp `  G ) )
183 ffun 5731 . . . . . . . 8  |-  ( S : I --> (SubGrp `  G )  ->  Fun  S )
184 funiunfv 6153 . . . . . . . 8  |-  ( Fun 
S  ->  U_ y  e.  ( C  \  { X } ) ( S `
 y )  = 
U. ( S "
( C  \  { X } ) ) )
185182, 183, 1843syl 18 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  U_ y  e.  ( C  \  { X } ) ( S `
 y )  = 
U. ( S "
( C  \  { X } ) ) )
1866ad2antrr 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  ->  G dom DProd  ( S  |`  C ) )
18713ad2antrr 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  ->  dom  ( S  |`  C )  =  C )
188 eldifi 3555 . . . . . . . . . . . 12  |-  ( y  e.  ( C  \  { X } )  -> 
y  e.  C )
189188adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
y  e.  C )
190 simplr 762 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  ->  X  e.  C )
191 eldifsni 4098 . . . . . . . . . . . 12  |-  ( y  e.  ( C  \  { X } )  -> 
y  =/=  X )
192191adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
y  =/=  X )
193186, 187, 189, 190, 192, 18dprdcntz 17640 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
( ( S  |`  C ) `  y
)  C_  ( Z `  ( ( S  |`  C ) `  X
) ) )
194 fvres 5879 . . . . . . . . . . 11  |-  ( y  e.  C  ->  (
( S  |`  C ) `
 y )  =  ( S `  y
) )
195189, 194syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
( ( S  |`  C ) `  y
)  =  ( S `
 y ) )
19620ad2antlr 733 . . . . . . . . . . 11  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
( ( S  |`  C ) `  X
)  =  ( S `
 X ) )
197196fveq2d 5869 . . . . . . . . . 10  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
( Z `  (
( S  |`  C ) `
 X ) )  =  ( Z `  ( S `  X ) ) )
198193, 195, 1973sstr3d 3474 . . . . . . . . 9  |-  ( ( ( ph  /\  X  e.  C )  /\  y  e.  ( C  \  { X } ) )  -> 
( S `  y
)  C_  ( Z `  ( S `  X
) ) )
199198ralrimiva 2802 . . . . . . . 8  |-  ( (
ph  /\  X  e.  C )  ->  A. y  e.  ( C  \  { X } ) ( S `
 y )  C_  ( Z `  ( S `
 X ) ) )
200 iunss 4319 . . . . . . . 8  |-  ( U_ y  e.  ( C  \  { X } ) ( S `  y
)  C_  ( Z `  ( S `  X
) )  <->  A. y  e.  ( C  \  { X } ) ( S `
 y )  C_  ( Z `  ( S `
 X ) ) )
201199, 200sylibr 216 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  U_ y  e.  ( C  \  { X } ) ( S `
 y )  C_  ( Z `  ( S `
 X ) ) )
202185, 201eqsstr3d 3467 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  U. ( S " ( C  \  { X } ) ) 
C_  ( Z `  ( S `  X ) ) )
20335subgss 16818 . . . . . . . 8  |-  ( ( S `  X )  e.  (SubGrp `  G
)  ->  ( S `  X )  C_  ( Base `  G ) )
204147, 203syl 17 . . . . . . 7  |-  ( (
ph  /\  X  e.  C )  ->  ( S `  X )  C_  ( Base `  G
) )
20535, 18cntzsubg 16990 . . . . . . 7  |-  ( ( G  e.  Grp  /\  ( S `  X ) 
C_  ( Base `  G
) )  ->  ( Z `  ( S `  X ) )  e.  (SubGrp `  G )
)
20659, 204, 205syl2anc 667 . . . . . 6  |-  ( (
ph  /\  X  e.  C )  ->  ( Z `  ( S `  X ) )  e.  (SubGrp `  G )
)
20785mrcsscl 15526 . . . . . 6  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( S " ( C  \  { X }
) )  C_  ( Z `  ( S `  X ) )  /\  ( Z `  ( S `
 X ) )  e.  (SubGrp `  G
) )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  C_  ( Z `  ( S `  X
) ) )
20862, 202, 206, 207syl3anc 1268 . . . . 5  |-  ( (
ph  /\  X  e.  C )  ->  ( K `  U. ( S
" ( C  \  { X } ) ) )  C_  ( Z `  ( S `  X
) ) )
20918, 118, 147, 208cntzrecd 17328 . . . 4  |-  ( (
ph  /\  X  e.  C )  ->  ( S `  X )  C_  ( Z `  ( K `  U. ( S
" ( C  \  { X } ) ) ) ) )
210122, 147, 118, 121, 148, 174, 181, 18, 209lsmdisj3 17333 . . 3  |-  ( (
ph  /\  X  e.  C )  ->  (
( S `  X
)  i^i  ( ( K `  U. ( S
" ( C  \  { X } ) ) ) ( LSSum `  G
) ( G DProd  ( S  |`  D ) ) ) )  =  {  .0.  } )
211144, 210sseqtrd 3468 . 2  |-  ( (
ph  /\  X  e.  C )  ->  (
( S `  X
)  i^i  ( K `  U. ( S "
( I  \  { X } ) ) ) )  C_  {  .0.  } )
21256, 211jca 535 1  |-  ( (
ph  /\  X  e.  C )  ->  (
( Y  e.  I  ->  ( X  =/=  Y  ->  ( S `  X
)  C_  ( Z `  ( S `  Y
) ) ) )  /\  ( ( S `
 X )  i^i  ( K `  U. ( S " ( I 
\  { X }
) ) ) ) 
C_  {  .0.  } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    = wceq 1444    e. wcel 1887    =/= wne 2622   A.wral 2737    \ cdif 3401    u. cun 3402    i^i cin 3403    C_ wss 3404   (/)c0 3731   ~Pcpw 3951   {csn 3968   U.cuni 4198   U_ciun 4278   class class class wbr 4402   dom cdm 4834   ran crn 4835    |` cres 4836   "cima 4837   Fun wfun 5576   -->wf 5578   ` cfv 5582  (class class class)co 6290   Basecbs 15121   0gc0g 15338  Moorecmre 15488  mrClscmrc 15489  ACScacs 15491   Grpcgrp 16669  SubGrpcsubg 16811  Cntzccntz 16969   LSSumclsm 17286   DProd cdprd 17625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-tpos 6973  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-map 7474  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-oi 8025  df-card 8373  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11785  df-fzo 11916  df-seq 12214  df-hash 12516  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-0g 15340  df-gsum 15341  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-mhm 16582  df-submnd 16583  df-grp 16673  df-minusg 16674  df-sbg 16675  df-mulg 16676  df-subg 16814  df-ghm 16881  df-gim 16923  df-cntz 16971  df-oppg 16997  df-lsm 17288  df-cmn 17432  df-dprd 17627
This theorem is referenced by:  dmdprdsplit2  17679
  Copyright terms: Public domain W3C validator