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 𝑁 ) ) |
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 𝑁 ) ) |