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

Metamath Proof Explorer

Theorem mhm0

Description: A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses mhm0.z ⊢ 0 ˙ = 0 S
mhm0.y ⊢ Y = 0 T
Assertion mhm0 ⊢ F ∈ S MndHom T → F ⁡ 0 ˙ = Y

Proof

Step Hyp Ref Expression
1 mhm0.z ⊢ 0 ˙ = 0 S
2 mhm0.y ⊢ Y = 0 T
3 eqid ⊢ Base S = Base S
4 eqid ⊢ Base T = Base T
5 eqid ⊢ + S = + S
6 eqid ⊢ + T = + T
7 3 4 5 6 1 2 ismhm ⊢ F ∈ S MndHom T ↔ S ∈ Mnd ∧ T ∈ Mnd ∧ F : Base S ⟶ Base T ∧ ∀ x ∈ Base S ∀ y ∈ Base S F ⁡ x + S y = F ⁡ x + T F ⁡ y ∧ F ⁡ 0 ˙ = Y
8 7 simprbi ⊢ F ∈ S MndHom T → F : Base S ⟶ Base T ∧ ∀ x ∈ Base S ∀ y ∈ Base S F ⁡ x + S y = F ⁡ x + T F ⁡ y ∧ F ⁡ 0 ˙ = Y
9 8 simp3d ⊢ F ∈ S MndHom T → F ⁡ 0 ˙ = Y