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 ⊢ B = Base G
gsummhm2.z ⊢ 0 ˙ = 0 G
gsummhm2.g ⊢ φ → G ∈ CMnd
gsummhm2.h ⊢ φ → H ∈ Mnd
gsummhm2.a ⊢ φ → A ∈ V
gsummhm2.k ⊢ φ → x ∈ B ⟼ C ∈ G MndHom H
gsummhm2.f ⊢ φ ∧ k ∈ A → X ∈ B
gsummhm2.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
gsummhm2.1 ⊢ x = X → C = D
gsummhm2.2 ⊢ x = ∑ G k ∈ A X → C = E
Assertion gsummhm2 ⊢ φ → ∑ H k ∈ A D = E

Proof

Step Hyp Ref Expression
1 gsummhm2.b ⊢ B = Base G
2 gsummhm2.z ⊢ 0 ˙ = 0 G
3 gsummhm2.g ⊢ φ → G ∈ CMnd
4 gsummhm2.h ⊢ φ → H ∈ Mnd
5 gsummhm2.a ⊢ φ → A ∈ V
6 gsummhm2.k ⊢ φ → x ∈ B ⟼ C ∈ G MndHom H
7 gsummhm2.f ⊢ φ ∧ k ∈ A → X ∈ B
8 gsummhm2.w ⊢ φ → finSupp 0 ˙⁡ k ∈ A ⟼ X
9 gsummhm2.1 ⊢ x = X → C = D
10 gsummhm2.2 ⊢ x = ∑ G k ∈ A X → C = E
11 7 fmpttd ⊢ φ → k ∈ A ⟼ X : A ⟶ B
12 1 2 3 4 5 6 11 8 gsummhm ⊢ φ → ∑ H x ∈ B ⟼ C ∘ k ∈ A ⟼ X = x ∈ B ⟼ C ⁡ ∑ G k ∈ A X
13 eqidd ⊢ φ → k ∈ A ⟼ X = k ∈ A ⟼ X
14 eqidd ⊢ φ → x ∈ B ⟼ C = x ∈ B ⟼ C
15 7 13 14 9 fmptco ⊢ φ → x ∈ B ⟼ C ∘ k ∈ A ⟼ X = k ∈ A ⟼ D
16 15 oveq2d ⊢ φ → ∑ H x ∈ B ⟼ C ∘ k ∈ A ⟼ X = ∑ H k ∈ A D
17 eqid ⊢ x ∈ B ⟼ C = x ∈ B ⟼ C
18 1 2 3 5 11 8 gsumcl ⊢ φ → ∑ G k ∈ A X ∈ B
19 10 eleq1d ⊢ x = ∑ G k ∈ A X → C ∈ Base H ↔ E ∈ Base H
20 eqid ⊢ Base H = Base H
21 1 20 mhmf ⊢ x ∈ B ⟼ C ∈ G MndHom H → x ∈ B ⟼ C : B ⟶ Base H
22 6 21 syl ⊢ φ → x ∈ B ⟼ C : B ⟶ Base H
23 17 fmpt ⊢ ∀ x ∈ B C ∈ Base H ↔ x ∈ B ⟼ C : B ⟶ Base H
24 22 23 sylibr ⊢ φ → ∀ x ∈ B C ∈ Base H
25 19 24 18 rspcdva ⊢ φ → E ∈ Base H
26 17 10 18 25 fvmptd3 ⊢ φ → x ∈ B ⟼ C ⁡ ∑ G k ∈ A X = E
27 12 16 26 3eqtr3d ⊢ φ → ∑ H k ∈ A D = E