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