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

Metamath Proof Explorer

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 ( 𝑘 ∈ { 𝑀 , 𝑁 , 𝑂 } ↦ 𝐴 ) ) = ( ( 𝐶 + 𝐷 ) + 𝐸 ) )