Step |
Hyp |
Ref |
Expression |
1 |
|
gsumdifsndf.k |
⊢ Ⅎ 𝑘 𝑌 |
2 |
|
gsumdifsndf.n |
⊢ Ⅎ 𝑘 𝜑 |
3 |
|
gsumdifsndf.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
4 |
|
gsumdifsndf.p |
⊢ + = ( +g ‘ 𝐺 ) |
5 |
|
gsumdifsndf.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
6 |
|
gsumdifsndf.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) |
7 |
|
gsumdifsndf.f |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) ) |
8 |
|
gsumdifsndf.e |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 ) |
9 |
|
gsumdifsndf.m |
⊢ ( 𝜑 → 𝑀 ∈ 𝐴 ) |
10 |
|
gsumdifsndf.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
11 |
|
gsumdifsndf.s |
⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 ) |
12 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
13 |
9
|
snssd |
⊢ ( 𝜑 → { 𝑀 } ⊆ 𝐴 ) |
14 |
|
difin2 |
⊢ ( { 𝑀 } ⊆ 𝐴 → ( { 𝑀 } ∖ { 𝑀 } ) = ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) ) |
15 |
13 14
|
syl |
⊢ ( 𝜑 → ( { 𝑀 } ∖ { 𝑀 } ) = ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) ) |
16 |
|
difid |
⊢ ( { 𝑀 } ∖ { 𝑀 } ) = ∅ |
17 |
15 16
|
eqtr3di |
⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) = ∅ ) |
18 |
|
difsnid |
⊢ ( 𝑀 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) = 𝐴 ) |
19 |
9 18
|
syl |
⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) = 𝐴 ) |
20 |
19
|
eqcomd |
⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) ) |
21 |
2 3 12 4 5 6 8 7 17 20
|
gsumsplit2f |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) ) |
22 |
|
cmnmnd |
⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd ) |
23 |
5 22
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
24 |
3 23 9 10 11 2 1
|
gsumsnfd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 ) |
25 |
24
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) ) |
26 |
21 25
|
eqtrd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) ) |