This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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