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