Metamath Proof Explorer

Theorem c0snmgmhm

Description: The constant mapping to zero is a magma homomorphism from a magma with one element 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. )
Assertion c0snmgmhm 
|- ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom 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 mndmgm 
 |-  ( S e. Mnd -> S e. Mgm )
5 4 anim1i 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> ( S e. Mgm /\ T e. Mgm ) )
6 5 3adant3 
 |-  ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( S e. Mgm /\ T e. Mgm ) )
7 6 ancomd 
 |-  ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( T e. Mgm /\ S e. Mgm ) )
8 1 fvexi 
 |-  B e. _V
9 hash1snb 
 |-  ( B e. _V -> ( ( # ` B ) = 1 <-> E. b B = { b } ) )
10 8 9 ax-mp 
 |-  ( ( # ` B ) = 1 <-> E. b B = { b } )
11 eqid 
 |-  ( Base ` S ) = ( Base ` S )
12 11 2 mndidcl 
 |-  ( S e. Mnd -> .0. e. ( Base ` S ) )
13 12 adantr 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> .0. e. ( Base ` S ) )
14 13 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> .0. e. ( Base ` S ) )
15 14 adantr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ x e. B ) -> .0. e. ( Base ` S ) )
16 15 3 fmptd 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> H : B --> ( Base ` S ) )
17 3 a1i 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> H = ( x e. B |-> .0. ) )
18 eqidd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ x = b ) -> .0. = .0. )
19 vsnid 
 |-  b e. { b }
20 19 a1i 
 |-  ( B = { b } -> b e. { b } )
21 eleq2 
 |-  ( B = { b } -> ( b e. B <-> b e. { b } ) )
22 20 21 mpbird 
 |-  ( B = { b } -> b e. B )
23 22 adantl 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> b e. B )
24 17 18 23 14 fvmptd 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` b ) = .0. )
25 simpr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` b ) = .0. )
26 25 25 oveq12d 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( ( H ` b ) ( +g ` S ) ( H ` b ) ) = ( .0. ( +g ` S ) .0. ) )
27 eqid 
 |-  ( +g ` S ) = ( +g ` S )
28 11 27 2 mndlid 
 |-  ( ( S e. Mnd /\ .0. e. ( Base ` S ) ) -> ( .0. ( +g ` S ) .0. ) = .0. )
29 12 28 mpdan 
 |-  ( S e. Mnd -> ( .0. ( +g ` S ) .0. ) = .0. )
30 29 adantr 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> ( .0. ( +g ` S ) .0. ) = .0. )
31 30 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( .0. ( +g ` S ) .0. ) = .0. )
32 31 adantr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( .0. ( +g ` S ) .0. ) = .0. )
33 simpr 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> T e. Mgm )
34 33 adantr 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> T e. Mgm )
35 34 adantr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> T e. Mgm )
36 simpr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> b e. B )
37 eqid 
 |-  ( +g ` T ) = ( +g ` T )
38 1 37 mgmcl 
 |-  ( ( T e. Mgm /\ b e. B /\ b e. B ) -> ( b ( +g ` T ) b ) e. B )
39 35 36 36 38 syl3anc 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( b ( +g ` T ) b ) e. B )
40 eleq2 
 |-  ( B = { b } -> ( ( b ( +g ` T ) b ) e. B <-> ( b ( +g ` T ) b ) e. { b } ) )
41 elsni 
 |-  ( ( b ( +g ` T ) b ) e. { b } -> ( b ( +g ` T ) b ) = b )
42 40 41 syl6bi 
 |-  ( B = { b } -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) )
43 42 adantl 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) )
44 43 adantr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( ( b ( +g ` T ) b ) e. B -> ( b ( +g ` T ) b ) = b ) )
45 39 44 mpd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ b e. B ) -> ( b ( +g ` T ) b ) = b )
46 23 45 mpdan 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( b ( +g ` T ) b ) = b )
47 46 fveq2d 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` ( b ( +g ` T ) b ) ) = ( H ` b ) )
48 47 adantr 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` ( b ( +g ` T ) b ) ) = ( H ` b ) )
49 48 25 eqtr2d 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> .0. = ( H ` ( b ( +g ` T ) b ) ) )
50 26 32 49 3eqtrrd 
 |-  ( ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) /\ ( H ` b ) = .0. ) -> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) )
51 24 50 mpdan 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) )
52 id 
 |-  ( B = { b } -> B = { b } )
53 52 raleqdv 
 |-  ( B = { b } -> ( A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) )
54 52 53 raleqbidv 
 |-  ( B = { b } -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) )
55 54 adantl 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) )
56 fvoveq1 
 |-  ( a = b -> ( H ` ( a ( +g ` T ) c ) ) = ( H ` ( b ( +g ` T ) c ) ) )
57 fveq2 
 |-  ( a = b -> ( H ` a ) = ( H ` b ) )
58 57 oveq1d 
 |-  ( a = b -> ( ( H ` a ) ( +g ` S ) ( H ` c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) )
59 56 58 eqeq12d 
 |-  ( a = b -> ( ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) ) )
60 oveq2 
 |-  ( c = b -> ( b ( +g ` T ) c ) = ( b ( +g ` T ) b ) )
61 60 fveq2d 
 |-  ( c = b -> ( H ` ( b ( +g ` T ) c ) ) = ( H ` ( b ( +g ` T ) b ) ) )
62 fveq2 
 |-  ( c = b -> ( H ` c ) = ( H ` b ) )
63 62 oveq2d 
 |-  ( c = b -> ( ( H ` b ) ( +g ` S ) ( H ` c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) )
64 61 63 eqeq12d 
 |-  ( c = b -> ( ( H ` ( b ( +g ` T ) c ) ) = ( ( H ` b ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) )
65 59 64 2ralsng 
 |-  ( ( b e. _V /\ b e. _V ) -> ( A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) )
66 65 el2v 
 |-  ( A. a e. { b } A. c e. { b } ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) )
67 55 66 bitrdi 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) <-> ( H ` ( b ( +g ` T ) b ) ) = ( ( H ` b ) ( +g ` S ) ( H ` b ) ) ) )
68 51 67 mpbird 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) )
69 16 68 jca 
 |-  ( ( ( S e. Mnd /\ T e. Mgm ) /\ B = { b } ) -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) )
70 69 ex 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> ( B = { b } -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) )
71 70 exlimdv 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> ( E. b B = { b } -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) )
72 10 71 syl5bi 
 |-  ( ( S e. Mnd /\ T e. Mgm ) -> ( ( # ` B ) = 1 -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) )
73 72 3impia 
 |-  ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) )
74 1 11 37 27 ismgmhm 
 |-  ( H e. ( T MgmHom S ) <-> ( ( T e. Mgm /\ S e. Mgm ) /\ ( H : B --> ( Base ` S ) /\ A. a e. B A. c e. B ( H ` ( a ( +g ` T ) c ) ) = ( ( H ` a ) ( +g ` S ) ( H ` c ) ) ) ) )
75 7 73 74 sylanbrc 
 |-  ( ( S e. Mnd /\ T e. Mgm /\ ( # ` B ) = 1 ) -> H e. ( T MgmHom S ) )