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. = ( 0g ` S )
zrrhm.h
|- H = ( x e. B |-> .0. )
c0snmhm.z
|- Z = ( 0g ` T )
Assertion c0snmhm
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b
 |-  B = ( Base ` T )
2 zrrhm.0
 |-  .0. = ( 0g ` S )
3 zrrhm.h
 |-  H = ( x e. B |-> .0. )
4 c0snmhm.z
 |-  Z = ( 0g ` T )
5 pm3.22
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( T e. Mnd /\ S e. Mnd ) )
6 5 3adant3
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( T e. Mnd /\ S e. Mnd ) )
7 simp1
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> S e. Mnd )
8 mndmgm
 |-  ( T e. Mnd -> T e. Mgm )
9 8 3ad2ant2
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> T e. Mgm )
10 fveq2
 |-  ( B = { Z } -> ( # ` B ) = ( # ` { Z } ) )
11 4 fvexi
 |-  Z e. _V
12 hashsng
 |-  ( Z e. _V -> ( # ` { Z } ) = 1 )
13 11 12 ax-mp
 |-  ( # ` { Z } ) = 1
14 10 13 eqtrdi
 |-  ( B = { Z } -> ( # ` B ) = 1 )
15 14 3ad2ant3
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( # ` B ) = 1 )
16 1 2 3 c0snmgmhm
 |-  ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom S ) )
17 7 9 15 16 syl3anc
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MgmHom S ) )
18 3 a1i
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H = ( x e. B |-> .0. ) )
19 eqidd
 |-  ( ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) /\ x = Z ) -> .0. = .0. )
20 11 snid
 |-  Z e. { Z }
21 eleq2
 |-  ( B = { Z } -> ( Z e. B <-> Z e. { Z } ) )
22 20 21 mpbiri
 |-  ( B = { Z } -> Z e. B )
23 22 3ad2ant3
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> Z e. B )
24 eqid
 |-  ( Base ` S ) = ( Base ` S )
25 24 2 mndidcl
 |-  ( S e. Mnd -> .0. e. ( Base ` S ) )
26 25 3ad2ant1
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> .0. e. ( Base ` S ) )
27 18 19 23 26 fvmptd
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( H ` Z ) = .0. )
28 17 27 jca
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> ( H e. ( T MgmHom S ) /\ ( H ` Z ) = .0. ) )
29 eqid
 |-  ( +g ` T ) = ( +g ` T )
30 eqid
 |-  ( +g ` S ) = ( +g ` S )
31 1 24 29 30 4 2 ismhm0
 |-  ( H e. ( T MndHom S ) <-> ( ( T e. Mnd /\ S e. Mnd ) /\ ( H e. ( T MgmHom S ) /\ ( H ` Z ) = .0. ) ) )
32 6 28 31 sylanbrc
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) )