Metamath Proof Explorer

Theorem srglmhm

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

Ref Expression
Hypotheses srglmhm.b 
|- B = ( Base ` R )
srglmhm.t 
|- .x. = ( .r ` R )
Assertion srglmhm 
|- ( ( 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 3expa 
 |-  ( ( ( R e. SRing /\ X e. B ) /\ x e. B ) -> ( X .x. x ) e. B )
8 7 fmpttd 
 |-  ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) : B --> B )
9 3anass 
 |-  ( ( X e. B /\ a e. B /\ b e. B ) <-> ( X e. B /\ ( a e. B /\ b e. B ) ) )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 1 10 2 srgdi 
 |-  ( ( R e. SRing /\ ( X e. B /\ a e. B /\ b e. B ) ) -> ( X .x. ( a ( +g ` R ) b ) ) = ( ( X .x. a ) ( +g ` R ) ( X .x. b ) ) )
12 9 11 sylan2br 
 |-  ( ( R e. SRing /\ ( X e. B /\ ( a e. B /\ b e. B ) ) ) -> ( X .x. ( a ( +g ` R ) b ) ) = ( ( X .x. a ) ( +g ` R ) ( X .x. b ) ) )
13 12 anassrs 
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( X .x. ( a ( +g ` R ) b ) ) = ( ( X .x. a ) ( +g ` R ) ( X .x. b ) ) )
14 1 10 srgacl 
 |-  ( ( R e. SRing /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )
15 14 3expb 
 |-  ( ( R e. SRing /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
16 15 adantlr 
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` R ) b ) e. B )
17 oveq2 
 |-  ( x = ( a ( +g ` R ) b ) -> ( X .x. x ) = ( X .x. ( a ( +g ` R ) b ) ) )
18 eqid 
 |-  ( x e. B |-> ( X .x. x ) ) = ( x e. B |-> ( X .x. x ) )
19 ovex 
 |-  ( X .x. ( a ( +g ` R ) b ) ) e. _V
20 17 18 19 fvmpt 
 |-  ( ( a ( +g ` R ) b ) e. B -> ( ( x e. B |-> ( X .x. x ) ) ` ( a ( +g ` R ) b ) ) = ( X .x. ( a ( +g ` R ) b ) ) )
21 16 20 syl 
 |-  ( ( ( R e. SRing /\ X e. B ) /\ ( a e. B /\ b e. B ) ) -> ( ( x e. B |-> ( X .x. x ) ) ` ( a ( +g ` R ) b ) ) = ( X .x. ( a ( +g ` R ) b ) ) )
22 oveq2 
 |-  ( x = a -> ( X .x. x ) = ( X .x. a ) )
23 ovex 
 |-  ( X .x. a ) e. _V
24 22 18 23 fvmpt 
 |-  ( a e. B -> ( ( x e. B |-> ( X .x. x ) ) ` a ) = ( X .x. a ) )
25 oveq2 
 |-  ( x = b -> ( X .x. x ) = ( X .x. b ) )
26 ovex 
 |-  ( X .x. b ) e. _V
27 25 18 26 fvmpt 
 |-  ( b e. B -> ( ( x e. B |-> ( X .x. x ) ) ` b ) = ( X .x. b ) )
28 24 27 oveqan12d 
 |-  ( ( a e. B /\ b e. B ) -> ( ( ( x e. B |-> ( X .x. x ) ) ` a ) ( +g ` R ) ( ( x e. B |-> ( X .x. x ) ) ` b ) ) = ( ( X .x. a ) ( +g ` R ) ( X .x. b ) ) )
29 28 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 ) ) = ( ( X .x. a ) ( +g ` R ) ( X .x. b ) ) )
30 13 21 29 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 ) ) )
31 30 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 ) ) )
32 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
33 1 32 srg0cl 
 |-  ( R e. SRing -> ( 0g ` R ) e. B )
34 33 adantr 
 |-  ( ( R e. SRing /\ X e. B ) -> ( 0g ` R ) e. B )
35 oveq2 
 |-  ( x = ( 0g ` R ) -> ( X .x. x ) = ( X .x. ( 0g ` R ) ) )
36 ovex 
 |-  ( X .x. ( 0g ` R ) ) e. _V
37 35 18 36 fvmpt 
 |-  ( ( 0g ` R ) e. B -> ( ( x e. B |-> ( X .x. x ) ) ` ( 0g ` R ) ) = ( X .x. ( 0g ` R ) ) )
38 34 37 syl 
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( x e. B |-> ( X .x. x ) ) ` ( 0g ` R ) ) = ( X .x. ( 0g ` R ) ) )
39 1 2 32 srgrz 
 |-  ( ( R e. SRing /\ X e. B ) -> ( X .x. ( 0g ` R ) ) = ( 0g ` R ) )
40 38 39 eqtrd 
 |-  ( ( R e. SRing /\ X e. B ) -> ( ( x e. B |-> ( X .x. x ) ) ` ( 0g ` R ) ) = ( 0g ` R ) )
41 8 31 40 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 ) ) )
42 1 1 10 10 32 32 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 ) ) ) )
43 5 41 42 sylanbrc 
 |-  ( ( R e. SRing /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) e. ( R MndHom R ) )