Metamath Proof Explorer

Theorem c0mhm

Description: The constant mapping to zero is a monoid homomorphism. (Contributed by AV, 16-Apr-2020)

Ref Expression
Hypotheses c0mhm.b 
|- B = ( Base ` S )
c0mhm.0 
|- .0. = ( 0g ` T )
c0mhm.h 
|- H = ( x e. B |-> .0. )
Assertion c0mhm 
|- ( ( S e. Mnd /\ T e. Mnd ) -> H e. ( S MndHom 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 eqid 
 |-  ( Base ` T ) = ( Base ` T )
5 4 2 mndidcl 
 |-  ( T e. Mnd -> .0. e. ( Base ` T ) )
6 5 adantl 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> .0. e. ( Base ` T ) )
7 6 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ x e. B ) -> .0. e. ( Base ` T ) )
8 7 3 fmptd 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> H : B --> ( Base ` T ) )
9 5 ancli 
 |-  ( T e. Mnd -> ( T e. Mnd /\ .0. e. ( Base ` T ) ) )
10 9 adantl 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( T e. Mnd /\ .0. e. ( Base ` T ) ) )
11 eqid 
 |-  ( +g ` T ) = ( +g ` T )
12 4 11 2 mndlid 
 |-  ( ( T e. Mnd /\ .0. e. ( Base ` T ) ) -> ( .0. ( +g ` T ) .0. ) = .0. )
13 10 12 syl 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( .0. ( +g ` T ) .0. ) = .0. )
14 13 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( .0. ( +g ` T ) .0. ) = .0. )
15 3 a1i 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> H = ( x e. B |-> .0. ) )
16 eqidd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = a ) -> .0. = .0. )
17 simprl 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
18 6 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> .0. e. ( Base ` T ) )
19 15 16 17 18 fvmptd 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` a ) = .0. )
20 eqidd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = b ) -> .0. = .0. )
21 simprr 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
22 15 20 21 18 fvmptd 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` b ) = .0. )
23 19 22 oveq12d 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( ( H ` a ) ( +g ` T ) ( H ` b ) ) = ( .0. ( +g ` T ) .0. ) )
24 eqidd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) /\ x = ( a ( +g ` S ) b ) ) -> .0. = .0. )
25 eqid 
 |-  ( +g ` S ) = ( +g ` S )
26 1 25 mndcl 
 |-  ( ( S e. Mnd /\ a e. B /\ b e. B ) -> ( a ( +g ` S ) b ) e. B )
27 26 3expb 
 |-  ( ( S e. Mnd /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` S ) b ) e. B )
28 27 adantlr 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` S ) b ) e. B )
29 15 24 28 18 fvmptd 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` ( a ( +g ` S ) b ) ) = .0. )
30 14 23 29 3eqtr4rd 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ ( a e. B /\ b e. B ) ) -> ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) )
31 30 ralrimivva 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> A. a e. B A. b e. B ( H ` ( a ( +g ` S ) b ) ) = ( ( H ` a ) ( +g ` T ) ( H ` b ) ) )
32 3 a1i 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> H = ( x e. B |-> .0. ) )
33 eqidd 
 |-  ( ( ( S e. Mnd /\ T e. Mnd ) /\ x = ( 0g ` S ) ) -> .0. = .0. )
34 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
35 1 34 mndidcl 
 |-  ( S e. Mnd -> ( 0g ` S ) e. B )
36 35 adantr 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( 0g ` S ) e. B )
37 32 33 36 6 fvmptd 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( H ` ( 0g ` S ) ) = .0. )
38 8 31 37 3jca 
 |-  ( ( S e. Mnd /\ 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 ) ) /\ ( H ` ( 0g ` S ) ) = .0. ) )
39 38 ancli 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> ( ( S e. Mnd /\ 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 ) ) /\ ( H ` ( 0g ` S ) ) = .0. ) ) )
40 1 4 25 11 34 2 ismhm 
 |-  ( H e. ( S MndHom T ) <-> ( ( S e. Mnd /\ 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 ) ) /\ ( H ` ( 0g ` S ) ) = .0. ) ) )
41 39 40 sylibr 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> H e. ( S MndHom T ) )