Metamath Proof Explorer

Theorem asclply1subcl

Description: Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses asclply1subcl.1 
|- A = ( algSc ` V )
asclply1subcl.2 
|- U = ( R |`s S )
asclply1subcl.3 
|- V = ( Poly1 ` R )
asclply1subcl.4 
|- W = ( Poly1 ` U )
asclply1subcl.5 
|- P = ( Base ` W )
asclply1subcl.6 
|- ( ph -> S e. ( SubRing ` R ) )
asclply1subcl.7 
|- ( ph -> Z e. S )
Assertion asclply1subcl 
|- ( ph -> ( A ` Z ) e. P )

Proof

Step Hyp Ref Expression
1 asclply1subcl.1 
 |-  A = ( algSc ` V )
2 asclply1subcl.2 
 |-  U = ( R |`s S )
3 asclply1subcl.3 
 |-  V = ( Poly1 ` R )
4 asclply1subcl.4 
 |-  W = ( Poly1 ` U )
5 asclply1subcl.5 
 |-  P = ( Base ` W )
6 asclply1subcl.6 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 asclply1subcl.7 
 |-  ( ph -> Z e. S )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ ( Base ` R ) )
10 6 9 syl 
 |-  ( ph -> S C_ ( Base ` R ) )
11 10 7 sseldd 
 |-  ( ph -> Z e. ( Base ` R ) )
12 subrgrcl 
 |-  ( S e. ( SubRing ` R ) -> R e. Ring )
13 3 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` V ) )
14 6 12 13 3syl 
 |-  ( ph -> R = ( Scalar ` V ) )
15 14 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` V ) ) )
16 11 15 eleqtrd 
 |-  ( ph -> Z e. ( Base ` ( Scalar ` V ) ) )
17 eqid 
 |-  ( Scalar ` V ) = ( Scalar ` V )
18 eqid 
 |-  ( Base ` ( Scalar ` V ) ) = ( Base ` ( Scalar ` V ) )
19 eqid 
 |-  ( .s ` V ) = ( .s ` V )
20 eqid 
 |-  ( 1r ` V ) = ( 1r ` V )
21 1 17 18 19 20 asclval 
 |-  ( Z e. ( Base ` ( Scalar ` V ) ) -> ( A ` Z ) = ( Z ( .s ` V ) ( 1r ` V ) ) )
22 16 21 syl 
 |-  ( ph -> ( A ` Z ) = ( Z ( .s ` V ) ( 1r ` V ) ) )
23 3 2 4 5 subrgply1 
 |-  ( S e. ( SubRing ` R ) -> P e. ( SubRing ` V ) )
24 eqid 
 |-  ( V |`s P ) = ( V |`s P )
25 24 19 ressvsca 
 |-  ( P e. ( SubRing ` V ) -> ( .s ` V ) = ( .s ` ( V |`s P ) ) )
26 6 23 25 3syl 
 |-  ( ph -> ( .s ` V ) = ( .s ` ( V |`s P ) ) )
27 26 oveqd 
 |-  ( ph -> ( Z ( .s ` V ) ( 1r ` V ) ) = ( Z ( .s ` ( V |`s P ) ) ( 1r ` V ) ) )
28 id 
 |-  ( ph -> ph )
29 20 subrg1cl 
 |-  ( P e. ( SubRing ` V ) -> ( 1r ` V ) e. P )
30 6 23 29 3syl 
 |-  ( ph -> ( 1r ` V ) e. P )
31 3 2 4 5 6 24 ressply1vsca 
 |-  ( ( ph /\ ( Z e. S /\ ( 1r ` V ) e. P ) ) -> ( Z ( .s ` W ) ( 1r ` V ) ) = ( Z ( .s ` ( V |`s P ) ) ( 1r ` V ) ) )
32 28 7 30 31 syl12anc 
 |-  ( ph -> ( Z ( .s ` W ) ( 1r ` V ) ) = ( Z ( .s ` ( V |`s P ) ) ( 1r ` V ) ) )
33 27 32 eqtr4d 
 |-  ( ph -> ( Z ( .s ` V ) ( 1r ` V ) ) = ( Z ( .s ` W ) ( 1r ` V ) ) )
34 2 subrgring 
 |-  ( S e. ( SubRing ` R ) -> U e. Ring )
35 4 ply1lmod 
 |-  ( U e. Ring -> W e. LMod )
36 6 34 35 3syl 
 |-  ( ph -> W e. LMod )
37 2 8 ressbas2 
 |-  ( S C_ ( Base ` R ) -> S = ( Base ` U ) )
38 6 9 37 3syl 
 |-  ( ph -> S = ( Base ` U ) )
39 7 38 eleqtrd 
 |-  ( ph -> Z e. ( Base ` U ) )
40 2 ovexi 
 |-  U e. _V
41 4 ply1sca 
 |-  ( U e. _V -> U = ( Scalar ` W ) )
42 40 41 ax-mp 
 |-  U = ( Scalar ` W )
43 eqid 
 |-  ( .s ` W ) = ( .s ` W )
44 eqid 
 |-  ( Base ` U ) = ( Base ` U )
45 5 42 43 44 lmodvscl 
 |-  ( ( W e. LMod /\ Z e. ( Base ` U ) /\ ( 1r ` V ) e. P ) -> ( Z ( .s ` W ) ( 1r ` V ) ) e. P )
46 36 39 30 45 syl3anc 
 |-  ( ph -> ( Z ( .s ` W ) ( 1r ` V ) ) e. P )
47 33 46 eqeltrd 
 |-  ( ph -> ( Z ( .s ` V ) ( 1r ` V ) ) e. P )
48 22 47 eqeltrd 
 |-  ( ph -> ( A ` Z ) e. P )