Theorem gsumtp

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

	Ref	Expression
Hypotheses	gsumtp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumtp.p	⊢ + = ( +g ‘ 𝐺 )
	gsumtp.s	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
	gsumtp.t	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐷 )
	gsumtp.u	⊢ ( 𝑘 = 𝑂 → 𝐴 = 𝐸 )
	gsumtp.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumtp.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	gsumtp.3	⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
	gsumtp.4	⊢ ( 𝜑 → 𝑂 ∈ 𝑋 )
	gsumtp.5	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
	gsumtp.6	⊢ ( 𝜑 → 𝑁 ≠ 𝑂 )
	gsumtp.7	⊢ ( 𝜑 → 𝑀 ≠ 𝑂 )
	gsumtp.8	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
	gsumtp.9	⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
	gsumtp.10	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
Assertion	gsumtp	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ↦ 𝐴 ) ) = ( ( 𝐶 + 𝐷 ) + 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumtp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumtp.p	⊢ + = ( +g ‘ 𝐺 )
3		gsumtp.s	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
4		gsumtp.t	⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐷 )
5		gsumtp.u	⊢ ( 𝑘 = 𝑂 → 𝐴 = 𝐸 )
6		gsumtp.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
7		gsumtp.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
8		gsumtp.3	⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
9		gsumtp.4	⊢ ( 𝜑 → 𝑂 ∈ 𝑋 )
10		gsumtp.5	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
11		gsumtp.6	⊢ ( 𝜑 → 𝑁 ≠ 𝑂 )
12		gsumtp.7	⊢ ( 𝜑 → 𝑀 ≠ 𝑂 )
13		gsumtp.8	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
14		gsumtp.9	⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
15		gsumtp.10	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
16		tpfi	⊢ { 𝑀 , 𝑁 , 𝑂 } ∈ Fin
17	16	a1i	⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝑂 } ∈ Fin )
18	3	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
19	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑀 ) → 𝐶 ∈ 𝐵 )
20	18 19	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑀 ) → 𝐴 ∈ 𝐵 )
21	4	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑁 ) → 𝐴 = 𝐷 )
22	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑁 ) → 𝐷 ∈ 𝐵 )
23	21 22	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑁 ) → 𝐴 ∈ 𝐵 )
24	5	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑂 ) → 𝐴 = 𝐸 )
25	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑂 ) → 𝐸 ∈ 𝐵 )
26	24 25	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) ∧ 𝑘 = 𝑂 ) → 𝐴 ∈ 𝐵 )
27		eltpi	⊢ ( 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝑁 ∨ 𝑘 = 𝑂 ) )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) → ( 𝑘 = 𝑀 ∨ 𝑘 = 𝑁 ∨ 𝑘 = 𝑂 ) )
29	20 23 26 28	mpjao3dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ) → 𝐴 ∈ 𝐵 )
30		disjprsn	⊢ ( ( 𝑀 ≠ 𝑂 ∧ 𝑁 ≠ 𝑂 ) → ( { 𝑀 , 𝑁 } ∩ { 𝑂 } ) = ∅ )
31	12 11 30	syl2anc	⊢ ( 𝜑 → ( { 𝑀 , 𝑁 } ∩ { 𝑂 } ) = ∅ )
32		df-tp	⊢ { 𝑀 , 𝑁 , 𝑂 } = ( { 𝑀 , 𝑁 } ∪ { 𝑂 } )
33	32	a1i	⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝑂 } = ( { 𝑀 , 𝑁 } ∪ { 𝑂 } ) )
34	1 2 6 17 29 31 33	gsummptfidmsplit	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ↦ 𝐴 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑂 } ↦ 𝐴 ) ) ) )
35	1 2 3 4	gsumpr	⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) = ( 𝐶 + 𝐷 ) )
36	6 7 8 10 13 14 35	syl132anc	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) = ( 𝐶 + 𝐷 ) )
37	6	cmnmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
38	5	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑂 ) → 𝐴 = 𝐸 )
39	1 37 9 15 38	gsumsnd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑂 } ↦ 𝐴 ) ) = 𝐸 )
40	36 39	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑂 } ↦ 𝐴 ) ) ) = ( ( 𝐶 + 𝐷 ) + 𝐸 ) )
41	34 40	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ↦ 𝐴 ) ) = ( ( 𝐶 + 𝐷 ) + 𝐸 ) )