Metamath Proof Explorer

Theorem c0mhm

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

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

Proof

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