This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1maplmhm

Description: The function F mapping polynomials p to their subring evaluation at a given point A is a module homomorphism, when considering the subring algebra. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses evls1maprhm.q 
|- O = ( R evalSub1 S )
evls1maprhm.p 
|- P = ( Poly1 ` ( R |`s S ) )
evls1maprhm.b 
|- B = ( Base ` R )
evls1maprhm.u 
|- U = ( Base ` P )
evls1maprhm.r 
|- ( ph -> R e. CRing )
evls1maprhm.s 
|- ( ph -> S e. ( SubRing ` R ) )
evls1maprhm.y 
|- ( ph -> X e. B )
evls1maprhm.f 
|- F = ( p e. U |-> ( ( O ` p ) ` X ) )
evls1maplmhm.1 
|- A = ( ( subringAlg ` R ) ` S )
Assertion evls1maplmhm 
|- ( ph -> F e. ( P LMHom A ) )

Proof

Step Hyp Ref Expression
1 evls1maprhm.q 
 |-  O = ( R evalSub1 S )
2 evls1maprhm.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 evls1maprhm.b 
 |-  B = ( Base ` R )
4 evls1maprhm.u 
 |-  U = ( Base ` P )
5 evls1maprhm.r 
 |-  ( ph -> R e. CRing )
6 evls1maprhm.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 evls1maprhm.y 
 |-  ( ph -> X e. B )
8 evls1maprhm.f 
 |-  F = ( p e. U |-> ( ( O ` p ) ` X ) )
9 evls1maplmhm.1 
 |-  A = ( ( subringAlg ` R ) ` S )
10 eqid 
 |-  ( R |`s S ) = ( R |`s S )
11 10 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
12 6 11 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
13 2 ply1lmod 
 |-  ( ( R |`s S ) e. Ring -> P e. LMod )
14 12 13 syl 
 |-  ( ph -> P e. LMod )
15 9 sralmod 
 |-  ( S e. ( SubRing ` R ) -> A e. LMod )
16 6 15 syl 
 |-  ( ph -> A e. LMod )
17 1 2 3 4 5 6 7 8 evls1maprhm 
 |-  ( ph -> F e. ( P RingHom R ) )
18 rhmghm 
 |-  ( F e. ( P RingHom R ) -> F e. ( P GrpHom R ) )
19 17 18 syl 
 |-  ( ph -> F e. ( P GrpHom R ) )
20 4 a1i 
 |-  ( ph -> U = ( Base ` P ) )
21 3 a1i 
 |-  ( ph -> B = ( Base ` R ) )
22 9 a1i 
 |-  ( ph -> A = ( ( subringAlg ` R ) ` S ) )
23 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
24 6 23 syl 
 |-  ( ph -> S C_ B )
25 24 3 sseqtrdi 
 |-  ( ph -> S C_ ( Base ` R ) )
26 22 25 srabase 
 |-  ( ph -> ( Base ` R ) = ( Base ` A ) )
27 3 26 eqtrid 
 |-  ( ph -> B = ( Base ` A ) )
28 eqidd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` P ) y ) )
29 22 25 sraaddg 
 |-  ( ph -> ( +g ` R ) = ( +g ` A ) )
30 29 oveqdr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` A ) y ) )
31 20 21 20 27 28 30 ghmpropd 
 |-  ( ph -> ( P GrpHom R ) = ( P GrpHom A ) )
32 19 31 eleqtrd 
 |-  ( ph -> F e. ( P GrpHom A ) )
33 22 25 srasca 
 |-  ( ph -> ( R |`s S ) = ( Scalar ` A ) )
34 ovex 
 |-  ( R |`s S ) e. _V
35 2 ply1sca 
 |-  ( ( R |`s S ) e. _V -> ( R |`s S ) = ( Scalar ` P ) )
36 34 35 mp1i 
 |-  ( ph -> ( R |`s S ) = ( Scalar ` P ) )
37 33 36 eqtr3d 
 |-  ( ph -> ( Scalar ` A ) = ( Scalar ` P ) )
38 fveq2 
 |-  ( p = ( k ( .s ` P ) x ) -> ( O ` p ) = ( O ` ( k ( .s ` P ) x ) ) )
39 38 fveq1d 
 |-  ( p = ( k ( .s ` P ) x ) -> ( ( O ` p ) ` X ) = ( ( O ` ( k ( .s ` P ) x ) ) ` X ) )
40 14 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> P e. LMod )
41 simplr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> k e. ( Base ` ( Scalar ` P ) ) )
42 simpr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> x e. U )
43 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
44 eqid 
 |-  ( .s ` P ) = ( .s ` P )
45 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
46 4 43 44 45 lmodvscl 
 |-  ( ( P e. LMod /\ k e. ( Base ` ( Scalar ` P ) ) /\ x e. U ) -> ( k ( .s ` P ) x ) e. U )
47 40 41 42 46 syl3anc 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( k ( .s ` P ) x ) e. U )
48 fvexd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( ( O ` ( k ( .s ` P ) x ) ) ` X ) e. _V )
49 8 39 47 48 fvmptd3 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( F ` ( k ( .s ` P ) x ) ) = ( ( O ` ( k ( .s ` P ) x ) ) ` X ) )
50 eqid 
 |-  ( .r ` R ) = ( .r ` R )
51 5 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> R e. CRing )
52 6 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> S e. ( SubRing ` R ) )
53 10 3 ressbas2 
 |-  ( S C_ B -> S = ( Base ` ( R |`s S ) ) )
54 24 53 syl 
 |-  ( ph -> S = ( Base ` ( R |`s S ) ) )
55 36 fveq2d 
 |-  ( ph -> ( Base ` ( R |`s S ) ) = ( Base ` ( Scalar ` P ) ) )
56 54 55 eqtr2d 
 |-  ( ph -> ( Base ` ( Scalar ` P ) ) = S )
57 56 eqimssd 
 |-  ( ph -> ( Base ` ( Scalar ` P ) ) C_ S )
58 57 sselda 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) -> k e. S )
59 58 adantr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> k e. S )
60 7 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> X e. B )
61 1 3 2 10 4 44 50 51 52 59 42 60 evls1vsca 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( ( O ` ( k ( .s ` P ) x ) ) ` X ) = ( k ( .r ` R ) ( ( O ` x ) ` X ) ) )
62 22 25 sravsca 
 |-  ( ph -> ( .r ` R ) = ( .s ` A ) )
63 62 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( .r ` R ) = ( .s ` A ) )
64 eqidd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> k = k )
65 fveq2 
 |-  ( p = x -> ( O ` p ) = ( O ` x ) )
66 65 fveq1d 
 |-  ( p = x -> ( ( O ` p ) ` X ) = ( ( O ` x ) ` X ) )
67 fvexd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( ( O ` x ) ` X ) e. _V )
68 8 66 42 67 fvmptd3 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( F ` x ) = ( ( O ` x ) ` X ) )
69 68 eqcomd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( ( O ` x ) ` X ) = ( F ` x ) )
70 63 64 69 oveq123d 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( k ( .r ` R ) ( ( O ` x ) ` X ) ) = ( k ( .s ` A ) ( F ` x ) ) )
71 49 61 70 3eqtrd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. U ) -> ( F ` ( k ( .s ` P ) x ) ) = ( k ( .s ` A ) ( F ` x ) ) )
72 71 anasss 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ x e. U ) ) -> ( F ` ( k ( .s ` P ) x ) ) = ( k ( .s ` A ) ( F ` x ) ) )
73 72 ralrimivva 
 |-  ( ph -> A. k e. ( Base ` ( Scalar ` P ) ) A. x e. U ( F ` ( k ( .s ` P ) x ) ) = ( k ( .s ` A ) ( F ` x ) ) )
74 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
75 eqid 
 |-  ( .s ` A ) = ( .s ` A )
76 43 74 45 4 44 75 islmhm 
 |-  ( F e. ( P LMHom A ) <-> ( ( P e. LMod /\ A e. LMod ) /\ ( F e. ( P GrpHom A ) /\ ( Scalar ` A ) = ( Scalar ` P ) /\ A. k e. ( Base ` ( Scalar ` P ) ) A. x e. U ( F ` ( k ( .s ` P ) x ) ) = ( k ( .s ` A ) ( F ` x ) ) ) ) )
77 76 biimpri 
 |-  ( ( ( P e. LMod /\ A e. LMod ) /\ ( F e. ( P GrpHom A ) /\ ( Scalar ` A ) = ( Scalar ` P ) /\ A. k e. ( Base ` ( Scalar ` P ) ) A. x e. U ( F ` ( k ( .s ` P ) x ) ) = ( k ( .s ` A ) ( F ` x ) ) ) ) -> F e. ( P LMHom A ) )
78 14 16 32 37 73 77 syl23anc 
 |-  ( ph -> F e. ( P LMHom A ) )