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

Metamath Proof Explorer

Theorem c0snghm

Description: The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
c0snmhm.z ⊢ 𝑍 = ( 0g ‘ 𝑇 )
Assertion c0snghm ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
2 zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
3 zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 c0snmhm.z ⊢ 𝑍 = ( 0g ‘ 𝑇 )
5 grpmnd ⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
6 grpmnd ⊢ ( 𝑇 ∈ Grp → 𝑇 ∈ Mnd )
7 id ⊢ ( 𝐵 = { 𝑍 } → 𝐵 = { 𝑍 } )
8 1 2 3 4 c0snmhm ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )
9 5 6 7 8 syl3an ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )
10 ghmmhmb ⊢ ( ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) → ( 𝑇 GrpHom 𝑆 ) = ( 𝑇 MndHom 𝑆 ) )
11 10 eleq2d ⊢ ( ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
12 11 ancoms ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
13 12 3adant3 ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
14 9 13 mpbird ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) )