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

Metamath Proof Explorer

Theorem gsumunsnd

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 2-Jan-2019) (Proof shortened by AV, 11-Dec-2019)

		Ref	Expression
	Hypotheses	gsumunsnd.b	$⊢ B = {Base}_{G}$
		gsumunsnd.p	$⊢ \underset{˙}{+} = +_{G}$
		gsumunsnd.g	$⊢ φ \to G \in CMnd$
		gsumunsnd.a	$⊢ φ \to A \in Fin$
		gsumunsnd.f	$⊢ (φ \land k \in A) \to X \in B$
		gsumunsnd.m	$⊢ φ \to M \in V$
		gsumunsnd.d	$⊢ φ \to \neg M \in A$
		gsumunsnd.y	$⊢ φ \to Y \in B$
		gsumunsnd.s	$⊢ (φ \land k = M) \to X = Y$
	Assertion	gsumunsnd	$⊢ φ \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		gsumunsnd.b	$⊢ B = {Base}_{G}$
2		gsumunsnd.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsumunsnd.g	$⊢ φ \to G \in CMnd$
4		gsumunsnd.a	$⊢ φ \to A \in Fin$
5		gsumunsnd.f	$⊢ (φ \land k \in A) \to X \in B$
6		gsumunsnd.m	$⊢ φ \to M \in V$
7		gsumunsnd.d	$⊢ φ \to \neg M \in A$
8		gsumunsnd.y	$⊢ φ \to Y \in B$
9		gsumunsnd.s	$⊢ (φ \land k = M) \to X = Y$
10		nfcv	$⊢ \underline{Ⅎ} k Y$
11	1 2 3 4 5 6 7 8 9 10	gsumunsnfd	$⊢ φ \to \underset{k \in A \cup \{M\}}{\sum_{G}} X = (\underset{k \in A}{\sum_{G}}, X) \underset{˙}{+} Y$