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