Theorem gsumtp

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

	Ref	Expression
Hypotheses	gsumtp.b	$$⊢B={\mathrm{Base}}_G$$
	gsumtp.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumtp.s	$$⊢k=M\to A=C$$
	gsumtp.t	$$⊢k=N\to A=D$$
	gsumtp.u	$$⊢k=O\to A=E$$
	gsumtp.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumtp.2	$$⊢\phi \to M\in V$$
	gsumtp.3	$$⊢\phi \to N\in W$$
	gsumtp.4	$$⊢\phi \to O\in X$$
	gsumtp.5	$$⊢\phi \to M\ne N$$
	gsumtp.6	$$⊢\phi \to N\ne O$$
	gsumtp.7	$$⊢\phi \to M\ne O$$
	gsumtp.8	$$⊢\phi \to C\in B$$
	gsumtp.9	$$⊢\phi \to D\in B$$
	gsumtp.10	$$⊢\phi \to E\in B$$
Assertion	gsumtp	$$⊢\phi \to \underset{k\in \left\{M,N,O\right\}}{{\sum }_G}A=\left(C\underset{\dot{}}{+}D\right)\underset{\dot{}}{+}E$$

Proof

Step	Hyp	Ref	Expression
1		gsumtp.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumtp.p	$$⊢\underset{\dot{}}{+}={+}_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	$$⊢\phi \to G\in \mathrm{CMnd}$$
7		gsumtp.2	$$⊢\phi \to M\in V$$
8		gsumtp.3	$$⊢\phi \to N\in W$$
9		gsumtp.4	$$⊢\phi \to O\in X$$
10		gsumtp.5	$$⊢\phi \to M\ne N$$
11		gsumtp.6	$$⊢\phi \to N\ne O$$
12		gsumtp.7	$$⊢\phi \to M\ne O$$
13		gsumtp.8	$$⊢\phi \to C\in B$$
14		gsumtp.9	$$⊢\phi \to D\in B$$
15		gsumtp.10	$$⊢\phi \to E\in B$$
16		tpfi	$$⊢\left\{M,N,O\right\}\in \mathrm{Fin}$$
17	16	a1i	$$⊢\phi \to \left\{M,N,O\right\}\in \mathrm{Fin}$$
18	3	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=M\right)\to A=C$$
19	13	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=M\right)\to C\in B$$
20	18 19	eqeltrd	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=M\right)\to A\in B$$
21	4	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=N\right)\to A=D$$
22	14	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=N\right)\to D\in B$$
23	21 22	eqeltrd	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=N\right)\to A\in B$$
24	5	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=O\right)\to A=E$$
25	15	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=O\right)\to E\in B$$
26	24 25	eqeltrd	$$⊢\left(\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\wedge k=O\right)\to A\in B$$
27		eltpi	$$⊢k\in \left\{M,N,O\right\}\to \left(k=M\vee k=N\vee k=O\right)$$
28	27	adantl	$$⊢\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\to \left(k=M\vee k=N\vee k=O\right)$$
29	20 23 26 28	mpjao3dan	$$⊢\left(\phi \wedge k\in \left\{M,N,O\right\}\right)\to A\in B$$
30		disjprsn	$$⊢\left(M\ne O\wedge N\ne O\right)\to \left\{M,N\right\}\cap \left\{O\right\}=\varnothing$$
31	12 11 30	syl2anc	$$⊢\phi \to \left\{M,N\right\}\cap \left\{O\right\}=\varnothing$$
32		df-tp	$$⊢\left\{M,N,O\right\}=\left\{M,N\right\}\cup \left\{O\right\}$$
33	32	a1i	$$⊢\phi \to \left\{M,N,O\right\}=\left\{M,N\right\}\cup \left\{O\right\}$$
34	1 2 6 17 29 31 33	gsummptfidmsplit	$$⊢\phi \to \underset{k\in \left\{M,N,O\right\}}{{\sum }_G}A=\left(\underset{k\in \left\{M,N\right\}}{{\sum }_G},A\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{O\right\}}{{\sum }_G},A\right)$$
35	1 2 3 4	gsumpr	$$⊢\left(G\in \mathrm{CMnd}\wedge \left(M\in V\wedge N\in W\wedge M\ne N\right)\wedge \left(C\in B\wedge D\in B\right)\right)\to \underset{k\in \left\{M,N\right\}}{{\sum }_G}A=C\underset{\dot{}}{+}D$$
36	6 7 8 10 13 14 35	syl132anc	$$⊢\phi \to \underset{k\in \left\{M,N\right\}}{{\sum }_G}A=C\underset{\dot{}}{+}D$$
37	6	cmnmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
38	5	adantl	$$⊢\left(\phi \wedge k=O\right)\to A=E$$
39	1 37 9 15 38	gsumsnd	$$⊢\phi \to \underset{k\in \left\{O\right\}}{{\sum }_G}A=E$$
40	36 39	oveq12d	$$⊢\phi \to \left(\underset{k\in \left\{M,N\right\}}{{\sum }_G},A\right)\underset{\dot{}}{+}\left(\underset{k\in \left\{O\right\}}{{\sum }_G},A\right)=\left(C\underset{\dot{}}{+}D\right)\underset{\dot{}}{+}E$$
41	34 40	eqtrd	$$⊢\phi \to \underset{k\in \left\{M,N,O\right\}}{{\sum }_G}A=\left(C\underset{\dot{}}{+}D\right)\underset{\dot{}}{+}E$$