Metamath Proof Explorer

Theorem c0mgm

Description: The constant mapping to zero is a magma homomorphism into a monoid. Remark: Instead of the assumption that T is a monoid, it would be sufficient that T is a magma with a right or left identity. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses c0mhm.b 
|- B = ( Base ` S )
c0mhm.0 
|- .0. = ( 0g ` T )
c0mhm.h 
|- H = ( x e. B |-> .0. )
Assertion c0mgm 
|- ( ( S e. Mgm /\ T e. Mnd ) -> H e. ( S MgmHom T ) )

Proof

Step Hyp Ref Expression
1 c0mhm.b 
 |-  B = ( Base ` S )
2 c0mhm.0 
 |-  .0. = ( 0g ` T )
3 c0mhm.h 
 |-  H = ( x e. B |-> .0. )
4 mndmgm 
 |-  ( T e. Mnd -> T e. Mgm )
5 4 anim2i 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> ( S e. Mgm /\ T e. Mgm ) )
6 eqid 
 |-  ( Base ` T ) = ( Base ` T )
7 6 2 mndidcl 
 |-  ( T e. Mnd -> .0. e. ( Base ` T ) )
8 7 adantl 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> .0. e. ( Base ` T ) )
9 8 adantr 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ x e. B ) -> .0. e. ( Base ` T ) )
10 9 3 fmptd 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> H : B --> ( Base ` T ) )
11 7 ancli 
 |-  ( T e. Mnd -> ( T e. Mnd /\ .0. e. ( Base ` T ) ) )
12 11 adantl 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> ( T e. Mnd /\ .0. e. ( Base ` T ) ) )
13 eqid 
 |-  ( +g ` T ) = ( +g ` T )
14 6 13 2 mndlid 
 |-  ( ( T e. Mnd /\ .0. e. ( Base ` T ) ) -> ( .0. ( +g ` T ) .0. ) = .0. )
15 12 14 syl 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> ( .0. ( +g ` T ) .0. ) = .0. )
16 15 adantr 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( .0. ( +g ` T ) .0. ) = .0. )
17 3 a1i 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> H = ( x e. B |-> .0. ) )
18 eqidd 
 |-  ( ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = a ) -> .0. = .0. )
19 simprl 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
20 8 adantr 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> .0. e. ( Base ` T ) )
21 17 18 19 20 fvmptd 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` a ) = .0. )
22 eqidd 
 |-  ( ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = b ) -> .0. = .0. )
23 simprr 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
24 17 22 23 20 fvmptd 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` b ) = .0. )
25 21 24 oveq12d 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( ( H ` a ) ( +g ` T ) ( H ` b ) ) = ( .0. ( +g ` T ) .0. ) )
26 eqidd 
 |-  ( ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = ( a ( +g ` S ) b ) ) -> .0. = .0. )
27 eqid 
 |-  ( +g ` S ) = ( +g ` S )
28 1 27 mgmcl 
 |-  ( ( S e. Mgm /\ a e. B /\ b e. B ) -> ( a ( +g ` S ) b ) e. B )
29 28 3expb 
 |-  ( ( S e. Mgm /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` S ) b ) e. B )
30 29 adantlr 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` S ) b ) e. B )
31 17 26 30 20 fvmptd 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` ( a ( +g ` S ) b ) ) = .0. )
32 16 25 31 3eqtr4rd 
 |-  ( ( ( S e. Mgm /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) )
33 32 ralrimivva 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> A. a e. B A. b e. B ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) )
34 10 33 jca 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> ( H : B --> ( Base ` T ) /\ A. a e. B A. b e. B ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) ) )
35 1 6 27 13 ismgmhm 
 |-  ( H e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( H : B --> ( Base ` T ) /\ A. a e. B A. b e. B ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) ) ) )
36 5 34 35 sylanbrc 
 |-  ( ( S e. Mgm /\ T e. Mnd ) -> H e. ( S MgmHom T ) )