# Metamath Proof Explorer

## Theorem gsumunsnfd

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumunsnd.b 𝐵 = ( Base ‘ 𝐺 )
gsumunsnd.p + = ( +g𝐺 )
gsumunsnd.g ( 𝜑𝐺 ∈ CMnd )
gsumunsnd.a ( 𝜑𝐴 ∈ Fin )
gsumunsnd.f ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
gsumunsnd.m ( 𝜑𝑀𝑉 )
gsumunsnd.d ( 𝜑 → ¬ 𝑀𝐴 )
gsumunsnd.y ( 𝜑𝑌𝐵 )
gsumunsnd.s ( ( 𝜑𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
gsumunsnfd.0 𝑘 𝑌
Assertion gsumunsnfd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) + 𝑌 ) )

### Proof

Step Hyp Ref Expression
1 gsumunsnd.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumunsnd.p + = ( +g𝐺 )
3 gsumunsnd.g ( 𝜑𝐺 ∈ CMnd )
4 gsumunsnd.a ( 𝜑𝐴 ∈ Fin )
5 gsumunsnd.f ( ( 𝜑𝑘𝐴 ) → 𝑋𝐵 )
6 gsumunsnd.m ( 𝜑𝑀𝑉 )
7 gsumunsnd.d ( 𝜑 → ¬ 𝑀𝐴 )
8 gsumunsnd.y ( 𝜑𝑌𝐵 )
9 gsumunsnd.s ( ( 𝜑𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
10 gsumunsnfd.0 𝑘 𝑌
11 snfi { 𝑀 } ∈ Fin
12 unfi ( ( 𝐴 ∈ Fin ∧ { 𝑀 } ∈ Fin ) → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
13 4 11 12 sylancl ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
14 elun ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↔ ( 𝑘𝐴𝑘 ∈ { 𝑀 } ) )
15 elsni ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
16 15 9 sylan2 ( ( 𝜑𝑘 ∈ { 𝑀 } ) → 𝑋 = 𝑌 )
17 8 adantr ( ( 𝜑𝑘 ∈ { 𝑀 } ) → 𝑌𝐵 )
18 16 17 eqeltrd ( ( 𝜑𝑘 ∈ { 𝑀 } ) → 𝑋𝐵 )
19 5 18 jaodan ( ( 𝜑 ∧ ( 𝑘𝐴𝑘 ∈ { 𝑀 } ) ) → 𝑋𝐵 )
20 14 19 sylan2b ( ( 𝜑𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋𝐵 )
21 disjsn ( ( 𝐴 ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀𝐴 )
22 7 21 sylibr ( 𝜑 → ( 𝐴 ∩ { 𝑀 } ) = ∅ )
23 eqidd ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) = ( 𝐴 ∪ { 𝑀 } ) )
24 1 2 3 13 20 22 23 gsummptfidmsplit ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) )
25 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
26 3 25 syl ( 𝜑𝐺 ∈ Mnd )
27 nfv 𝑘 𝜑
28 1 26 6 8 9 27 10 gsumsnfd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 )
29 28 oveq2d ( 𝜑 → ( ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) + 𝑌 ) )
30 24 29 eqtrd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘𝐴𝑋 ) ) + 𝑌 ) )