Metamath Proof Explorer


Theorem 0ghm

Description: The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses 0ghm.z 0 = ( 0g𝑁 )
0ghm.b 𝐵 = ( Base ‘ 𝑀 )
Assertion 0ghm ( ( 𝑀 ∈ Grp ∧ 𝑁 ∈ Grp ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 GrpHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0ghm.z 0 = ( 0g𝑁 )
2 0ghm.b 𝐵 = ( Base ‘ 𝑀 )
3 grpmnd ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
4 grpmnd ( 𝑁 ∈ Grp → 𝑁 ∈ Mnd )
5 1 2 0mhm ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 MndHom 𝑁 ) )
6 3 4 5 syl2an ( ( 𝑀 ∈ Grp ∧ 𝑁 ∈ Grp ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 MndHom 𝑁 ) )
7 ghmmhmb ( ( 𝑀 ∈ Grp ∧ 𝑁 ∈ Grp ) → ( 𝑀 GrpHom 𝑁 ) = ( 𝑀 MndHom 𝑁 ) )
8 6 7 eleqtrrd ( ( 𝑀 ∈ Grp ∧ 𝑁 ∈ Grp ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 GrpHom 𝑁 ) )