This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumsnfd

Description: Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Revised by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnd.b 
|- B = ( Base ` G )
gsumsnd.g 
|- ( ph -> G e. Mnd )
gsumsnd.m 
|- ( ph -> M e. V )
gsumsnd.c 
|- ( ph -> C e. B )
gsumsnd.s 
|- ( ( ph /\ k = M ) -> A = C )
gsumsnfd.p 
|- F/ k ph
gsumsnfd.c 
|- F/_ k C
Assertion gsumsnfd 
|- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C )

Proof

Step Hyp Ref Expression
1 gsumsnd.b 
 |-  B = ( Base ` G )
2 gsumsnd.g 
 |-  ( ph -> G e. Mnd )
3 gsumsnd.m 
 |-  ( ph -> M e. V )
4 gsumsnd.c 
 |-  ( ph -> C e. B )
5 gsumsnd.s 
 |-  ( ( ph /\ k = M ) -> A = C )
6 gsumsnfd.p 
 |-  F/ k ph
7 gsumsnfd.c 
 |-  F/_ k C
8 elsni 
 |-  ( k e. { M } -> k = M )
9 8 5 sylan2 
 |-  ( ( ph /\ k e. { M } ) -> A = C )
10 6 9 mpteq2da 
 |-  ( ph -> ( k e. { M } |-> A ) = ( k e. { M } |-> C ) )
11 10 oveq2d 
 |-  ( ph -> ( G gsum ( k e. { M } |-> A ) ) = ( G gsum ( k e. { M } |-> C ) ) )
12 snfi 
 |-  { M } e. Fin
13 12 a1i 
 |-  ( ph -> { M } e. Fin )
14 eqid 
 |-  ( .g ` G ) = ( .g ` G )
15 7 1 14 gsumconstf 
 |-  ( ( G e. Mnd /\ { M } e. Fin /\ C e. B ) -> ( G gsum ( k e. { M } |-> C ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
16 2 13 4 15 syl3anc 
 |-  ( ph -> ( G gsum ( k e. { M } |-> C ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
17 11 16 eqtrd 
 |-  ( ph -> ( G gsum ( k e. { M } |-> A ) ) = ( ( # ` { M } ) ( .g ` G ) C ) )
18 hashsng 
 |-  ( M e. V -> ( # ` { M } ) = 1 )
19 3 18 syl 
 |-  ( ph -> ( # ` { M } ) = 1 )
20 19 oveq1d 
 |-  ( ph -> ( ( # ` { M } ) ( .g ` G ) C ) = ( 1 ( .g ` G ) C ) )
21 1 14 mulg1 
 |-  ( C e. B -> ( 1 ( .g ` G ) C ) = C )
22 4 21 syl 
 |-  ( ph -> ( 1 ( .g ` G ) C ) = C )
23 17 20 22 3eqtrd 
 |-  ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C )