Metamath Proof Explorer


Theorem gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumdifsnd.b 𝐵 = ( Base ‘ 𝐺 )
gsumdifsnd.p + = ( +g𝐺 )
gsumdifsnd.g ( 𝜑𝐺 ∈ CMnd )
gsumdifsnd.a ( 𝜑𝐴𝑊 )
gsumdifsnd.f ( 𝜑 → ( 𝑘𝐴𝑋 ) finSupp ( 0g𝐺 ) )
gsumdifsnd.e ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
gsumdifsnd.m ( 𝜑𝑀𝐴 )
gsumdifsnd.y ( 𝜑𝑌𝐵 )
gsumdifsnd.s ( ( 𝜑𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
Assertion gsumdifsnd ( 𝜑 → ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) )

Proof

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