Metamath Proof Explorer

Theorem gsummpt1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 . (Contributed by AV, 11-Oct-2019)

Ref Expression
Hypotheses gsummpt1n0.0 
|- .0. = ( 0g ` G )
gsummpt1n0.g 
|- ( ph -> G e. Mnd )
gsummpt1n0.i 
|- ( ph -> I e. W )
gsummpt1n0.x 
|- ( ph -> X e. I )
gsummpt1n0.f 
|- F = ( n e. I |-> if ( n = X , A , .0. ) )
gsummpt1n0.a 
|- ( ph -> A. n e. I A e. ( Base ` G ) )
Assertion gsummpt1n0 
|- ( ph -> ( G gsum F ) = [_ X / n ]_ A )

Proof

Step Hyp Ref Expression
1 gsummpt1n0.0 
 |-  .0. = ( 0g ` G )
2 gsummpt1n0.g 
 |-  ( ph -> G e. Mnd )
3 gsummpt1n0.i 
 |-  ( ph -> I e. W )
4 gsummpt1n0.x 
 |-  ( ph -> X e. I )
5 gsummpt1n0.f 
 |-  F = ( n e. I |-> if ( n = X , A , .0. ) )
6 gsummpt1n0.a 
 |-  ( ph -> A. n e. I A e. ( Base ` G ) )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 6 r19.21bi 
 |-  ( ( ph /\ n e. I ) -> A e. ( Base ` G ) )
9 7 1 mndidcl 
 |-  ( G e. Mnd -> .0. e. ( Base ` G ) )
10 2 9 syl 
 |-  ( ph -> .0. e. ( Base ` G ) )
11 10 adantr 
 |-  ( ( ph /\ n e. I ) -> .0. e. ( Base ` G ) )
12 8 11 ifcld 
 |-  ( ( ph /\ n e. I ) -> if ( n = X , A , .0. ) e. ( Base ` G ) )
13 12 5 fmptd 
 |-  ( ph -> F : I --> ( Base ` G ) )
14 5 oveq1i 
 |-  ( F supp .0. ) = ( ( n e. I |-> if ( n = X , A , .0. ) ) supp .0. )
15 eldifsni 
 |-  ( n e. ( I \ { X } ) -> n =/= X )
16 15 adantl 
 |-  ( ( ph /\ n e. ( I \ { X } ) ) -> n =/= X )
17 ifnefalse 
 |-  ( n =/= X -> if ( n = X , A , .0. ) = .0. )
18 16 17 syl 
 |-  ( ( ph /\ n e. ( I \ { X } ) ) -> if ( n = X , A , .0. ) = .0. )
19 18 3 suppss2 
 |-  ( ph -> ( ( n e. I |-> if ( n = X , A , .0. ) ) supp .0. ) C_ { X } )
20 14 19 eqsstrid 
 |-  ( ph -> ( F supp .0. ) C_ { X } )
21 7 1 2 3 4 13 20 gsumpt 
 |-  ( ph -> ( G gsum F ) = ( F ` X ) )
22 nfcv 
 |-  F/_ y if ( n = X , A , .0. )
23 nfv 
 |-  F/ n y = X
24 nfcsb1v 
 |-  F/_ n [_ y / n ]_ A
25 nfcv 
 |-  F/_ n .0.
26 23 24 25 nfif 
 |-  F/_ n if ( y = X , [_ y / n ]_ A , .0. )
27 eqeq1 
 |-  ( n = y -> ( n = X <-> y = X ) )
28 csbeq1a 
 |-  ( n = y -> A = [_ y / n ]_ A )
29 27 28 ifbieq1d 
 |-  ( n = y -> if ( n = X , A , .0. ) = if ( y = X , [_ y / n ]_ A , .0. ) )
30 22 26 29 cbvmpt 
 |-  ( n e. I |-> if ( n = X , A , .0. ) ) = ( y e. I |-> if ( y = X , [_ y / n ]_ A , .0. ) )
31 5 30 eqtri 
 |-  F = ( y e. I |-> if ( y = X , [_ y / n ]_ A , .0. ) )
32 iftrue 
 |-  ( y = X -> if ( y = X , [_ y / n ]_ A , .0. ) = [_ y / n ]_ A )
33 csbeq1 
 |-  ( y = X -> [_ y / n ]_ A = [_ X / n ]_ A )
34 32 33 eqtrd 
 |-  ( y = X -> if ( y = X , [_ y / n ]_ A , .0. ) = [_ X / n ]_ A )
35 rspcsbela 
 |-  ( ( X e. I /\ A. n e. I A e. ( Base ` G ) ) -> [_ X / n ]_ A e. ( Base ` G ) )
36 4 6 35 syl2anc 
 |-  ( ph -> [_ X / n ]_ A e. ( Base ` G ) )
37 31 34 4 36 fvmptd3 
 |-  ( ph -> ( F ` X ) = [_ X / n ]_ A )
38 21 37 eqtrd 
 |-  ( ph -> ( G gsum F ) = [_ X / n ]_ A )