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

Metamath Proof Explorer

Theorem gsumsnf

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

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

Proof

Step Hyp Ref Expression
1 gsumsnf.c 
 |-  F/_ k C
2 gsumsnf.b 
 |-  B = ( Base ` G )
3 gsumsnf.s 
 |-  ( k = M -> A = C )
4 simp1 
 |-  ( ( G e. Mnd /\ M e. V /\ C e. B ) -> G e. Mnd )
5 simp2 
 |-  ( ( G e. Mnd /\ M e. V /\ C e. B ) -> M e. V )
6 simp3 
 |-  ( ( G e. Mnd /\ M e. V /\ C e. B ) -> C e. B )
7 3 adantl 
 |-  ( ( ( G e. Mnd /\ M e. V /\ C e. B ) /\ k = M ) -> A = C )
8 nfv 
 |-  F/ k G e. Mnd
9 nfv 
 |-  F/ k M e. V
10 1 nfel1 
 |-  F/ k C e. B
11 8 9 10 nf3an 
 |-  F/ k ( G e. Mnd /\ M e. V /\ C e. B )
12 2 4 5 6 7 11 1 gsumsnfd 
 |-  ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M } |-> A ) ) = C )