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

Metamath Proof Explorer

Theorem gsumzresunsn

Description: Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Hypotheses gsumzresunsn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzresunsn.p ⊢ + = ( +g ‘ 𝐺 )
gsumzresunsn.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzresunsn.y ⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
gsumzresunsn.f ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
gsumzresunsn.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
gsumzresunsn.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzresunsn.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsumzresunsn.2 ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
gsumzresunsn.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
gsumzresunsn.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
gsumzresunsn.5 ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) )
Assertion gsumzresunsn ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gsumzresunsn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzresunsn.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumzresunsn.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4 gsumzresunsn.y ⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
5 gsumzresunsn.f ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
6 gsumzresunsn.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
7 gsumzresunsn.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
8 gsumzresunsn.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
9 gsumzresunsn.2 ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
10 gsumzresunsn.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
11 gsumzresunsn.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12 gsumzresunsn.5 ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) )
13 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) )
14 df-ima ⊢ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) )
15 10 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐶 )
16 6 15 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝐶 )
17 5 16 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
18 17 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
19 14 18 eqtrid ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
20 19 fveq2d ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( 𝑍 ‘ ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
21 12 19 20 3sstr3d ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑍 ‘ ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐶 ⟶ 𝐵 )
23 6 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐶 )
24 22 23 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
27 26 4 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = 𝑌 )
28 1 2 3 13 7 8 21 24 10 9 11 27 gsumzunsnd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) + 𝑌 ) )
29 17 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
30 5 6 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
32 31 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) + 𝑌 ) )
33 28 29 32 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) )