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

Metamath Proof Explorer

Theorem c0mgm

Description: The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion c0mgm ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → 𝐻 ∈ ( 𝑆 MgmHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 c0mhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 c0mhm.0 ⊢ 0 = ( 0g ‘ 𝑇 )
3 c0mhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 mndmgm ⊢ ( 𝑇 ∈ Mnd → 𝑇 ∈ Mgm )
5 4 anim2i ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
7 6 2 mndidcl ⊢ ( 𝑇 ∈ Mnd → 0 ∈ ( Base ‘ 𝑇 ) )
8 7 adantl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → 0 ∈ ( Base ‘ 𝑇 ) )
9 8 adantr ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ 𝑥 ∈ 𝐵 ) → 0 ∈ ( Base ‘ 𝑇 ) )
10 9 3 fmptd ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
11 7 ancli ⊢ ( 𝑇 ∈ Mnd → ( 𝑇 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑇 ) ) )
12 11 adantl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → ( 𝑇 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑇 ) ) )
13 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
14 6 13 2 mndlid ⊢ ( ( 𝑇 ∈ Mnd ∧ 0 ∈ ( Base ‘ 𝑇 ) ) → ( 0 ( +g ‘ 𝑇 ) 0 ) = 0 )
15 12 14 syl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → ( 0 ( +g ‘ 𝑇 ) 0 ) = 0 )
16 15 adantr ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 0 ( +g ‘ 𝑇 ) 0 ) = 0 )
17 3 a1i ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 ) )
18 eqidd ⊢ ( ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑎 ) → 0 = 0 )
19 simprl ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
20 8 adantr ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 0 ∈ ( Base ‘ 𝑇 ) )
21 17 18 19 20 fvmptd ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐻 ‘ 𝑎 ) = 0 )
22 eqidd ⊢ ( ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑏 ) → 0 = 0 )
23 simprr ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
24 17 22 23 20 fvmptd ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐻 ‘ 𝑏 ) = 0 )
25 21 24 oveq12d ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑇 ) ( 𝐻 ‘ 𝑏 ) ) = ( 0 ( +g ‘ 𝑇 ) 0 ) )
26 eqidd ⊢ ( ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑥 = ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) → 0 = 0 )
27 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
28 1 27 mgmcl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ 𝐵 )
29 28 3expb ⊢ ( ( 𝑆 ∈ Mgm ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ 𝐵 )
30 29 adantlr ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ 𝐵 )
31 17 26 30 20 fvmptd ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) = 0 )
32 16 25 31 3eqtr4rd ⊢ ( ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑇 ) ( 𝐻 ‘ 𝑏 ) ) )
33 32 ralrimivva ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑇 ) ( 𝐻 ‘ 𝑏 ) ) )
34 10 33 jca ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑇 ) ( 𝐻 ‘ 𝑏 ) ) ) )
35 1 6 27 13 ismgmhm ⊢ ( 𝐻 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝐻 ‘ ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ) = ( ( 𝐻 ‘ 𝑎 ) ( +g ‘ 𝑇 ) ( 𝐻 ‘ 𝑏 ) ) ) ) )
36 5 34 35 sylanbrc ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mnd ) → 𝐻 ∈ ( 𝑆 MgmHom 𝑇 ) )