Metamath Proof Explorer


Theorem gsumdifsndf

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019)

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

Proof

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 ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) )