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

Theorem dpjidcl 17627
Description: The key property of projections: the sum of all the projections of  A is  A. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
Hypotheses
Ref Expression
dpjfval.1  |-  ( ph  ->  G dom DProd  S )
dpjfval.2  |-  ( ph  ->  dom  S  =  I )
dpjfval.p  |-  P  =  ( GdProj S )
dpjidcl.3  |-  ( ph  ->  A  e.  ( G DProd 
S ) )
dpjidcl.0  |-  .0.  =  ( 0g `  G )
dpjidcl.w  |-  W  =  { h  e.  X_ i  e.  I  ( S `  i )  |  h finSupp  .0.  }
Assertion
Ref Expression
dpjidcl  |-  ( ph  ->  ( ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e.  W  /\  A  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `  A
) ) ) ) )
Distinct variable groups:    x, h,  .0.    h, i, G, x    P, h, x    ph, i, x    h, I, i, x   
x, W    A, h, x    S, h, i, x
Allowed substitution hints:    ph( h)    A( i)    P( i)    W( h, i)    .0. ( i)

Proof of Theorem dpjidcl
Dummy variables  k 
f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dpjidcl.3 . . . 4  |-  ( ph  ->  A  e.  ( G DProd 
S ) )
2 dpjfval.2 . . . . 5  |-  ( ph  ->  dom  S  =  I )
3 dpjidcl.0 . . . . . 6  |-  .0.  =  ( 0g `  G )
4 dpjidcl.w . . . . . 6  |-  W  =  { h  e.  X_ i  e.  I  ( S `  i )  |  h finSupp  .0.  }
53, 4eldprd 17572 . . . . 5  |-  ( dom 
S  =  I  -> 
( A  e.  ( G DProd  S )  <->  ( G dom DProd  S  /\  E. f  e.  W  A  =  ( G  gsumg  f ) ) ) )
62, 5syl 17 . . . 4  |-  ( ph  ->  ( A  e.  ( G DProd  S )  <->  ( G dom DProd  S  /\  E. f  e.  W  A  =  ( G  gsumg  f ) ) ) )
71, 6mpbid 213 . . 3  |-  ( ph  ->  ( G dom DProd  S  /\  E. f  e.  W  A  =  ( G  gsumg  f ) ) )
87simprd 464 . 2  |-  ( ph  ->  E. f  e.  W  A  =  ( G  gsumg  f ) )
9 dpjfval.1 . . . . 5  |-  ( ph  ->  G dom DProd  S )
109adantr 466 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  G dom DProd  S )
112adantr 466 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  dom  S  =  I )
129ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G dom DProd  S )
132ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  dom  S  =  I )
14 dpjfval.p . . . . . 6  |-  P  =  ( GdProj S )
15 simpr 462 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  x  e.  I )
1612, 13, 14, 15dpjf 17626 . . . . 5  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( P `  x
) : ( G DProd 
S ) --> ( S `
 x ) )
171ad2antrr 730 . . . . 5  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  e.  ( G DProd 
S ) )
1816, 17ffvelrnd 5975 . . . 4  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( P `  x ) `  A
)  e.  ( S `
 x ) )
199, 2dprddomcld 17569 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
20 mptexg 6087 . . . . . . 7  |-  ( I  e.  _V  ->  (
x  e.  I  |->  ( ( P `  x
) `  A )
)  e.  _V )
2119, 20syl 17 . . . . . 6  |-  ( ph  ->  ( x  e.  I  |->  ( ( P `  x ) `  A
) )  e.  _V )
2221adantr 466 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e. 
_V )
23 funmpt 5573 . . . . . 6  |-  Fun  (
x  e.  I  |->  ( ( P `  x
) `  A )
)
2423a1i 11 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  Fun  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) )
25 simprl 762 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  e.  W
)
264, 10, 11, 25dprdffsupp 17583 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f finSupp  .0.  )
27 eldifi 3523 . . . . . . . 8  |-  ( x  e.  ( I  \ 
( f supp  .0.  )
)  ->  x  e.  I )
28 eqid 2422 . . . . . . . . . 10  |-  ( proj1 `  G )  =  ( proj1 `  G )
2912, 13, 14, 28, 15dpjval 17625 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( P `  x
)  =  ( ( S `  x ) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) )
3029fveq1d 5820 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( P `  x ) `  A
)  =  ( ( ( S `  x
) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) `  A ) )
3127, 30sylan2 476 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( ( P `  x ) `  A
)  =  ( ( ( S `  x
) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) `  A ) )
32 simplrr 769 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  =  ( G  gsumg  f ) )
33 eqid 2422 . . . . . . . . . . 11  |-  ( Base `  G )  =  (
Base `  G )
34 eqid 2422 . . . . . . . . . . 11  |-  (Cntz `  G )  =  (Cntz `  G )
35 dprdgrp 17573 . . . . . . . . . . . . 13  |-  ( G dom DProd  S  ->  G  e. 
Grp )
36 grpmnd 16614 . . . . . . . . . . . . 13  |-  ( G  e.  Grp  ->  G  e.  Mnd )
3710, 35, 363syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  G  e.  Mnd )
3837adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  G  e.  Mnd )
3919ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  I  e.  _V )
404, 10, 11, 25, 33dprdff 17581 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f : I --> ( Base `  G
) )
4140adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
f : I --> ( Base `  G ) )
4225adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f  e.  W )
434, 12, 13, 42, 34dprdfcntz 17584 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ran  f  C_  (
(Cntz `  G ) `  ran  f ) )
4427, 43sylan2 476 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  ran  f  C_  ( (Cntz `  G ) `  ran  f ) )
45 snssi 4080 . . . . . . . . . . . . 13  |-  ( x  e.  ( I  \ 
( f supp  .0.  )
)  ->  { x }  C_  ( I  \ 
( f supp  .0.  )
) )
4645adantl 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  { x }  C_  ( I  \  (
f supp  .0.  ) )
)
4746difss2d 3531 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  { x }  C_  I )
48 suppssdm 6875 . . . . . . . . . . . . . . 15  |-  ( f supp 
.0.  )  C_  dom  f
49 fdm 5686 . . . . . . . . . . . . . . . 16  |-  ( f : I --> ( Base `  G )  ->  dom  f  =  I )
5040, 49syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  dom  f  =  I )
5148, 50syl5sseq 3448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( f supp  .0.  )  C_  I )
5251adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( f supp  .0.  )  C_  I )
53 ssconb 3534 . . . . . . . . . . . . 13  |-  ( ( { x }  C_  I  /\  ( f supp  .0.  )  C_  I )  -> 
( { x }  C_  ( I  \  (
f supp  .0.  ) )  <->  ( f supp  .0.  )  C_  ( I  \  { x } ) ) )
5447, 52, 53syl2anc 665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( { x }  C_  ( I  \  (
f supp  .0.  ) )  <->  ( f supp  .0.  )  C_  ( I  \  { x } ) ) )
5546, 54mpbid 213 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( f supp  .0.  )  C_  ( I  \  {
x } ) )
5626adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
f finSupp  .0.  )
5733, 3, 34, 38, 39, 41, 44, 55, 56gsumzres 17479 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( G  gsumg  ( f  |`  (
I  \  { x } ) ) )  =  ( G  gsumg  f ) )
5832, 57eqtr4d 2459 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  =  ( G  gsumg  ( f  |`  ( I  \  { x } ) ) ) )
59 eqid 2422 . . . . . . . . . . 11  |-  { h  e.  X_ i  e.  ( I  \  { x } ) ( ( S  |`  ( I  \  { x } ) ) `  i )  |  h finSupp  .0.  }  =  { h  e.  X_ i  e.  ( I  \  {
x } ) ( ( S  |`  (
I  \  { x } ) ) `  i )  |  h finSupp  .0.  }
60 difss 3528 . . . . . . . . . . . . . 14  |-  ( I 
\  { x }
)  C_  I
6160a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( I  \  {
x } )  C_  I )
6212, 13, 61dprdres 17597 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G dom DProd  ( S  |`  ( I  \  {
x } ) )  /\  ( G DProd  ( S  |`  ( I  \  { x } ) ) )  C_  ( G DProd  S ) ) )
6362simpld 460 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G dom DProd  ( S  |`  ( I  \  {
x } ) ) )
6412, 13dprdf2 17575 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  S : I --> (SubGrp `  G ) )
65 fssres 5702 . . . . . . . . . . . . 13  |-  ( ( S : I --> (SubGrp `  G )  /\  (
I  \  { x } )  C_  I
)  ->  ( S  |`  ( I  \  {
x } ) ) : ( I  \  { x } ) --> (SubGrp `  G )
)
6664, 60, 65sylancl 666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( S  |`  (
I  \  { x } ) ) : ( I  \  {
x } ) --> (SubGrp `  G ) )
67 fdm 5686 . . . . . . . . . . . 12  |-  ( ( S  |`  ( I  \  { x } ) ) : ( I 
\  { x }
) --> (SubGrp `  G )  ->  dom  ( S  |`  ( I  \  { x } ) )  =  ( I  \  {
x } ) )
6866, 67syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  dom  ( S  |`  ( I  \  { x } ) )  =  ( I  \  {
x } ) )
6940adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f : I --> ( Base `  G ) )
7069feqmptd 5871 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f  =  ( k  e.  I  |->  ( f `
 k ) ) )
7170reseq1d 5059 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  (
I  \  { x } ) )  =  ( ( k  e.  I  |->  ( f `  k ) )  |`  ( I  \  { x } ) ) )
72 resmpt 5109 . . . . . . . . . . . . . 14  |-  ( ( I  \  { x } )  C_  I  ->  ( ( k  e.  I  |->  ( f `  k ) )  |`  ( I  \  { x } ) )  =  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) ) )
7360, 72ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( k  e.  I  |->  ( f `  k ) )  |`  ( I  \  { x } ) )  =  ( k  e.  ( I  \  { x } ) 
|->  ( f `  k
) )
7471, 73syl6eq 2472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  (
I  \  { x } ) )  =  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) ) )
75 eldifi 3523 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( I  \  { x } )  ->  k  e.  I
)
764, 12, 13, 42dprdfcl 17582 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  I )  ->  (
f `  k )  e.  ( S `  k
) )
7775, 76sylan2 476 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  { x } ) )  -> 
( f `  k
)  e.  ( S `
 k ) )
78 fvres 5832 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( I  \  { x } )  ->  ( ( S  |`  ( I  \  {
x } ) ) `
 k )  =  ( S `  k
) )
7978adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  { x } ) )  -> 
( ( S  |`  ( I  \  { x } ) ) `  k )  =  ( S `  k ) )
8077, 79eleqtrrd 2503 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  { x } ) )  -> 
( f `  k
)  e.  ( ( S  |`  ( I  \  { x } ) ) `  k ) )
81 difexg 4508 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  _V  ->  (
I  \  { x } )  e.  _V )
8219, 81syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  \  {
x } )  e. 
_V )
83 mptexg 6087 . . . . . . . . . . . . . . . 16  |-  ( ( I  \  { x } )  e.  _V  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) )  e.  _V )
8482, 83syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) )  e.  _V )
8584ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) )  e.  _V )
86 funmpt 5573 . . . . . . . . . . . . . . 15  |-  Fun  (
k  e.  ( I 
\  { x }
)  |->  ( f `  k ) )
8786a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  Fun  ( k  e.  ( I  \  {
x } )  |->  ( f `  k ) ) )
8826adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f finSupp  .0.  )
89 ssdif 3536 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  \  { x } )  C_  I  ->  ( ( I  \  { x } ) 
\  ( f supp  .0.  ) )  C_  (
I  \  ( f supp  .0.  ) ) )
9060, 89ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { x } )  \  (
f supp  .0.  ) )  C_  ( I  \  (
f supp  .0.  ) )
9190sseli 3396 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ( I 
\  { x }
)  \  ( f supp  .0.  ) )  ->  k  e.  ( I  \  (
f supp  .0.  ) )
)
92 ssid 3419 . . . . . . . . . . . . . . . . . 18  |-  ( f supp 
.0.  )  C_  (
f supp  .0.  )
9392a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f supp  .0.  )  C_  ( f supp  .0.  )
)
9419ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  I  e.  _V )
95 fvex 5828 . . . . . . . . . . . . . . . . . . 19  |-  ( 0g
`  G )  e. 
_V
963, 95eqeltri 2496 . . . . . . . . . . . . . . . . . 18  |-  .0.  e.  _V
9796a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  .0.  e.  _V )
9869, 93, 94, 97suppssr 6894 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  (
f supp  .0.  ) )
)  ->  ( f `  k )  =  .0.  )
9991, 98sylan2 476 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( ( I  \  { x } ) 
\  ( f supp  .0.  ) ) )  -> 
( f `  k
)  =  .0.  )
10082ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( I  \  {
x } )  e. 
_V )
10199, 100suppss2 6897 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( k  e.  ( I  \  {
x } )  |->  ( f `  k ) ) supp  .0.  )  C_  ( f supp  .0.  )
)
102 fsuppsssupp 7845 . . . . . . . . . . . . . 14  |-  ( ( ( ( k  e.  ( I  \  {
x } )  |->  ( f `  k ) )  e.  _V  /\  Fun  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) ) )  /\  ( f finSupp  .0.  /\  ( ( k  e.  ( I  \  { x } ) 
|->  ( f `  k
) ) supp  .0.  )  C_  ( f supp  .0.  )
) )  ->  (
k  e.  ( I 
\  { x }
)  |->  ( f `  k ) ) finSupp  .0.  )
10385, 87, 88, 101, 102syl22anc 1265 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) ) finSupp  .0.  )
10459, 63, 68, 80, 103dprdwd 17579 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) )  e.  { h  e.  X_ i  e.  (
I  \  { x } ) ( ( S  |`  ( I  \  { x } ) ) `  i )  |  h finSupp  .0.  } )
10574, 104eqeltrd 2500 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  (
I  \  { x } ) )  e. 
{ h  e.  X_ i  e.  ( I  \  { x } ) ( ( S  |`  ( I  \  { x } ) ) `  i )  |  h finSupp  .0.  } )
1063, 59, 63, 68, 105eldprdi 17587 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( f  |`  (
I  \  { x } ) ) )  e.  ( G DProd  ( S  |`  ( I  \  { x } ) ) ) )
10727, 106sylan2 476 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( G  gsumg  ( f  |`  (
I  \  { x } ) ) )  e.  ( G DProd  ( S  |`  ( I  \  { x } ) ) ) )
10858, 107eqeltrd 2500 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  e.  ( G DProd  ( S  |`  ( I  \  { x } ) ) ) )
109 eqid 2422 . . . . . . . . . 10  |-  ( +g  `  G )  =  ( +g  `  G )
110 eqid 2422 . . . . . . . . . 10  |-  ( LSSum `  G )  =  (
LSSum `  G )
11164, 15ffvelrnd 5975 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( S `  x
)  e.  (SubGrp `  G ) )
112 dprdsubg 17593 . . . . . . . . . . 11  |-  ( G dom DProd  ( S  |`  ( I  \  { x } ) )  -> 
( G DProd  ( S  |`  ( I  \  {
x } ) ) )  e.  (SubGrp `  G ) )
11363, 112syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G DProd  ( S  |`  ( I  \  {
x } ) ) )  e.  (SubGrp `  G ) )
11412, 13, 15, 3dpjdisj 17622 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( S `  x )  i^i  ( G DProd  ( S  |`  (
I  \  { x } ) ) ) )  =  {  .0.  } )
11512, 13, 15, 34dpjcntz 17621 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( S `  x
)  C_  ( (Cntz `  G ) `  ( G DProd  ( S  |`  (
I  \  { x } ) ) ) ) )
116109, 110, 3, 34, 111, 113, 114, 115, 28pj1rid 17288 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  A  e.  ( G DProd  ( S  |`  ( I  \  {
x } ) ) ) )  ->  (
( ( S `  x ) ( proj1 `  G )
( G DProd  ( S  |`  ( I  \  {
x } ) ) ) ) `  A
)  =  .0.  )
11727, 116sylanl2 655 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp 
.0.  ) ) )  /\  A  e.  ( G DProd  ( S  |`  ( I  \  { x } ) ) ) )  ->  ( (
( S `  x
) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) `  A )  =  .0.  )
118108, 117mpdan 672 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( ( ( S `
 x ) (
proj1 `  G
) ( G DProd  ( S  |`  ( I  \  { x } ) ) ) ) `  A )  =  .0.  )
11931, 118eqtrd 2456 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( ( P `  x ) `  A
)  =  .0.  )
12019adantr 466 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  I  e.  _V )
121119, 120suppss2 6897 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) supp 
.0.  )  C_  (
f supp  .0.  ) )
122 fsuppsssupp 7845 . . . . 5  |-  ( ( ( ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e. 
_V  /\  Fun  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) )  /\  ( f finSupp  .0.  /\  ( ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) supp 
.0.  )  C_  (
f supp  .0.  ) )
)  ->  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) finSupp  .0.  )
12322, 24, 26, 121, 122syl22anc 1265 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) ) finSupp  .0.  )
1244, 10, 11, 18, 123dprdwd 17579 . . 3  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e.  W )
125 simprr 764 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  A  =  ( G  gsumg  f ) )
12640feqmptd 5871 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  =  ( x  e.  I  |->  ( f `  x ) ) )
127 simplrr 769 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  =  ( G 
gsumg  f ) )
12812, 35, 363syl 18 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G  e.  Mnd )
1294, 12, 13, 42dprdffsupp 17583 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f finSupp  .0.  )
130 disjdif 3805 . . . . . . . . . . . . 13  |-  ( { x }  i^i  (
I  \  { x } ) )  =  (/)
131130a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( { x }  i^i  ( I  \  {
x } ) )  =  (/) )
132 undif2 3809 . . . . . . . . . . . . 13  |-  ( { x }  u.  (
I  \  { x } ) )  =  ( { x }  u.  I )
13315snssd 4081 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  { x }  C_  I )
134 ssequn1 3572 . . . . . . . . . . . . . 14  |-  ( { x }  C_  I  <->  ( { x }  u.  I )  =  I )
135133, 134sylib 199 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( { x }  u.  I )  =  I )
136132, 135syl5req 2469 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  I  =  ( { x }  u.  (
I  \  { x } ) ) )
13733, 3, 109, 34, 128, 94, 69, 43, 129, 131, 136gsumzsplit 17496 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  f )  =  ( ( G  gsumg  ( f  |`  { x } ) ) ( +g  `  G ) ( G  gsumg  ( f  |`  (
I  \  { x } ) ) ) ) )
13869, 133feqresmpt 5872 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  { x } )  =  ( k  e.  { x }  |->  ( f `  k ) ) )
139138oveq2d 6258 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( f  |`  { x } ) )  =  ( G  gsumg  ( k  e.  {
x }  |->  ( f `
 k ) ) ) )
14069, 15ffvelrnd 5975 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f `  x
)  e.  ( Base `  G ) )
141 fveq2 5818 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
f `  k )  =  ( f `  x ) )
14233, 141gsumsn 17523 . . . . . . . . . . . . . 14  |-  ( ( G  e.  Mnd  /\  x  e.  I  /\  ( f `  x
)  e.  ( Base `  G ) )  -> 
( G  gsumg  ( k  e.  {
x }  |->  ( f `
 k ) ) )  =  ( f `
 x ) )
143128, 15, 140, 142syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( k  e.  {
x }  |->  ( f `
 k ) ) )  =  ( f `
 x ) )
144139, 143eqtrd 2456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( f  |`  { x } ) )  =  ( f `  x
) )
145144oveq1d 6257 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( G  gsumg  ( f  |`  { x } ) ) ( +g  `  G
) ( G  gsumg  ( f  |`  ( I  \  {
x } ) ) ) )  =  ( ( f `  x
) ( +g  `  G
) ( G  gsumg  ( f  |`  ( I  \  {
x } ) ) ) ) )
146127, 137, 1453eqtrd 2460 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  =  ( ( f `  x ) ( +g  `  G
) ( G  gsumg  ( f  |`  ( I  \  {
x } ) ) ) ) )
14712, 13, 15, 110dpjlsm 17623 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G DProd  S )  =  ( ( S `
 x ) (
LSSum `  G ) ( G DProd  ( S  |`  ( I  \  { x } ) ) ) ) )
14817, 147eleqtrd 2502 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  e.  ( ( S `  x ) ( LSSum `  G )
( G DProd  ( S  |`  ( I  \  {
x } ) ) ) ) )
1494, 10, 11, 25dprdfcl 17582 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f `  x
)  e.  ( S `
 x ) )
150109, 110, 3, 34, 111, 113, 114, 115, 28, 148, 149, 106pj1eq 17286 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( A  =  ( ( f `  x
) ( +g  `  G
) ( G  gsumg  ( f  |`  ( I  \  {
x } ) ) ) )  <->  ( (
( ( S `  x ) ( proj1 `  G )
( G DProd  ( S  |`  ( I  \  {
x } ) ) ) ) `  A
)  =  ( f `
 x )  /\  ( ( ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ( proj1 `  G ) ( S `
 x ) ) `
 A )  =  ( G  gsumg  ( f  |`  (
I  \  { x } ) ) ) ) ) )
151146, 150mpbid 213 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( ( ( S `  x ) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) `  A )  =  ( f `  x )  /\  (
( ( G DProd  ( S  |`  ( I  \  { x } ) ) ) ( proj1 `  G )
( S `  x
) ) `  A
)  =  ( G 
gsumg  ( f  |`  (
I  \  { x } ) ) ) ) )
152151simpld 460 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( ( S `
 x ) (
proj1 `  G
) ( G DProd  ( S  |`  ( I  \  { x } ) ) ) ) `  A )  =  ( f `  x ) )
15330, 152eqtrd 2456 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( P `  x ) `  A
)  =  ( f `
 x ) )
154153mpteq2dva 4446 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  =  ( x  e.  I  |->  ( f `  x
) ) )
155126, 154eqtr4d 2459 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  =  ( x  e.  I  |->  ( ( P `  x
) `  A )
) )
156155oveq2d 6258 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( G  gsumg  f )  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) ) )
157125, 156eqtrd 2456 . . 3  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  A  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `  A
) ) ) )
158124, 157jca 534 . 2  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( ( x  e.  I  |->  ( ( P `  x ) `
 A ) )  e.  W  /\  A  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) ) ) )
1598, 158rexlimddv 2854 1  |-  ( ph  ->  ( ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e.  W  /\  A  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `  A
) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   E.wrex 2709   {crab 2712   _Vcvv 3016    \ cdif 3369    u. cun 3370    i^i cin 3371    C_ wss 3372   (/)c0 3697   {csn 3934   class class class wbr 4359    |-> cmpt 4418   dom cdm 4789   ran crn 4790    |` cres 4791   Fun wfun 5531   -->wf 5533   ` cfv 5537  (class class class)co 6242   supp csupp 6862   X_cixp 7470   finSupp cfsupp 7829   Basecbs 15057   +g cplusg 15126   0gc0g 15274    gsumg cgsu 15275   Mndcmnd 16471   Grpcgrp 16605  SubGrpcsubg 16747  Cntzccntz 16905   LSSumclsm 17222   proj1cpj1 17223   DProd cdprd 17561  dProjcdpj 17562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-inf2 8092  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-iin 4238  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-se 4749  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-isom 5546  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-of 6482  df-om 6644  df-1st 6744  df-2nd 6745  df-supp 6863  df-tpos 6921  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7830  df-oi 7971  df-card 8318  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-2 10612  df-n0 10814  df-z 10882  df-uz 11104  df-fz 11729  df-fzo 11860  df-seq 12157  df-hash 12459  df-ndx 15060  df-slot 15061  df-base 15062  df-sets 15063  df-ress 15064  df-plusg 15139  df-0g 15276  df-gsum 15277  df-mre 15428  df-mrc 15429  df-acs 15431  df-mgm 16424  df-sgrp 16463  df-mnd 16473  df-mhm 16518  df-submnd 16519  df-grp 16609  df-minusg 16610  df-sbg 16611  df-mulg 16612  df-subg 16750  df-ghm 16817  df-gim 16859  df-cntz 16907  df-oppg 16933  df-lsm 17224  df-pj1 17225  df-cmn 17368  df-dprd 17563  df-dpj 17564
This theorem is referenced by:  dpjeq  17628  dpjid  17629
  Copyright terms: Public domain W3C validator