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

Metamath Proof Explorer

Theorem c0ghm

Description: The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020)

Ref Expression
Hypotheses c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion c0ghm ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
3 c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 grpmnd ⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
5 grpmnd ⊢ ( 𝑇 ∈ Grp → 𝑇 ∈ Mnd )
6 4 5 anim12i ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) )
7 1 2 3 c0mhm ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) )
8 6 7 syl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) )
9 ghmmhmb ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
10 9 eleq2d ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) ) )
11 8 10 mpbird ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )