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.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
8 selvval2.r 
 |-  ( ph -> R e. CRing )
9 selvval2.j 
 |-  ( ph -> J C_ I )
10 selvval2.f 
 |-  ( ph -> F e. B )
11 1 2 3 4 5 6 7 8 9 10 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 ) ) ) ) ) )
12 eqid 
 |-  ( ( I evalSub T ) ` ran D ) = ( ( I evalSub T ) ` ran D )
13 eqid 
 |-  ( I eval T ) = ( I eval T )
14 eqid 
 |-  ( I mPoly ( T |`s ran D ) ) = ( I mPoly ( T |`s ran D ) )
15 eqid 
 |-  ( T |`s ran D ) = ( T |`s ran D )
16 eqid 
 |-  ( Base ` ( I mPoly ( T |`s ran D ) ) ) = ( Base ` ( I mPoly ( T |`s ran D ) ) )
17 7 9 ssexd 
 |-  ( ph -> J e. _V )
18 7 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
19 3 18 8 mplcrngd 
 |-  ( ph -> U e. CRing )
20 4 17 19 mplcrngd 
 |-  ( ph -> T e. CRing )
21 3 4 5 6 18 17 8 selvcllem3 
 |-  ( ph -> ran D e. ( SubRing ` T ) )
22 1 2 3 4 5 6 15 14 16 7 8 9 10 selvcllem4 
 |-  ( ph -> ( D o. F ) e. ( Base ` ( I mPoly ( T |`s ran D ) ) ) )
23 12 13 14 15 16 7 20 21 22 evlsevl 
 |-  ( ph -> ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) = ( ( I eval T ) ` ( D o. F ) ) )
24 23 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 ) ) ) ) ) )
25 11 24 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 ) ) ) ) ) )