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 ) )