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 ⊢ 𝐵 = ( Base ‘ 𝑇 )
zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
c0snmhm.z ⊢ 𝑍 = ( 0g ‘ 𝑇 )
Assertion c0snmhm ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
2 zrrhm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
3 zrrhm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4 c0snmhm.z ⊢ 𝑍 = ( 0g ‘ 𝑇 )
5 pm3.22 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( 𝑇 ∈ Mnd ∧ 𝑆 ∈ Mnd ) )
6 5 3adant3 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → ( 𝑇 ∈ Mnd ∧ 𝑆 ∈ Mnd ) )
7 simp1 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝑆 ∈ Mnd )
8 mndmgm ⊢ ( 𝑇 ∈ Mnd → 𝑇 ∈ Mgm )
9 8 3ad2ant2 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝑇 ∈ Mgm )
10 fveq2 ⊢ ( 𝐵 = { 𝑍 } → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ { 𝑍 } ) )
11 4 fvexi ⊢ 𝑍 ∈ V
12 hashsng ⊢ ( 𝑍 ∈ V → ( ♯ ‘ { 𝑍 } ) = 1 )
13 11 12 ax-mp ⊢ ( ♯ ‘ { 𝑍 } ) = 1
14 10 13 eqtrdi ⊢ ( 𝐵 = { 𝑍 } → ( ♯ ‘ 𝐵 ) = 1 )
15 14 3ad2ant3 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → ( ♯ ‘ 𝐵 ) = 1 )
16 1 2 3 c0snmgmhm ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mgm ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) )
17 7 9 15 16 syl3anc ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) )
18 3 a1i ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 ) )
19 eqidd ⊢ ( ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) ∧ 𝑥 = 𝑍 ) → 0 = 0 )
20 11 snid ⊢ 𝑍 ∈ { 𝑍 }
21 eleq2 ⊢ ( 𝐵 = { 𝑍 } → ( 𝑍 ∈ 𝐵 ↔ 𝑍 ∈ { 𝑍 } ) )
22 20 21 mpbiri ⊢ ( 𝐵 = { 𝑍 } → 𝑍 ∈ 𝐵 )
23 22 3ad2ant3 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝑍 ∈ 𝐵 )
24 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
25 24 2 mndidcl ⊢ ( 𝑆 ∈ Mnd → 0 ∈ ( Base ‘ 𝑆 ) )
26 25 3ad2ant1 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 0 ∈ ( Base ‘ 𝑆 ) )
27 18 19 23 26 fvmptd ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → ( 𝐻 ‘ 𝑍 ) = 0 )
28 17 27 jca ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → ( 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) ∧ ( 𝐻 ‘ 𝑍 ) = 0 ) )
29 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
30 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
31 1 24 29 30 4 2 ismhm0 ⊢ ( 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ↔ ( ( 𝑇 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝐻 ∈ ( 𝑇 MgmHom 𝑆 ) ∧ ( 𝐻 ‘ 𝑍 ) = 0 ) ) )
32 6 28 31 sylanbrc ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )