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

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.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.r 
 |-  ( ph -> R e. CRing )
7 selvcl.j 
 |-  ( ph -> J C_ I )
8 selvcl.f 
 |-  ( ph -> F e. B )
9 eqid 
 |-  ( algSc ` T ) = ( algSc ` T )
10 eqid 
 |-  ( ( algSc ` T ) o. ( algSc ` U ) ) = ( ( algSc ` T ) o. ( algSc ` U ) )
11 1 2 3 4 9 10 7 8 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 ) ) ) ) ) )
12 eqid 
 |-  ( T ^s ( E ^m I ) ) = ( T ^s ( E ^m I ) )
13 eqid 
 |-  ( Base ` ( T ^s ( E ^m I ) ) ) = ( Base ` ( T ^s ( E ^m I ) ) )
14 1 2 mplrcl 
 |-  ( F e. B -> I e. _V )
15 8 14 syl 
 |-  ( ph -> I e. _V )
16 15 7 ssexd 
 |-  ( ph -> J e. _V )
17 15 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
18 3 17 6 mplcrngd 
 |-  ( ph -> U e. CRing )
19 4 16 18 mplcrngd 
 |-  ( ph -> T e. CRing )
20 ovexd 
 |-  ( ph -> ( E ^m I ) e. _V )
21 eqid 
 |-  ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) = ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) )
22 eqid 
 |-  ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) = ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) )
23 eqid 
 |-  ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) = ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) )
24 3 4 9 10 21 22 23 12 5 15 6 7 selvcllemh 
 |-  ( 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 ) ) ) )
25 eqid 
 |-  ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) = ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) )
26 25 13 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 ) ) ) )
27 24 26 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 ) ) ) )
28 1 2 3 4 9 10 23 22 25 6 7 8 selvcllem4 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) e. ( Base ` ( I mPoly ( T |`s ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ) ) )
29 27 28 ffvelcdmd 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) e. ( Base ` ( T ^s ( E ^m I ) ) ) )
30 12 5 13 19 20 29 pwselbas 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran ( ( algSc ` T ) o. ( algSc ` U ) ) ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) : ( E ^m I ) --> E )
31 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 ) ) ) )
32 3 4 9 5 31 15 6 7 selvcllem5 
 |-  ( ph -> ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) e. ( E ^m I ) )
33 30 32 ffvelcdmd 
 |-  ( 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 )
34 11 33 eqeltrd 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) e. E )