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

Metamath Proof Explorer

Theorem gsumpr

Description: Group sum of a pair. (Contributed by AV, 6-Dec-2018) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumpr.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumpr.p ⊢ + = ( +g ‘ 𝐺 )
gsumpr.s ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
gsumpr.t ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐷 )
Assertion gsumpr ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) = ( 𝐶 + 𝐷 ) )

Proof

Step Hyp Ref Expression
1 gsumpr.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumpr.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumpr.s ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
4 gsumpr.t ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐷 )
5 simp1 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐺 ∈ CMnd )
6 prfi ⊢ { 𝑀 , 𝑁 } ∈ Fin
7 6 a1i ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → { 𝑀 , 𝑁 } ∈ Fin )
8 vex ⊢ 𝑘 ∈ V
9 8 elpr ⊢ ( 𝑘 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑘 = 𝑀 ∨ 𝑘 = 𝑁 ) )
10 eleq1a ⊢ ( 𝐶 ∈ 𝐵 → ( 𝐴 = 𝐶 → 𝐴 ∈ 𝐵 ) )
11 10 adantr ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐴 = 𝐶 → 𝐴 ∈ 𝐵 ) )
12 11 3ad2ant3 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐴 = 𝐶 → 𝐴 ∈ 𝐵 ) )
13 3 12 syl5com ⊢ ( 𝑘 = 𝑀 → ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 ) )
14 eleq1a ⊢ ( 𝐷 ∈ 𝐵 → ( 𝐴 = 𝐷 → 𝐴 ∈ 𝐵 ) )
15 14 adantl ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐴 = 𝐷 → 𝐴 ∈ 𝐵 ) )
16 15 3ad2ant3 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐴 = 𝐷 → 𝐴 ∈ 𝐵 ) )
17 4 16 syl5com ⊢ ( 𝑘 = 𝑁 → ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 ) )
18 13 17 jaoi ⊢ ( ( 𝑘 = 𝑀 ∨ 𝑘 = 𝑁 ) → ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 ) )
19 9 18 sylbi ⊢ ( 𝑘 ∈ { 𝑀 , 𝑁 } → ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐵 ) )
20 19 impcom ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑀 , 𝑁 } ) → 𝐴 ∈ 𝐵 )
21 disjsn2 ⊢ ( 𝑀 ≠ 𝑁 → ( { 𝑀 } ∩ { 𝑁 } ) = ∅ )
22 21 3ad2ant3 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) → ( { 𝑀 } ∩ { 𝑁 } ) = ∅ )
23 22 3ad2ant2 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( { 𝑀 } ∩ { 𝑁 } ) = ∅ )
24 df-pr ⊢ { 𝑀 , 𝑁 } = ( { 𝑀 } ∪ { 𝑁 } )
25 24 a1i ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → { 𝑀 , 𝑁 } = ( { 𝑀 } ∪ { 𝑁 } ) )
26 eqid ⊢ ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) = ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 )
27 1 2 5 7 20 23 25 26 gsummptfidmsplitres ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) = ( ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) ) ) )
28 snsspr1 ⊢ { 𝑀 } ⊆ { 𝑀 , 𝑁 }
29 resmpt ⊢ ( { 𝑀 } ⊆ { 𝑀 , 𝑁 } → ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) )
30 28 29 mp1i ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) )
31 30 oveq2d ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) )
32 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
33 simp1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) → 𝑀 ∈ 𝑉 )
34 simpl ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
35 1 3 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )
36 32 33 34 35 syl3an ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )
37 31 36 eqtrd ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) ) = 𝐶 )
38 snsspr2 ⊢ { 𝑁 } ⊆ { 𝑀 , 𝑁 }
39 resmpt ⊢ ( { 𝑁 } ⊆ { 𝑀 , 𝑁 } → ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) = ( 𝑘 ∈ { 𝑁 } ↦ 𝐴 ) )
40 38 39 mp1i ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) = ( 𝑘 ∈ { 𝑁 } ↦ 𝐴 ) )
41 40 oveq2d ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝐴 ) ) )
42 simp2 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) → 𝑁 ∈ 𝑊 )
43 simpr ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → 𝐷 ∈ 𝐵 )
44 1 4 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ 𝑊 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝐴 ) ) = 𝐷 )
45 32 42 43 44 syl3an ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑁 } ↦ 𝐴 ) ) = 𝐷 )
46 41 45 eqtrd ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) ) = 𝐷 )
47 37 46 oveq12d ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑀 } ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ↾ { 𝑁 } ) ) ) = ( 𝐶 + 𝐷 ) )
48 27 47 eqtrd ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 , 𝑁 } ↦ 𝐴 ) ) = ( 𝐶 + 𝐷 ) )