gsumtp

Description: Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	gsumtp.b	$⊢ B = {Base}_{G}$
	gsumtp.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumtp.s	$⊢ k = M \to A = C$
	gsumtp.t	$⊢ k = N \to A = D$
	gsumtp.u	$⊢ k = O \to A = E$
	gsumtp.1	$⊢ φ \to G \in CMnd$
	gsumtp.2	$⊢ φ \to M \in V$
	gsumtp.3	$⊢ φ \to N \in W$
	gsumtp.4	$⊢ φ \to O \in X$
	gsumtp.5	$⊢ φ \to M \neq N$
	gsumtp.6	$⊢ φ \to N \neq O$
	gsumtp.7	$⊢ φ \to M \neq O$
	gsumtp.8	$⊢ φ \to C \in B$
	gsumtp.9	$⊢ φ \to D \in B$
	gsumtp.10	$⊢ φ \to E \in B$
Assertion	gsumtp	$⊢ φ \to \underset{k \in \{M, N, O\}}{\sum_{G}} A = (C \underset{˙}{+} D) \underset{˙}{+} E$

Proof

Step	Hyp	Ref	Expression
1		gsumtp.b	$⊢ B = {Base}_{G}$
2		gsumtp.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsumtp.s	$⊢ k = M \to A = C$
4		gsumtp.t	$⊢ k = N \to A = D$
5		gsumtp.u	$⊢ k = O \to A = E$
6		gsumtp.1	$⊢ φ \to G \in CMnd$
7		gsumtp.2	$⊢ φ \to M \in V$
8		gsumtp.3	$⊢ φ \to N \in W$
9		gsumtp.4	$⊢ φ \to O \in X$
10		gsumtp.5	$⊢ φ \to M \neq N$
11		gsumtp.6	$⊢ φ \to N \neq O$
12		gsumtp.7	$⊢ φ \to M \neq O$
13		gsumtp.8	$⊢ φ \to C \in B$
14		gsumtp.9	$⊢ φ \to D \in B$
15		gsumtp.10	$⊢ φ \to E \in B$
16		tpfi	$⊢ \{M, N, O\} \in Fin$
17	16	a1i	$⊢ φ \to \{M, N, O\} \in Fin$
18	3	adantl	$⊢ ((φ \land k \in \{M, N, O\}) \land k = M) \to A = C$
19	13	ad2antrr	$⊢ ((φ \land k \in \{M, N, O\}) \land k = M) \to C \in B$
20	18 19	eqeltrd	$⊢ ((φ \land k \in \{M, N, O\}) \land k = M) \to A \in B$
21	4	adantl	$⊢ ((φ \land k \in \{M, N, O\}) \land k = N) \to A = D$
22	14	ad2antrr	$⊢ ((φ \land k \in \{M, N, O\}) \land k = N) \to D \in B$
23	21 22	eqeltrd	$⊢ ((φ \land k \in \{M, N, O\}) \land k = N) \to A \in B$
24	5	adantl	$⊢ ((φ \land k \in \{M, N, O\}) \land k = O) \to A = E$
25	15	ad2antrr	$⊢ ((φ \land k \in \{M, N, O\}) \land k = O) \to E \in B$
26	24 25	eqeltrd	$⊢ ((φ \land k \in \{M, N, O\}) \land k = O) \to A \in B$
27		eltpi	$⊢ k \in \{M, N, O\} \to (k = M \lor k = N \lor k = O)$
28	27	adantl	$⊢ (φ \land k \in \{M, N, O\}) \to (k = M \lor k = N \lor k = O)$
29	20 23 26 28	mpjao3dan	$⊢ (φ \land k \in \{M, N, O\}) \to A \in B$
30		disjprsn	$⊢ (M \neq O \land N \neq O) \to \{M, N\} \cap \{O\} = \emptyset$
31	12 11 30	syl2anc	$⊢ φ \to \{M, N\} \cap \{O\} = \emptyset$
32		df-tp	$⊢ \{M, N, O\} = \{M, N\} \cup \{O\}$
33	32	a1i	$⊢ φ \to \{M, N, O\} = \{M, N\} \cup \{O\}$
34	1 2 6 17 29 31 33	gsummptfidmsplit	$⊢ φ \to \underset{k \in \{M, N, O\}}{\sum_{G}} A = (\underset{k \in \{M, N\}}{\sum_{G}}, A) \underset{˙}{+} (\underset{k \in \{O\}}{\sum_{G}}, A)$
35	1 2 3 4	gsumpr	$⊢ (G \in CMnd \land (M \in V \land N \in W \land M \neq N) \land (C \in B \land D \in B)) \to \underset{k \in \{M, N\}}{\sum_{G}} A = C \underset{˙}{+} D$
36	6 7 8 10 13 14 35	syl132anc	$⊢ φ \to \underset{k \in \{M, N\}}{\sum_{G}} A = C \underset{˙}{+} D$
37	6	cmnmndd	$⊢ φ \to G \in Mnd$
38	5	adantl	$⊢ (φ \land k = O) \to A = E$
39	1 37 9 15 38	gsumsnd	$⊢ φ \to \underset{k \in \{O\}}{\sum_{G}} A = E$
40	36 39	oveq12d	$⊢ φ \to (\underset{k \in \{M, N\}}{\sum_{G}}, A) \underset{˙}{+} (\underset{k \in \{O\}}{\sum_{G}}, A) = (C \underset{˙}{+} D) \underset{˙}{+} E$
41	34 40	eqtrd	$⊢ φ \to \underset{k \in \{M, N, O\}}{\sum_{G}} A = (C \underset{˙}{+} D) \underset{˙}{+} E$

Metamath Proof Explorer

Theorem gsumtp

Proof