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

Metamath Proof Explorer

Theorem gsummhm2

Description: Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsummhm2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummhm2.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsummhm2.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummhm2.h ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
gsummhm2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsummhm2.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) )
gsummhm2.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
gsummhm2.w ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
gsummhm2.1 ⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝐷 )
gsummhm2.2 ⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → 𝐶 = 𝐸 )
Assertion gsummhm2 ( 𝜑 → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 gsummhm2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummhm2.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsummhm2.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummhm2.h ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
5 gsummhm2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsummhm2.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) )
7 gsummhm2.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
8 gsummhm2.w ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
9 gsummhm2.1 ⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝐷 )
10 gsummhm2.2 ⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → 𝐶 = 𝐸 )
11 7 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐵 )
12 1 2 3 4 5 6 11 8 gsummhm ⊢ ( 𝜑 → ( 𝐻 Σg ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) )
13 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
15 7 13 14 9 fmptco ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) )
16 15 oveq2d ⊢ ( 𝜑 → ( 𝐻 Σg ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∘ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) )
17 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
18 1 2 3 5 11 8 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ∈ 𝐵 )
19 10 eleq1d ⊢ ( 𝑥 = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) → ( 𝐶 ∈ ( Base ‘ 𝐻 ) ↔ 𝐸 ∈ ( Base ‘ 𝐻 ) ) )
20 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
21 1 20 mhmf ⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ ( 𝐺 MndHom 𝐻 ) → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
22 6 21 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
23 17 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐵 𝐶 ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
24 22 23 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐶 ∈ ( Base ‘ 𝐻 ) )
25 19 24 18 rspcdva ⊢ ( 𝜑 → 𝐸 ∈ ( Base ‘ 𝐻 ) )
26 17 10 18 25 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) ) = 𝐸 )
27 12 16 26 3eqtr3d ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑘 ∈ 𝐴 ↦ 𝐷 ) ) = 𝐸 )