Metamath Proof Explorer

Theorem selvcl

Description: Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024)

Ref Expression
Hypotheses selvcl.p 
|- P = ( I mPoly R )
selvcl.b 
|- B = ( Base ` P )
selvcl.u 
|- U = ( ( I \ J ) mPoly R )
selvcl.t 
|- T = ( J mPoly U )
selvcl.e 
|- E = ( Base ` T )
selvcl.i 
|- ( ph -> I e. V )
selvcl.r 
|- ( ph -> R e. CRing )
selvcl.j 
|- ( ph -> J C_ I )
selvcl.f 
|- ( ph -> F e. B )
Assertion selvcl 
|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) e. E )

Proof

Step Hyp Ref Expression
1 selvcl.p 
 |-  P = ( I mPoly R )
2 selvcl.b 
 |-  B = ( Base ` P )
3 selvcl.u 
 |-  U = ( ( I \ J ) mPoly R )
4 selvcl.t 
 |-  T = ( J mPoly U )
5 selvcl.e 
 |-  E = ( Base ` T )
6 selvcl.i 
 |-  ( ph -> I e. V )
7 selvcl.r 
 |-  ( ph -> R e. CRing )
8 selvcl.j 
 |-  ( ph -> J C_ I )
9 selvcl.f 
 |-  ( ph -> F e. B )
10 eqid 
 |-  ( algSc ` T ) = ( algSc ` T )
11 eqid 
 |-  ( ( algSc ` T ) o. ( algSc ` U ) ) = ( ( algSc ` T ) o. ( algSc ` U ) )
12 1 2 3 4 10 11 6 7 8 9 selvval 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
13 eqid 
 |-  ( T ^s ( E ^m I ) ) = ( T ^s ( E ^m I ) )
14 eqid 
 |-  ( Base ` ( T ^s ( E ^m I ) ) ) = ( Base ` ( T ^s ( E ^m I ) ) )
15 6 8 ssexd 
 |-  ( ph -> J e. _V )
16 6 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
17 3 mplcrng 
 |-  ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. CRing )
18 16 7 17 syl2anc 
 |-  ( ph -> U e. CRing )
19 4 mplcrng 
 |-  ( ( J e. _V /\ U e. CRing ) -> T e. CRing )
20 15 18 19 syl2anc 
 |-  ( ph -> T e. CRing )
21 ovexd 
 |-  ( ph -> ( E ^m I ) e. _V )
22 eqid 
 |-  ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) = ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) )
23 eqid 
 |-  ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) = ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) )
24 eqid 
 |-  ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) = ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) )
25 3 4 10 11 22 23 24 13 5 6 7 8 selvval2lemn 
 |-  ( ph -> ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) e. ( ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) RingHom ( T ^s ( E ^m I ) ) ) )
26 eqid 
 |-  ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) = ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) )
27 26 14 rhmf 
 |-  ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) e. ( ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) RingHom ( T ^s ( E ^m I ) ) ) -> ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) : ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) --> ( Base ` ( T ^s ( E ^m I ) ) ) )
28 25 27 syl 
 |-  ( ph -> ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) : ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) --> ( Base ` ( T ^s ( E ^m I ) ) ) )
29 1 2 3 4 10 11 24 23 26 6 7 8 9 selvval2lem4 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) e. ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) )
30 28 29 ffvelrnd 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) e. ( Base ` ( T ^s ( E ^m I ) ) ) )
31 13 5 14 20 21 30 pwselbas 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) : ( E ^m I ) --> E )
32 eqid 
 |-  ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) = ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
33 3 4 10 5 32 6 7 8 selvval2lem5 
 |-  ( ph -> ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) e. ( E ^m I ) )
34 31 33 ffvelrnd 
 |-  ( ph -> ( ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) e. E )
35 12 34 eqeltrd 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) e. E )