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