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 ⊢ B = Base S
c0mhm.0 ⊢ 0 ˙ = 0 T
c0mhm.h ⊢ H = x ∈ B ⟼ 0 ˙
Assertion c0mhm ⊢ S ∈ Mnd ∧ T ∈ Mnd → H ∈ S MndHom T

Proof

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