Metamath Proof Explorer

Theorem selvascl

Description: The "variable selection" function evaluated at a scalar. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses selvascl.1 
|- B = ( Base ` R )
selvascl.2 
|- P = ( I mPoly R )
selvascl.3 
|- A = ( algSc ` P )
selvascl.4 
|- C = ( algSc ` T )
selvascl.5 
|- ( ph -> I e. V )
selvascl.6 
|- ( ph -> X e. B )
selvascl.7 
|- U = ( ( I \ J ) mPoly R )
selvascl.8 
|- T = ( J mPoly U )
selvascl.9 
|- D = ( C o. ( algSc ` U ) )
selvascl.10 
|- ( ph -> R e. CRing )
selvascl.11 
|- ( ph -> J C_ I )
Assertion selvascl 
|- ( ph -> ( ( ( I selectVars R ) ` J ) ` ( A ` X ) ) = ( D ` X ) )

Proof

Step Hyp Ref Expression
1 selvascl.1 
 |-  B = ( Base ` R )
2 selvascl.2 
 |-  P = ( I mPoly R )
3 selvascl.3 
 |-  A = ( algSc ` P )
4 selvascl.4 
 |-  C = ( algSc ` T )
5 selvascl.5 
 |-  ( ph -> I e. V )
6 selvascl.6 
 |-  ( ph -> X e. B )
7 selvascl.7 
 |-  U = ( ( I \ J ) mPoly R )
8 selvascl.8 
 |-  T = ( J mPoly U )
9 selvascl.9 
 |-  D = ( C o. ( algSc ` U ) )
10 selvascl.10 
 |-  ( ph -> R e. CRing )
11 selvascl.11 
 |-  ( ph -> J C_ I )
12 9 coeq1i 
 |-  ( D o. ( A ` X ) ) = ( ( C o. ( algSc ` U ) ) o. ( A ` X ) )
13 coass 
 |-  ( ( C o. ( algSc ` U ) ) o. ( A ` X ) ) = ( C o. ( ( algSc ` U ) o. ( A ` X ) ) )
14 12 13 eqtri 
 |-  ( D o. ( A ` X ) ) = ( C o. ( ( algSc ` U ) o. ( A ` X ) ) )
15 eqid 
 |-  ( I mPoly U ) = ( I mPoly U )
16 eqid 
 |-  ( algSc ` U ) = ( algSc ` U )
17 eqid 
 |-  ( algSc ` ( I mPoly U ) ) = ( algSc ` ( I mPoly U ) )
18 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
19 eqid 
 |-  { h e. ( NN0 ^m ( I \ J ) ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m ( I \ J ) ) | ( `' h " NN ) e. Fin }
20 difssd 
 |-  ( ph -> ( I \ J ) C_ I )
21 1 7 2 15 16 3 17 18 19 5 20 10 6 mplasclco 
 |-  ( ph -> ( ( algSc ` U ) o. ( A ` X ) ) = ( ( algSc ` ( I mPoly U ) ) ` ( ( algSc ` U ) ` X ) ) )
22 21 coeq2d 
 |-  ( ph -> ( C o. ( ( algSc ` U ) o. ( A ` X ) ) ) = ( C o. ( ( algSc ` ( I mPoly U ) ) ` ( ( algSc ` U ) ` X ) ) ) )
23 14 22 eqtrid 
 |-  ( ph -> ( D o. ( A ` X ) ) = ( C o. ( ( algSc ` ( I mPoly U ) ) ` ( ( algSc ` U ) ` X ) ) ) )
24 eqid 
 |-  ( Base ` U ) = ( Base ` U )
25 eqid 
 |-  ( I mPoly T ) = ( I mPoly T )
26 eqid 
 |-  ( algSc ` ( I mPoly T ) ) = ( algSc ` ( I mPoly T ) )
27 eqid 
 |-  { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin }
28 5 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
29 7 28 10 mplcrngd 
 |-  ( ph -> U e. CRing )
30 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
31 10 crngringd 
 |-  ( ph -> R e. Ring )
32 7 28 31 mplringd 
 |-  ( ph -> U e. Ring )
33 7 28 31 mpllmodd 
 |-  ( ph -> U e. LMod )
34 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
35 16 30 32 33 34 24 asclf 
 |-  ( ph -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> ( Base ` U ) )
36 7 28 31 mplsca 
 |-  ( ph -> R = ( Scalar ` U ) )
37 36 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` U ) ) )
38 1 37 eqtr2id 
 |-  ( ph -> ( Base ` ( Scalar ` U ) ) = B )
39 6 38 eleqtrrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` U ) ) )
40 35 39 ffvelcdmd 
 |-  ( ph -> ( ( algSc ` U ) ` X ) e. ( Base ` U ) )
41 24 8 15 25 4 17 26 18 27 5 11 29 40 mplasclco 
 |-  ( ph -> ( C o. ( ( algSc ` ( I mPoly U ) ) ` ( ( algSc ` U ) ` X ) ) ) = ( ( algSc ` ( I mPoly T ) ) ` ( C ` ( ( algSc ` U ) ` X ) ) ) )
42 23 41 eqtrd 
 |-  ( ph -> ( D o. ( A ` X ) ) = ( ( algSc ` ( I mPoly T ) ) ` ( C ` ( ( algSc ` U ) ` X ) ) ) )
43 42 fveq2d 
 |-  ( ph -> ( ( I eval T ) ` ( D o. ( A ` X ) ) ) = ( ( I eval T ) ` ( ( algSc ` ( I mPoly T ) ) ` ( C ` ( ( algSc ` U ) ` X ) ) ) ) )
44 eqid 
 |-  ( I eval T ) = ( I eval T )
45 eqid 
 |-  ( Base ` T ) = ( Base ` T )
46 5 11 ssexd 
 |-  ( ph -> J e. _V )
47 8 46 29 mplcrngd 
 |-  ( ph -> T e. CRing )
48 8 45 24 4 46 32 mplasclf 
 |-  ( ph -> C : ( Base ` U ) --> ( Base ` T ) )
49 48 40 ffvelcdmd 
 |-  ( ph -> ( C ` ( ( algSc ` U ) ` X ) ) e. ( Base ` T ) )
50 44 25 45 26 5 47 49 evlsca 
 |-  ( ph -> ( ( I eval T ) ` ( ( algSc ` ( I mPoly T ) ) ` ( C ` ( ( algSc ` U ) ` X ) ) ) ) = ( ( ( Base ` T ) ^m I ) X. { ( C ` ( ( algSc ` U ) ` X ) ) } ) )
51 43 50 eqtrd 
 |-  ( ph -> ( ( I eval T ) ` ( D o. ( A ` X ) ) ) = ( ( ( Base ` T ) ^m I ) X. { ( C ` ( ( algSc ` U ) ` X ) ) } ) )
52 51 fveq1d 
 |-  ( ph -> ( ( ( I eval T ) ` ( D o. ( A ` X ) ) ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) = ( ( ( ( Base ` T ) ^m I ) X. { ( C ` ( ( algSc ` U ) ` X ) ) } ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) )
53 47 crngringd 
 |-  ( ph -> T e. Ring )
54 45 subrgid 
 |-  ( T e. Ring -> ( Base ` T ) e. ( SubRing ` T ) )
55 53 54 syl 
 |-  ( ph -> ( Base ` T ) e. ( SubRing ` T ) )
56 eqid 
 |-  ( J mVar U ) = ( J mVar U )
57 46 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ i e. J ) -> J e. _V )
58 32 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ i e. J ) -> U e. Ring )
59 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ i e. J ) -> i e. J )
60 8 56 45 57 58 59 mvrcl 
 |-  ( ( ( ph /\ i e. I ) /\ i e. J ) -> ( ( J mVar U ) ` i ) e. ( Base ` T ) )
61 48 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> C : ( Base ` U ) --> ( Base ` T ) )
62 eqid 
 |-  ( ( I \ J ) mVar R ) = ( ( I \ J ) mVar R )
63 28 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> ( I \ J ) e. _V )
64 31 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> R e. Ring )
65 simplr 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> i e. I )
66 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> -. i e. J )
67 65 66 eldifd 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> i e. ( I \ J ) )
68 7 62 24 63 64 67 mvrcl 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> ( ( ( I \ J ) mVar R ) ` i ) e. ( Base ` U ) )
69 61 68 ffvelcdmd 
 |-  ( ( ( ph /\ i e. I ) /\ -. i e. J ) -> ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) e. ( Base ` T ) )
70 60 69 ifclda 
 |-  ( ( ph /\ i e. I ) -> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) e. ( Base ` T ) )
71 70 fmpttd 
 |-  ( ph -> ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) : I --> ( Base ` T ) )
72 55 5 71 elmapdd 
 |-  ( ph -> ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) e. ( ( Base ` T ) ^m I ) )
73 fvex 
 |-  ( C ` ( ( algSc ` U ) ` X ) ) e. _V
74 73 fvconst2 
 |-  ( ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) e. ( ( Base ` T ) ^m I ) -> ( ( ( ( Base ` T ) ^m I ) X. { ( C ` ( ( algSc ` U ) ` X ) ) } ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) = ( C ` ( ( algSc ` U ) ` X ) ) )
75 72 74 syl 
 |-  ( ph -> ( ( ( ( Base ` T ) ^m I ) X. { ( C ` ( ( algSc ` U ) ` X ) ) } ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) = ( C ` ( ( algSc ` U ) ` X ) ) )
76 52 75 eqtrd 
 |-  ( ph -> ( ( ( I eval T ) ` ( D o. ( A ` X ) ) ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) = ( C ` ( ( algSc ` U ) ` X ) ) )
77 eqid 
 |-  ( Base ` P ) = ( Base ` P )
78 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
79 2 5 31 mplringd 
 |-  ( ph -> P e. Ring )
80 2 5 31 mpllmodd 
 |-  ( ph -> P e. LMod )
81 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
82 3 78 79 80 81 77 asclf 
 |-  ( ph -> A : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
83 2 5 31 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
84 83 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
85 1 84 eqtr2id 
 |-  ( ph -> ( Base ` ( Scalar ` P ) ) = B )
86 6 85 eleqtrrd 
 |-  ( ph -> X e. ( Base ` ( Scalar ` P ) ) )
87 82 86 ffvelcdmd 
 |-  ( ph -> ( A ` X ) e. ( Base ` P ) )
88 2 77 7 8 4 9 10 11 87 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` ( A ` X ) ) = ( ( ( I eval T ) ` ( D o. ( A ` X ) ) ) ` ( i e. I |-> if ( i e. J , ( ( J mVar U ) ` i ) , ( C ` ( ( ( I \ J ) mVar R ) ` i ) ) ) ) ) )
89 35 ffund 
 |-  ( ph -> Fun ( algSc ` U ) )
90 35 fdmd 
 |-  ( ph -> dom ( algSc ` U ) = ( Base ` ( Scalar ` U ) ) )
91 39 90 eleqtrrd 
 |-  ( ph -> X e. dom ( algSc ` U ) )
92 89 91 9 fvcod 
 |-  ( ph -> ( D ` X ) = ( C ` ( ( algSc ` U ) ` X ) ) )
93 76 88 92 3eqtr4d 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` ( A ` X ) ) = ( D ` X ) )