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

Theorem dpjidcl 17319
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 17247 . . . . 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 210 . . 3  |-  ( ph  ->  ( G dom DProd  S  /\  E. f  e.  W  A  =  ( G  gsumg  f ) ) )
87simprd 461 . 2  |-  ( ph  ->  E. f  e.  W  A  =  ( G  gsumg  f ) )
9 dpjfval.1 . . . . 5  |-  ( ph  ->  G dom DProd  S )
109adantr 463 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  G dom DProd  S )
112adantr 463 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  dom  S  =  I )
129ad2antrr 724 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G dom DProd  S )
132ad2antrr 724 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  dom  S  =  I )
14 dpjfval.p . . . . . 6  |-  P  =  ( GdProj S )
15 simpr 459 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  x  e.  I )
1612, 13, 14, 15dpjf 17318 . . . . 5  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( P `  x
) : ( G DProd 
S ) --> ( S `
 x ) )
171ad2antrr 724 . . . . 5  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  e.  ( G DProd 
S ) )
1816, 17ffvelrnd 5966 . . . 4  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( P `  x ) `  A
)  e.  ( S `
 x ) )
199, 2dprddomcld 17244 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
20 mptexg 6079 . . . . . . 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 463 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e. 
_V )
23 funmpt 5561 . . . . . 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 756 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  e.  W
)
264, 10, 11, 25dprdffsupp 17260 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f finSupp  .0.  )
27 eldifi 3564 . . . . . . . 8  |-  ( x  e.  ( I  \ 
( f supp  .0.  )
)  ->  x  e.  I )
28 eqid 2402 . . . . . . . . . 10  |-  ( proj1 `  G )  =  ( proj1 `  G )
2912, 13, 14, 28, 15dpjval 17317 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( P `  x
)  =  ( ( S `  x ) ( proj1 `  G ) ( G DProd 
( S  |`  (
I  \  { x } ) ) ) ) )
3029fveq1d 5807 . . . . . . . 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 472 . . . . . . 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 763 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  =  ( G  gsumg  f ) )
33 eqid 2402 . . . . . . . . . . 11  |-  ( Base `  G )  =  (
Base `  G )
34 eqid 2402 . . . . . . . . . . 11  |-  (Cntz `  G )  =  (Cntz `  G )
35 dprdgrp 17250 . . . . . . . . . . . . 13  |-  ( G dom DProd  S  ->  G  e. 
Grp )
36 grpmnd 16278 . . . . . . . . . . . . 13  |-  ( G  e.  Grp  ->  G  e.  Mnd )
3710, 35, 363syl 20 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  G  e.  Mnd )
3837adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  G  e.  Mnd )
3919ad2antrr 724 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  I  e.  _V )
404, 10, 11, 25, 33dprdff 17258 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f : I --> ( Base `  G
) )
4140adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
f : I --> ( Base `  G ) )
4225adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f  e.  W )
434, 12, 13, 42, 34dprdfcntz 17261 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ran  f  C_  (
(Cntz `  G ) `  ran  f ) )
4427, 43sylan2 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  ran  f  C_  ( (Cntz `  G ) `  ran  f ) )
45 snssi 4115 . . . . . . . . . . . . 13  |-  ( x  e.  ( I  \ 
( f supp  .0.  )
)  ->  { x }  C_  ( I  \ 
( f supp  .0.  )
) )
4645adantl 464 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  { x }  C_  ( I  \  (
f supp  .0.  ) )
)
4746difss2d 3572 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  { x }  C_  I )
48 suppssdm 6869 . . . . . . . . . . . . . . 15  |-  ( f supp 
.0.  )  C_  dom  f
49 fdm 5674 . . . . . . . . . . . . . . . 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 3489 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( f supp  .0.  )  C_  I )
5251adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( f supp  .0.  )  C_  I )
53 ssconb 3575 . . . . . . . . . . . . 13  |-  ( ( { x }  C_  I  /\  ( f supp  .0.  )  C_  I )  -> 
( { x }  C_  ( I  \  (
f supp  .0.  ) )  <->  ( f supp  .0.  )  C_  ( I  \  { x } ) ) )
5447, 52, 53syl2anc 659 . . . . . . . . . . . 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 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( f supp  .0.  )  C_  ( I  \  {
x } ) )
5626adantr 463 . . . . . . . . . . 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 17130 . . . . . . . . . 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 2446 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  =  ( G  gsumg  ( f  |`  ( I  \  { x } ) ) ) )
59 eqid 2402 . . . . . . . . . . 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 3569 . . . . . . . . . . . . . 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 17287 . . . . . . . . . . . 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 457 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G dom DProd  ( S  |`  ( I  \  {
x } ) ) )
6412, 13dprdf2 17252 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  S : I --> (SubGrp `  G ) )
65 fssres 5690 . . . . . . . . . . . . 13  |-  ( ( S : I --> (SubGrp `  G )  /\  (
I  \  { x } )  C_  I
)  ->  ( S  |`  ( I  \  {
x } ) ) : ( I  \  { x } ) --> (SubGrp `  G )
)
6664, 60, 65sylancl 660 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( S  |`  (
I  \  { x } ) ) : ( I  \  {
x } ) --> (SubGrp `  G ) )
67 fdm 5674 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f : I --> ( Base `  G ) )
7069feqmptd 5858 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f  =  ( k  e.  I  |->  ( f `
 k ) ) )
7170reseq1d 5214 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  (
I  \  { x } ) )  =  ( ( k  e.  I  |->  ( f `  k ) )  |`  ( I  \  { x } ) ) )
72 resmpt 5264 . . . . . . . . . . . . . 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 2459 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  (
I  \  { x } ) )  =  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) ) )
75 eldifi 3564 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( I  \  { x } )  ->  k  e.  I
)
764, 12, 13, 42dprdfcl 17259 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  I )  ->  (
f `  k )  e.  ( S `  k
) )
7775, 76sylan2 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  { x } ) )  -> 
( f `  k
)  e.  ( S `
 k ) )
78 fvres 5819 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( I  \  { x } )  ->  ( ( S  |`  ( I  \  {
x } ) ) `
 k )  =  ( S `  k
) )
7978adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  { x } ) )  -> 
( ( S  |`  ( I  \  { x } ) ) `  k )  =  ( S `  k ) )
8077, 79eleqtrrd 2493 . . . . . . . . . . . . 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 4541 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  _V  ->  (
I  \  { x } )  e.  _V )
8219, 81syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  \  {
x } )  e. 
_V )
83 mptexg 6079 . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( k  e.  ( I  \  { x } )  |->  ( f `
 k ) )  e.  _V )
86 funmpt 5561 . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f finSupp  .0.  )
89 ssdif 3577 . . . . . . . . . . . . . . . . . 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 3437 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ( I 
\  { x }
)  \  ( f supp  .0.  ) )  ->  k  e.  ( I  \  (
f supp  .0.  ) )
)
92 ssid 3460 . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  I  e.  _V )
95 fvex 5815 . . . . . . . . . . . . . . . . . . 19  |-  ( 0g
`  G )  e. 
_V
963, 95eqeltri 2486 . . . . . . . . . . . . . . . . . 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 6888 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( I  \  (
f supp  .0.  ) )
)  ->  ( f `  k )  =  .0.  )
9991, 98sylan2 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I
)  /\  k  e.  ( ( I  \  { x } ) 
\  ( f supp  .0.  ) ) )  -> 
( f `  k
)  =  .0.  )
10082ad2antrr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( I  \  {
x } )  e. 
_V )
10199, 100suppss2 6891 . . . . . . . . . . . . . 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 7799 . . . . . . . . . . . . . 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 1231 . . . . . . . . . . . . 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 17256 . . . . . . . . . . . 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 2490 . . . . . . . . . . 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 17270 . . . . . . . . . 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 472 . . . . . . . . 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 2490 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  ->  A  e.  ( G DProd  ( S  |`  ( I  \  { x } ) ) ) )
109 eqid 2402 . . . . . . . . . 10  |-  ( +g  `  G )  =  ( +g  `  G )
110 eqid 2402 . . . . . . . . . 10  |-  ( LSSum `  G )  =  (
LSSum `  G )
11164, 15ffvelrnd 5966 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( S `  x
)  e.  (SubGrp `  G ) )
112 dprdsubg 17283 . . . . . . . . . . 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 17314 . . . . . . . . . 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 17313 . . . . . . . . . 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 16936 . . . . . . . . 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 649 . . . . . . . 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 666 . . . . . . 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 2443 . . . . . 6  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  ( I  \  ( f supp  .0.  ) ) )  -> 
( ( P `  x ) `  A
)  =  .0.  )
12019adantr 463 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  I  e.  _V )
121119, 120suppss2 6891 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) supp 
.0.  )  C_  (
f supp  .0.  ) )
122 fsuppsssupp 7799 . . . . 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 1231 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) ) finSupp  .0.  )
1244, 10, 11, 18, 123dprdwd 17256 . . 3  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  e.  W )
125 simprr 758 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  A  =  ( G  gsumg  f ) )
12640feqmptd 5858 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  =  ( x  e.  I  |->  ( f `  x ) ) )
127 simplrr 763 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  A  =  ( G 
gsumg  f ) )
12812, 35, 363syl 20 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  G  e.  Mnd )
1294, 12, 13, 42dprdffsupp 17260 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  f finSupp  .0.  )
130 disjdif 3843 . . . . . . . . . . . . 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 3847 . . . . . . . . . . . . 13  |-  ( { x }  u.  (
I  \  { x } ) )  =  ( { x }  u.  I )
13315snssd 4116 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  { x }  C_  I )
134 ssequn1 3612 . . . . . . . . . . . . . 14  |-  ( { x }  C_  I  <->  ( { x }  u.  I )  =  I )
135133, 134sylib 196 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( { x }  u.  I )  =  I )
136132, 135syl5req 2456 . . . . . . . . . . . 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 17160 . . . . . . . . . . 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 5859 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f  |`  { x } )  =  ( k  e.  { x }  |->  ( f `  k ) ) )
139138oveq2d 6250 . . . . . . . . . . . . 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 5966 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( f `  x
)  e.  ( Base `  G ) )
141 fveq2 5805 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
f `  k )  =  ( f `  x ) )
14233, 141gsumsn 17194 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( k  e.  {
x }  |->  ( f `
 k ) ) )  =  ( f `
 x ) )
144139, 143eqtrd 2443 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( G  gsumg  ( f  |`  { x } ) )  =  ( f `  x
) )
145144oveq1d 6249 . . . . . . . . . . 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 2447 . . . . . . . . . 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 17315 . . . . . . . . . . . 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 2492 . . . . . . . . . . 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 17259 . . . . . . . . . . 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 16934 . . . . . . . . . 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 210 . . . . . . . . 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 457 . . . . . . . 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 2443 . . . . . . 7  |-  ( ( ( ph  /\  (
f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  /\  x  e.  I )  ->  ( ( P `  x ) `  A
)  =  ( f `
 x ) )
154153mpteq2dva 4480 . . . . . 6  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( x  e.  I  |->  ( ( P `
 x ) `  A ) )  =  ( x  e.  I  |->  ( f `  x
) ) )
155126, 154eqtr4d 2446 . . . . 5  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  f  =  ( x  e.  I  |->  ( ( P `  x
) `  A )
) )
156155oveq2d 6250 . . . 4  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  ( G  gsumg  f )  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `
 A ) ) ) )
157125, 156eqtrd 2443 . . 3  |-  ( (
ph  /\  ( f  e.  W  /\  A  =  ( G  gsumg  f ) ) )  ->  A  =  ( G  gsumg  ( x  e.  I  |->  ( ( P `  x ) `  A
) ) ) )
158124, 157jca 530 . 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 2899 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 184    /\ wa 367    = wceq 1405    e. wcel 1842   E.wrex 2754   {crab 2757   _Vcvv 3058    \ cdif 3410    u. cun 3411    i^i cin 3412    C_ wss 3413   (/)c0 3737   {csn 3971   class class class wbr 4394    |-> cmpt 4452   dom cdm 4942   ran crn 4943    |` cres 4944   Fun wfun 5519   -->wf 5521   ` cfv 5525  (class class class)co 6234   supp csupp 6856   X_cixp 7427   finSupp cfsupp 7783   Basecbs 14733   +g cplusg 14801   0gc0g 14946    gsumg cgsu 14947   Mndcmnd 16135   Grpcgrp 16269  SubGrpcsubg 16411  Cntzccntz 16569   LSSumclsm 16870   proj1cpj1 16871   DProd cdprd 17236  dProjcdpj 17237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-inf2 8011  ax-cnex 9498  ax-resscn 9499  ax-1cn 9500  ax-icn 9501  ax-addcl 9502  ax-addrcl 9503  ax-mulcl 9504  ax-mulrcl 9505  ax-mulcom 9506  ax-addass 9507  ax-mulass 9508  ax-distr 9509  ax-i2m1 9510  ax-1ne0 9511  ax-1rid 9512  ax-rnegex 9513  ax-rrecex 9514  ax-cnre 9515  ax-pre-lttri 9516  ax-pre-lttrn 9517  ax-pre-ltadd 9518  ax-pre-mulgt0 9519
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-of 6477  df-om 6639  df-1st 6738  df-2nd 6739  df-supp 6857  df-tpos 6912  df-recs 6999  df-rdg 7033  df-1o 7087  df-oadd 7091  df-er 7268  df-map 7379  df-ixp 7428  df-en 7475  df-dom 7476  df-sdom 7477  df-fin 7478  df-fsupp 7784  df-oi 7889  df-card 8272  df-pnf 9580  df-mnf 9581  df-xr 9582  df-ltxr 9583  df-le 9584  df-sub 9763  df-neg 9764  df-nn 10497  df-2 10555  df-n0 10757  df-z 10826  df-uz 11046  df-fz 11644  df-fzo 11768  df-seq 12062  df-hash 12360  df-ndx 14736  df-slot 14737  df-base 14738  df-sets 14739  df-ress 14740  df-plusg 14814  df-0g 14948  df-gsum 14949  df-mre 15092  df-mrc 15093  df-acs 15095  df-mgm 16088  df-sgrp 16127  df-mnd 16137  df-mhm 16182  df-submnd 16183  df-grp 16273  df-minusg 16274  df-sbg 16275  df-mulg 16276  df-subg 16414  df-ghm 16481  df-gim 16523  df-cntz 16571  df-oppg 16597  df-lsm 16872  df-pj1 16873  df-cmn 17016  df-dprd 17238  df-dpj 17239
This theorem is referenced by:  dpjeq  17320  dpjid  17321
  Copyright terms: Public domain W3C validator