Theorem mhm0

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

	Ref	Expression
Hypotheses	mhm0.z	⊢ 0 = ( 0g ‘ 𝑆 )
	mhm0.y	⊢ 𝑌 = ( 0g ‘ 𝑇 )
Assertion	mhm0	⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 ‘ 0 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		mhm0.z	⊢ 0 = ( 0g ‘ 𝑆 )
2		mhm0.y	⊢ 𝑌 = ( 0g ‘ 𝑇 )
3		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
4		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
6		eqid	⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
7	3 4 5 6 1 2	ismhm	⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
8	7	simprbi	⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) )
9	8	simp3d	⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 ‘ 0 ) = 𝑌 )