Metamath Proof Explorer

Theorem gsumzunsnd

Description: Append an element to a finite group sum, more general version of gsumunsnd . (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses gsumzunsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzunsnd.p ⊢ + = ( +g ‘ 𝐺 )
gsumzunsnd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzunsnd.f ⊢ 𝐹 = ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 )
gsumzunsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzunsnd.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsumzunsnd.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzunsnd.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
gsumzunsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
gsumzunsnd.d ⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
gsumzunsnd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
gsumzunsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
Assertion gsumzunsnd ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gsumzunsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzunsnd.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumzunsnd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4 gsumzunsnd.f ⊢ 𝐹 = ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 )
5 gsumzunsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumzunsnd.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 gsumzunsnd.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
8 gsumzunsnd.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
9 gsumzunsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
10 gsumzunsnd.d ⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
11 gsumzunsnd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12 gsumzunsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
13 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14 snfi ⊢ { 𝑀 } ∈ Fin
15 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑀 } ∈ Fin ) → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
16 6 14 15 sylancl ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
17 elun ⊢ ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) )
18 elsni ⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
19 18 12 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 = 𝑌 )
20 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑌 ∈ 𝐵 )
21 19 20 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 ∈ 𝐵 )
22 8 21 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
23 17 22 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
24 23 4 fmptd ⊢ ( 𝜑 → 𝐹 : ( 𝐴 ∪ { 𝑀 } ) ⟶ 𝐵 )
25 8 expcom ⊢ ( 𝑘 ∈ 𝐴 → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
26 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑌 ∈ 𝐵 )
27 12 26 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 ∈ 𝐵 )
28 27 expcom ⊢ ( 𝑘 = 𝑀 → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
29 18 28 syl ⊢ ( 𝑘 ∈ { 𝑀 } → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
30 25 29 jaoi ⊢ ( ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
31 17 30 sylbi ⊢ ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
32 31 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
33 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
34 4 16 32 33 fsuppmptdm ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
35 disjsn ⊢ ( ( 𝐴 ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ 𝐴 )
36 10 35 sylibr ⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑀 } ) = ∅ )
37 eqidd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) = ( 𝐴 ∪ { 𝑀 } ) )
38 1 13 2 3 5 16 24 7 34 36 37 gsumzsplit ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) ) )
39 4 reseq1i ⊢ ( 𝐹 ↾ 𝐴 ) = ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 )
40 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑀 } )
41 resmpt ⊢ ( 𝐴 ⊆ ( 𝐴 ∪ { 𝑀 } ) → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
42 40 41 mp1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
43 39 42 syl5eq ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
44 43 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) )
45 4 reseq1i ⊢ ( 𝐹 ↾ { 𝑀 } ) = ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } )
46 ssun2 ⊢ { 𝑀 } ⊆ ( 𝐴 ∪ { 𝑀 } )
47 resmpt ⊢ ( { 𝑀 } ⊆ ( 𝐴 ∪ { 𝑀 } ) → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
48 46 47 mp1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
49 45 48 syl5eq ⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
50 49 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) )
51 44 50 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) )
52 1 5 9 11 12 gsumsnd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 )
53 52 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )
54 38 51 53 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )