Metamath Proof Explorer

Theorem c0snmhm

Description: The constant mapping to zero is a monoid homomorphism from the trivial monoid (consisting of the zero only) to any monoid. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ⊢ B = Base T
zrrhm.0 ⊢ 0 ˙ = 0 S
zrrhm.h ⊢ H = x ∈ B ⟼ 0 ˙
c0snmhm.z ⊢ Z = 0 T
Assertion c0snmhm ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H ∈ T MndHom S

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢ B = Base T
2 zrrhm.0 ⊢ 0 ˙ = 0 S
3 zrrhm.h ⊢ H = x ∈ B ⟼ 0 ˙
4 c0snmhm.z ⊢ Z = 0 T
5 pm3.22 ⊢ S ∈ Mnd ∧ T ∈ Mnd → T ∈ Mnd ∧ S ∈ Mnd
6 5 3adant3 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → T ∈ Mnd ∧ S ∈ Mnd
7 simp1 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → S ∈ Mnd
8 mndmgm ⊢ T ∈ Mnd → T ∈ Mgm
9 8 3ad2ant2 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → T ∈ Mgm
10 fveq2 ⊢ B = Z → B = Z
11 4 fvexi ⊢ Z ∈ V
12 hashsng ⊢ Z ∈ V → Z = 1
13 11 12 ax-mp ⊢ Z = 1
14 10 13 eqtrdi ⊢ B = Z → B = 1
15 14 3ad2ant3 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → B = 1
16 1 2 3 c0snmgmhm ⊢ S ∈ Mnd ∧ T ∈ Mgm ∧ B = 1 → H ∈ T MgmHom S
17 7 9 15 16 syl3anc ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H ∈ T MgmHom S
18 3 a1i ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H = x ∈ B ⟼ 0 ˙
19 eqidd ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z ∧ x = Z → 0 ˙ = 0 ˙
20 11 snid ⊢ Z ∈ Z
21 eleq2 ⊢ B = Z → Z ∈ B ↔ Z ∈ Z
22 20 21 mpbiri ⊢ B = Z → Z ∈ B
23 22 3ad2ant3 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → Z ∈ B
24 eqid ⊢ Base S = Base S
25 24 2 mndidcl ⊢ S ∈ Mnd → 0 ˙ ∈ Base S
26 25 3ad2ant1 ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → 0 ˙ ∈ Base S
27 18 19 23 26 fvmptd ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H ⁡ Z = 0 ˙
28 17 27 jca ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H ∈ T MgmHom S ∧ H ⁡ Z = 0 ˙
29 eqid ⊢ + T = + T
30 eqid ⊢ + S = + S
31 1 24 29 30 4 2 ismhm0 ⊢ H ∈ T MndHom S ↔ T ∈ Mnd ∧ S ∈ Mnd ∧ H ∈ T MgmHom S ∧ H ⁡ Z = 0 ˙
32 6 28 31 sylanbrc ⊢ S ∈ Mnd ∧ T ∈ Mnd ∧ B = Z → H ∈ T MndHom S