Metamath Proof Explorer


Theorem srgrmhm

Description: Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm . (Contributed by AV, 23-Aug-2019)

Ref Expression
Hypotheses srglmhm.b
|- B = ( Base ` R )
srglmhm.t
|- .x. = ( .r ` R )
Assertion srgrmhm
|- ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R MndHom R ) )

Proof

Step Hyp Ref Expression
1 srglmhm.b
 |-  B = ( Base ` R )
2 srglmhm.t
 |-  .x. = ( .r ` R )
3 srgmnd
 |-  ( R e. SRing -> R e. Mnd )
4 3 3 jca
 |-  ( R e. SRing -> ( R e. Mnd /\ R e. Mnd ) )
5 4 adantr
 |-  ( ( R e. SRing /\ X e. B ) -> ( R e. Mnd /\ R e. Mnd ) )
6 1 2 srgcl
 |-  ( ( R e. SRing /\ x e. B /\ X e. B ) -> ( x .x. X ) e. B )
7 6 3com23
 |-  ( ( R e. SRing /\ X e. B /\ x e. B ) -> ( x .x. X ) e. B )
8 7 3expa
 |-  ( ( ( R e. SRing /\ X e. B ) /\ x e. B ) -> ( x .x. X ) e. B )
9 8 fmpttd
 |-  ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) : B --> B )
10 3anrot
 |-  ( ( X e. B /\ a e. B /\ b e. B ) <-> ( a e. B /\ b e. B /\ X e. B ) )
11 3anass
 |-  ( ( X e. B /\ a e. B /\ b e. B ) <-> ( X e. B /\ ( a e. B /\ b e. B ) ) )
12 10 11 bitr3i
 |-  ( ( a e. B /\ b e. B /\ X e. B ) <-> ( X e. B /\ ( a e. B /\ b e. B ) ) )
13 eqid
 |-  ( +g ` R ) = ( +g ` R )
14 1 13 2 srgdir
 |-  ( ( R e. SRing /\ ( a e. B /\ b e. B /\ X e. B ) ) -> ( ( a ( +g ` R ) b ) .x. X ) = ( ( a .x. X ) ( +g ` R ) ( b .x. X ) ) )
15 12 14 sylan2br
 |-  ( ( R e. SRing /\ ( X e. B /\ ( a e. B /\ b e. B ) ) ) -> ( ( a ( +g ` R ) b ) .x. X ) = ( ( a .x. X ) ( +g ` R ) ( b .x. X ) ) )
16 15 anassrs
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( ( a ( +g ` R ) b ) .x. X ) = ( ( a .x. X ) ( +g ` R ) ( b .x. X ) ) )
17 1 13 srgacl
 |-  ( ( R e. SRing /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )
18 17 3expb
 |-  ( ( R e. SRing /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
19 18 adantlr
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
20 oveq1
 |-  ( x = ( a ( +g ` R ) b ) -> ( x .x. X ) = ( ( a ( +g ` R ) b ) .x. X ) )
21 eqid
 |-  ( x e. B |-> ( x .x. X ) ) = ( x e. B |-> ( x .x. X ) )
22 ovex
 |-  ( ( a ( +g ` R ) b ) .x. X ) e. _V
23 20 21 22 fvmpt
 |-  ( ( a ( +g ` R ) b ) e. B -> ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( a ( +g ` R ) b ) .x. X ) )
24 19 23 syl
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( a ( +g ` R ) b ) .x. X ) )
25 oveq1
 |-  ( x = a -> ( x .x. X ) = ( a .x. X ) )
26 ovex
 |-  ( a .x. X ) e. _V
27 25 21 26 fvmpt
 |-  ( a e. B -> ( ( x e. B |-> ( x .x. X ) ) ` a ) = ( a .x. X ) )
28 oveq1
 |-  ( x = b -> ( x .x. X ) = ( b .x. X ) )
29 ovex
 |-  ( b .x. X ) e. _V
30 28 21 29 fvmpt
 |-  ( b e. B -> ( ( x e. B |-> ( x .x. X ) ) ` b ) = ( b .x. X ) )
31 27 30 oveqan12d
 |-  ( ( a e. B /\ b e. B ) -> ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) = ( ( a .x. X ) ( +g ` R ) ( b .x. X ) ) )
32 31 adantl
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) = ( ( a .x. X ) ( +g ` R ) ( b .x. X ) ) )
33 16 24 32 3eqtr4d
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) )
34 33 ralrimivva
 |-  ( ( R e. SRing /\ X e. B ) -> A. a e. B A. b e. B ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) )
35 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
36 1 35 srg0cl
 |-  ( R e. SRing -> ( 0g ` R ) e. B )
37 36 adantr
 |-  ( ( R e. SRing /\ X e. B ) -> ( 0g ` R ) e. B )
38 oveq1
 |-  ( x = ( 0g ` R ) -> ( x .x. X ) = ( ( 0g ` R ) .x. X ) )
39 ovex
 |-  ( ( 0g ` R ) .x. X ) e. _V
40 38 21 39 fvmpt
 |-  ( ( 0g ` R ) e. B -> ( ( x e. B |-> ( x .x. X ) ) ` ( 0g ` R ) ) = ( ( 0g ` R ) .x. X ) )
41 37 40 syl
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( x e. B |-> ( x .x. X ) ) ` ( 0g ` R ) ) = ( ( 0g ` R ) .x. X ) )
42 1 2 35 srglz
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( 0g ` R ) .x. X ) = ( 0g ` R ) )
43 41 42 eqtrd
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( x e. B |-> ( x .x. X ) ) ` ( 0g ` R ) ) = ( 0g ` R ) )
44 9 34 43 3jca
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( x e. B |-> ( x .x. X ) ) : B --> B /\ A. a e. B A. b e. B ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) /\ ( ( x e. B |-> ( x .x. X ) ) ` ( 0g ` R ) ) = ( 0g ` R ) ) )
45 1 1 13 13 35 35 ismhm
 |-  ( ( x e. B |-> ( x .x. X ) ) e. ( R MndHom R ) <-> ( ( R e. Mnd /\ R e. Mnd ) /\ ( ( x e. B |-> ( x .x. X ) ) : B --> B /\ A. a e. B A. b e. B ( ( x e. B |-> ( x .x. X ) ) ` ( a ( +g ` R ) b ) ) = ( ( ( x e. B |-> ( x .x. X ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( x .x. X ) ) ` b ) ) /\ ( ( x e. B |-> ( x .x. X ) ) ` ( 0g ` R ) ) = ( 0g ` R ) ) ) )
46 5 44 45 sylanbrc
 |-  ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R MndHom R ) )