gsumunsnf

Description: Append an element to a finite group sum, 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	gsumunsnf.0	$⊢ \underline{Ⅎ} k Y$
	gsumunsnf.b	$⊢ B = {Base}_{G}$
	gsumunsnf.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumunsnf.g	$⊢ φ \to G \in CMnd$
	gsumunsnf.a	$⊢ φ \to A \in Fin$
	gsumunsnf.f	$⊢ (φ \land k \in A) \to X \in B$
	gsumunsnf.m	$⊢ φ \to M \in V$
	gsumunsnf.d	$⊢ φ \to \neg M \in A$
	gsumunsnf.y	$⊢ φ \to Y \in B$
	gsumunsnf.s	$⊢ k = M \to X = Y$
Assertion	gsumunsnf	$⊢ φ \to \underset{k \in A \cup \{M\}}{\sum_{G}} X = (\underset{k \in A}{\sum_{G}}, X) \underset{˙}{+} Y$

Proof

Step	Hyp	Ref	Expression
1		gsumunsnf.0	$⊢ \underline{Ⅎ} k Y$
2		gsumunsnf.b	$⊢ B = {Base}_{G}$
3		gsumunsnf.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumunsnf.g	$⊢ φ \to G \in CMnd$
5		gsumunsnf.a	$⊢ φ \to A \in Fin$
6		gsumunsnf.f	$⊢ (φ \land k \in A) \to X \in B$
7		gsumunsnf.m	$⊢ φ \to M \in V$
8		gsumunsnf.d	$⊢ φ \to \neg M \in A$
9		gsumunsnf.y	$⊢ φ \to Y \in B$
10		gsumunsnf.s	$⊢ k = M \to X = Y$
11	10	adantl	$⊢ (φ \land k = M) \to X = Y$
12	2 3 4 5 6 7 8 9 11 1	gsumunsnfd	$⊢ φ \to \underset{k \in A \cup \{M\}}{\sum_{G}} X = (\underset{k \in A}{\sum_{G}}, X) \underset{˙}{+} Y$

Metamath Proof Explorer

Theorem gsumunsnf

Proof