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	$⊢ \underline{Ⅎ} k C$
		gsumsnf.b	$⊢ B = {Base}_{G}$
		gsumsnf.s	$⊢ k = M \to A = C$
	Assertion	gsumsnf	$⊢ (G \in Mnd \land M \in V \land C \in B) \to \underset{k \in \{M\}}{\sum_{G}} A = C$

Proof

Step	Hyp	Ref	Expression
1		gsumsnf.c	$⊢ \underline{Ⅎ} k C$
2		gsumsnf.b	$⊢ B = {Base}_{G}$
3		gsumsnf.s	$⊢ k = M \to A = C$
4		simp1	$⊢ (G \in Mnd \land M \in V \land C \in B) \to G \in Mnd$
5		simp2	$⊢ (G \in Mnd \land M \in V \land C \in B) \to M \in V$
6		simp3	$⊢ (G \in Mnd \land M \in V \land C \in B) \to C \in B$
7	3	adantl	$⊢ ((G \in Mnd \land M \in V \land C \in B) \land k = M) \to A = C$
8		nfv	$⊢ Ⅎ k G \in Mnd$
9		nfv	$⊢ Ⅎ k M \in V$
10	1	nfel1	$⊢ Ⅎ k C \in B$
11	8 9 10	nf3an	$⊢ Ⅎ k (G \in Mnd \land M \in V \land C \in B)$
12	2 4 5 6 7 11 1	gsumsnfd	$⊢ (G \in Mnd \land M \in V \land C \in B) \to \underset{k \in \{M\}}{\sum_{G}} A = C$