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	$⊢ φ \to G \in Mnd$
	gsumsnd.m	$⊢ φ \to M \in V$
	gsumsnd.c	$⊢ φ \to C \in B$
	gsumsnd.s	$⊢ (φ \land k = M) \to A = C$
	gsumsnfd.p	$⊢ Ⅎ k φ$
	gsumsnfd.c	$⊢ \underline{Ⅎ} k C$
Assertion	gsumsnfd	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} A = C$

Proof

Step	Hyp	Ref	Expression
1		gsumsnd.b	$⊢ B = {Base}_{G}$
2		gsumsnd.g	$⊢ φ \to G \in Mnd$
3		gsumsnd.m	$⊢ φ \to M \in V$
4		gsumsnd.c	$⊢ φ \to C \in B$
5		gsumsnd.s	$⊢ (φ \land k = M) \to A = C$
6		gsumsnfd.p	$⊢ Ⅎ k φ$
7		gsumsnfd.c	$⊢ \underline{Ⅎ} k C$
8		elsni	$⊢ k \in \{M\} \to k = M$
9	8 5	sylan2	$⊢ (φ \land k \in \{M\}) \to A = C$
10	6 9	mpteq2da	$⊢ φ \to (k \in \{M\} ⟼ A) = (k \in \{M\} ⟼ C)$
11	10	oveq2d	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} A = \underset{k \in \{M\}}{\sum_{G}} C$
12		snfi	$⊢ \{M\} \in Fin$
13	12	a1i	$⊢ φ \to \{M\} \in Fin$
14		eqid	$⊢ \cdot_{G} = \cdot_{G}$
15	7 1 14	gsumconstf	$⊢ (G \in Mnd \land \{M\} \in Fin \land C \in B) \to \underset{k \in \{M\}}{\sum_{G}} C = \|\{M\}\| \cdot_{G} C$
16	2 13 4 15	syl3anc	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} C = \|\{M\}\| \cdot_{G} C$
17	11 16	eqtrd	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} A = \|\{M\}\| \cdot_{G} C$
18		hashsng	$⊢ M \in V \to \|\{M\}\| = 1$
19	3 18	syl	$⊢ φ \to \|\{M\}\| = 1$
20	19	oveq1d	$⊢ φ \to \|\{M\}\| \cdot_{G} C = 1 \cdot_{G} C$
21	1 14	mulg1	$⊢ C \in B \to 1 \cdot_{G} C = C$
22	4 21	syl	$⊢ φ \to 1 \cdot_{G} C = C$
23	17 20 22	3eqtrd	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} A = C$

Metamath Proof Explorer

Theorem gsumsnfd

Proof