Metamath Proof Explorer

Theorem selvval2lem4

Description: The fourth argument passed to evalSub is in the domain (a polynomial in ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ). (Contributed by SN, 5-Nov-2023)

Ref Expression
Hypotheses selvval2lem4.p 
|- P = ( I mPoly R )
selvval2lem4.b 
|- B = ( Base ` P )
selvval2lem4.u 
|- U = ( ( I \ J ) mPoly R )
selvval2lem4.t 
|- T = ( J mPoly U )
selvval2lem4.c 
|- C = ( algSc ` T )
selvval2lem4.d 
|- D = ( C o. ( algSc ` U ) )
selvval2lem4.s 
|- S = ( T |`s ran D )
selvval2lem4.w 
|- W = ( I mPoly S )
selvval2lem4.x 
|- X = ( Base ` W )
selvval2lem4.i 
|- ( ph -> I e. V )
selvval2lem4.r 
|- ( ph -> R e. CRing )
selvval2lem4.j 
|- ( ph -> J C_ I )
selvval2lem4.f 
|- ( ph -> F e. B )
Assertion selvval2lem4 
|- ( ph -> ( D o. F ) e. X )

Proof

Step Hyp Ref Expression
1 selvval2lem4.p 
 |-  P = ( I mPoly R )
2 selvval2lem4.b 
 |-  B = ( Base ` P )
3 selvval2lem4.u 
 |-  U = ( ( I \ J ) mPoly R )
4 selvval2lem4.t 
 |-  T = ( J mPoly U )
5 selvval2lem4.c 
 |-  C = ( algSc ` T )
6 selvval2lem4.d 
 |-  D = ( C o. ( algSc ` U ) )
7 selvval2lem4.s 
 |-  S = ( T |`s ran D )
8 selvval2lem4.w 
 |-  W = ( I mPoly S )
9 selvval2lem4.x 
 |-  X = ( Base ` W )
10 selvval2lem4.i 
 |-  ( ph -> I e. V )
11 selvval2lem4.r 
 |-  ( ph -> R e. CRing )
12 selvval2lem4.j 
 |-  ( ph -> J C_ I )
13 selvval2lem4.f 
 |-  ( ph -> F e. B )
14 10 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
15 10 12 ssexd 
 |-  ( ph -> J e. _V )
16 3 4 5 6 14 15 11 selvval2lem2 
 |-  ( ph -> D e. ( R RingHom T ) )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 eqid 
 |-  ( Base ` T ) = ( Base ` T )
19 17 18 rhmf 
 |-  ( D e. ( R RingHom T ) -> D : ( Base ` R ) --> ( Base ` T ) )
20 ffrn 
 |-  ( D : ( Base ` R ) --> ( Base ` T ) -> D : ( Base ` R ) --> ran D )
21 16 19 20 3syl 
 |-  ( ph -> D : ( Base ` R ) --> ran D )
22 3 4 5 6 14 15 11 selvval2lem3 
 |-  ( ph -> ran D e. ( SubRing ` T ) )
23 18 subrgss 
 |-  ( ran D e. ( SubRing ` T ) -> ran D C_ ( Base ` T ) )
24 7 18 ressbas2 
 |-  ( ran D C_ ( Base ` T ) -> ran D = ( Base ` S ) )
25 22 23 24 3syl 
 |-  ( ph -> ran D = ( Base ` S ) )
26 25 feq3d 
 |-  ( ph -> ( D : ( Base ` R ) --> ran D <-> D : ( Base ` R ) --> ( Base ` S ) ) )
27 21 26 mpbid 
 |-  ( ph -> D : ( Base ` R ) --> ( Base ` S ) )
28 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
29 1 17 2 28 13 mplelf 
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
30 27 29 fcod 
 |-  ( ph -> ( D o. F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` S ) )
31 fvexd 
 |-  ( ph -> ( Base ` S ) e. _V )
32 ovex 
 |-  ( NN0 ^m I ) e. _V
33 32 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
34 33 a1i 
 |-  ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
35 31 34 elmapd 
 |-  ( ph -> ( ( D o. F ) e. ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) <-> ( D o. F ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` S ) ) )
36 30 35 mpbird 
 |-  ( ph -> ( D o. F ) e. ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
37 eqid 
 |-  ( I mPwSer S ) = ( I mPwSer S )
38 eqid 
 |-  ( Base ` S ) = ( Base ` S )
39 eqid 
 |-  ( Base ` ( I mPwSer S ) ) = ( Base ` ( I mPwSer S ) )
40 37 38 28 39 10 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer S ) ) = ( ( Base ` S ) ^m { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) )
41 36 40 eleqtrrd 
 |-  ( ph -> ( D o. F ) e. ( Base ` ( I mPwSer S ) ) )
42 fvexd 
 |-  ( ph -> ( 0g ` S ) e. _V )
43 crngring 
 |-  ( R e. CRing -> R e. Ring )
44 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
45 17 44 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
46 11 43 45 3syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
47 ssidd 
 |-  ( ph -> ( Base ` R ) C_ ( Base ` R ) )
48 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
49 1 2 44 13 11 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
50 6 a1i 
 |-  ( ph -> D = ( C o. ( algSc ` U ) ) )
51 50 fveq1d 
 |-  ( ph -> ( D ` ( 0g ` R ) ) = ( ( C o. ( algSc ` U ) ) ` ( 0g ` R ) ) )
52 eqid 
 |-  ( Base ` U ) = ( Base ` U )
53 eqid 
 |-  ( algSc ` U ) = ( algSc ` U )
54 11 43 syl 
 |-  ( ph -> R e. Ring )
55 3 52 17 53 14 54 mplasclf 
 |-  ( ph -> ( algSc ` U ) : ( Base ` R ) --> ( Base ` U ) )
56 55 46 fvco3d 
 |-  ( ph -> ( ( C o. ( algSc ` U ) ) ` ( 0g ` R ) ) = ( C ` ( ( algSc ` U ) ` ( 0g ` R ) ) ) )
57 3 14 11 mplsca 
 |-  ( ph -> R = ( Scalar ` U ) )
58 57 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` U ) ) )
59 58 fveq2d 
 |-  ( ph -> ( ( algSc ` U ) ` ( 0g ` R ) ) = ( ( algSc ` U ) ` ( 0g ` ( Scalar ` U ) ) ) )
60 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
61 3 mplassa 
 |-  ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. AssAlg )
62 14 11 61 syl2anc 
 |-  ( ph -> U e. AssAlg )
63 assalmod 
 |-  ( U e. AssAlg -> U e. LMod )
64 62 63 syl 
 |-  ( ph -> U e. LMod )
65 assaring 
 |-  ( U e. AssAlg -> U e. Ring )
66 62 65 syl 
 |-  ( ph -> U e. Ring )
67 53 60 64 66 ascl0 
 |-  ( ph -> ( ( algSc ` U ) ` ( 0g ` ( Scalar ` U ) ) ) = ( 0g ` U ) )
68 59 67 eqtrd 
 |-  ( ph -> ( ( algSc ` U ) ` ( 0g ` R ) ) = ( 0g ` U ) )
69 68 fveq2d 
 |-  ( ph -> ( C ` ( ( algSc ` U ) ` ( 0g ` R ) ) ) = ( C ` ( 0g ` U ) ) )
70 4 15 62 mplsca 
 |-  ( ph -> U = ( Scalar ` T ) )
71 70 fveq2d 
 |-  ( ph -> ( 0g ` U ) = ( 0g ` ( Scalar ` T ) ) )
72 71 fveq2d 
 |-  ( ph -> ( C ` ( 0g ` U ) ) = ( C ` ( 0g ` ( Scalar ` T ) ) ) )
73 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
74 3 4 14 15 11 selvval2lem1 
 |-  ( ph -> T e. AssAlg )
75 assalmod 
 |-  ( T e. AssAlg -> T e. LMod )
76 74 75 syl 
 |-  ( ph -> T e. LMod )
77 assaring 
 |-  ( T e. AssAlg -> T e. Ring )
78 74 77 syl 
 |-  ( ph -> T e. Ring )
79 5 73 76 78 ascl0 
 |-  ( ph -> ( C ` ( 0g ` ( Scalar ` T ) ) ) = ( 0g ` T ) )
80 subrgsubg 
 |-  ( ran D e. ( SubRing ` T ) -> ran D e. ( SubGrp ` T ) )
81 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
82 7 81 subg0 
 |-  ( ran D e. ( SubGrp ` T ) -> ( 0g ` T ) = ( 0g ` S ) )
83 22 80 82 3syl 
 |-  ( ph -> ( 0g ` T ) = ( 0g ` S ) )
84 79 83 eqtrd 
 |-  ( ph -> ( C ` ( 0g ` ( Scalar ` T ) ) ) = ( 0g ` S ) )
85 69 72 84 3eqtrd 
 |-  ( ph -> ( C ` ( ( algSc ` U ) ` ( 0g ` R ) ) ) = ( 0g ` S ) )
86 51 56 85 3eqtrd 
 |-  ( ph -> ( D ` ( 0g ` R ) ) = ( 0g ` S ) )
87 42 46 29 21 47 34 48 49 86 fsuppcor 
 |-  ( ph -> ( D o. F ) finSupp ( 0g ` S ) )
88 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
89 8 37 39 88 9 mplelbas 
 |-  ( ( D o. F ) e. X <-> ( ( D o. F ) e. ( Base ` ( I mPwSer S ) ) /\ ( D o. F ) finSupp ( 0g ` S ) ) )
90 41 87 89 sylanbrc 
 |-  ( ph -> ( D o. F ) e. X )