Metamath Proof Explorer

Theorem selvval2

Description: Value of the "variable selection" function. Convert selvval into a simpler form by using evlsevl . (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses selvval2.p 
|- P = ( I mPoly R )
selvval2.b 
|- B = ( Base ` P )
selvval2.u 
|- U = ( ( I \ J ) mPoly R )
selvval2.t 
|- T = ( J mPoly U )
selvval2.c 
|- C = ( algSc ` T )
selvval2.d 
|- D = ( C o. ( algSc ` U ) )
selvval2.r 
|- ( ph -> R e. CRing )
selvval2.j 
|- ( ph -> J C_ I )
selvval2.f 
|- ( ph -> F e. B )
Assertion selvval2 
|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( I eval T ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selvval2.p 
 |-  P = ( I mPoly R )
2 selvval2.b 
 |-  B = ( Base ` P )
3 selvval2.u 
 |-  U = ( ( I \ J ) mPoly R )
4 selvval2.t 
 |-  T = ( J mPoly U )
5 selvval2.c 
 |-  C = ( algSc ` T )
6 selvval2.d 
 |-  D = ( C o. ( algSc ` U ) )
7 selvval2.r 
 |-  ( ph -> R e. CRing )
8 selvval2.j 
 |-  ( ph -> J C_ I )
9 selvval2.f 
 |-  ( ph -> F e. B )
10 1 2 3 4 5 6 8 9 selvval 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
11 eqid 
 |-  ( ( I evalSub T ) ` ran D ) = ( ( I evalSub T ) ` ran D )
12 eqid 
 |-  ( I eval T ) = ( I eval T )
13 eqid 
 |-  ( I mPoly ( T |`s ran D ) ) = ( I mPoly ( T |`s ran D ) )
14 eqid 
 |-  ( T |`s ran D ) = ( T |`s ran D )
15 eqid 
 |-  ( Base ` ( I mPoly ( T |`s ran D ) ) ) = ( Base ` ( I mPoly ( T |`s ran D ) ) )
16 1 2 mplrcl 
 |-  ( F e. B -> I e. _V )
17 9 16 syl 
 |-  ( ph -> I e. _V )
18 17 8 ssexd 
 |-  ( ph -> J e. _V )
19 17 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
20 3 19 7 mplcrngd 
 |-  ( ph -> U e. CRing )
21 4 18 20 mplcrngd 
 |-  ( ph -> T e. CRing )
22 3 4 5 6 19 18 7 selvcllem3 
 |-  ( ph -> ran D e. ( SubRing ` T ) )
23 1 2 3 4 5 6 14 13 15 7 8 9 selvcllem4 
 |-  ( ph -> ( D o. F ) e. ( Base ` ( I mPoly ( T |`s ran D ) ) ) )
24 11 12 13 14 15 17 21 22 23 evlsevl 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) = ( ( I eval T ) ` ( D o. F ) ) )
25 24 fveq1d 
 |-  ( ph -> ( ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
26 10 25 eqtrd 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( I eval T ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )