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 ⊢ φ → I ∈ V
selvascl.6 ⊢ φ → X ∈ B
selvascl.7 ⊢ U = I ∖ J mPoly R
selvascl.8 ⊢ T = J mPoly U
selvascl.9 ⊢ D = C ∘ algSc ⁡ U
selvascl.10 ⊢ φ → R ∈ CRing
selvascl.11 ⊢ φ → J ⊆ I
Assertion selvascl ⊢ φ → 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 ⊢ φ → I ∈ V
6 selvascl.6 ⊢ φ → X ∈ B
7 selvascl.7 ⊢ U = I ∖ J mPoly R
8 selvascl.8 ⊢ T = J mPoly U
9 selvascl.9 ⊢ D = C ∘ algSc ⁡ U
10 selvascl.10 ⊢ φ → R ∈ CRing
11 selvascl.11 ⊢ φ → J ⊆ I
12 9 coeq1i ⊢ D ∘ A ⁡ X = C ∘ algSc ⁡ U ∘ A ⁡ X
13 coass ⊢ C ∘ algSc ⁡ U ∘ A ⁡ X = C ∘ algSc ⁡ U ∘ A ⁡ X
14 12 13 eqtri ⊢ D ∘ A ⁡ X = C ∘ algSc ⁡ U ∘ 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 ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
19 eqid ⊢ h ∈ ℕ 0 I ∖ J | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I ∖ J | h -1 ℕ ∈ Fin
20 difssd ⊢ φ → I ∖ J ⊆ I
21 1 7 2 15 16 3 17 18 19 5 20 10 6 mplasclco ⊢ φ → algSc ⁡ U ∘ A ⁡ X = algSc ⁡ I mPoly U ⁡ algSc ⁡ U ⁡ X
22 21 coeq2d ⊢ φ → C ∘ algSc ⁡ U ∘ A ⁡ X = C ∘ algSc ⁡ I mPoly U ⁡ algSc ⁡ U ⁡ X
23 14 22 eqtrid ⊢ φ → D ∘ A ⁡ X = C ∘ 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 ∈ ℕ 0 J | h -1 ℕ ∈ Fin = h ∈ ℕ 0 J | h -1 ℕ ∈ Fin
28 5 difexd ⊢ φ → I ∖ J ∈ V
29 7 28 10 mplcrngd ⊢ φ → U ∈ CRing
30 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
31 10 crngringd ⊢ φ → R ∈ Ring
32 7 28 31 mplringd ⊢ φ → U ∈ Ring
33 7 28 31 mpllmodd ⊢ φ → U ∈ LMod
34 eqid ⊢ Base Scalar ⁡ U = Base Scalar ⁡ U
35 16 30 32 33 34 24 asclf ⊢ φ → algSc ⁡ U : Base Scalar ⁡ U ⟶ Base U
36 7 28 31 mplsca ⊢ φ → R = Scalar ⁡ U
37 36 fveq2d ⊢ φ → Base R = Base Scalar ⁡ U
38 1 37 eqtr2id ⊢ φ → Base Scalar ⁡ U = B
39 6 38 eleqtrrd ⊢ φ → X ∈ Base Scalar ⁡ U
40 35 39 ffvelcdmd ⊢ φ → algSc ⁡ U ⁡ X ∈ Base U
41 24 8 15 25 4 17 26 18 27 5 11 29 40 mplasclco ⊢ φ → C ∘ algSc ⁡ I mPoly U ⁡ algSc ⁡ U ⁡ X = algSc ⁡ I mPoly T ⁡ C ⁡ algSc ⁡ U ⁡ X
42 23 41 eqtrd ⊢ φ → D ∘ A ⁡ X = algSc ⁡ I mPoly T ⁡ C ⁡ algSc ⁡ U ⁡ X
43 42 fveq2d ⊢ φ → I eval T ⁡ D ∘ 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 ⊢ φ → J ∈ V
47 8 46 29 mplcrngd ⊢ φ → T ∈ CRing
48 8 45 24 4 46 32 mplasclf ⊢ φ → C : Base U ⟶ Base T
49 48 40 ffvelcdmd ⊢ φ → C ⁡ algSc ⁡ U ⁡ X ∈ Base T
50 44 25 45 26 5 47 49 evlsca ⊢ φ → I eval T ⁡ algSc ⁡ I mPoly T ⁡ C ⁡ algSc ⁡ U ⁡ X = Base T I × C ⁡ algSc ⁡ U ⁡ X
51 43 50 eqtrd ⊢ φ → I eval T ⁡ D ∘ A ⁡ X = Base T I × C ⁡ algSc ⁡ U ⁡ X
52 51 fveq1d ⊢ φ → I eval T ⁡ D ∘ A ⁡ X ⁡ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i = Base T I × C ⁡ algSc ⁡ U ⁡ X ⁡ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i
53 47 crngringd ⊢ φ → T ∈ Ring
54 45 subrgid ⊢ T ∈ Ring → Base T ∈ SubRing ⁡ T
55 53 54 syl ⊢ φ → Base T ∈ SubRing ⁡ T
56 eqid ⊢ J mVar U = J mVar U
57 46 ad2antrr ⊢ φ ∧ i ∈ I ∧ i ∈ J → J ∈ V
58 32 ad2antrr ⊢ φ ∧ i ∈ I ∧ i ∈ J → U ∈ Ring
59 simpr ⊢ φ ∧ i ∈ I ∧ i ∈ J → i ∈ J
60 8 56 45 57 58 59 mvrcl ⊢ φ ∧ i ∈ I ∧ i ∈ J → J mVar U ⁡ i ∈ Base T
61 48 ad2antrr ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → C : Base U ⟶ Base T
62 eqid ⊢ I ∖ J mVar R = I ∖ J mVar R
63 28 ad2antrr ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → I ∖ J ∈ V
64 31 ad2antrr ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → R ∈ Ring
65 simplr ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → i ∈ I
66 simpr ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → ¬ i ∈ J
67 65 66 eldifd ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → i ∈ I ∖ J
68 7 62 24 63 64 67 mvrcl ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → I ∖ J mVar R ⁡ i ∈ Base U
69 61 68 ffvelcdmd ⊢ φ ∧ i ∈ I ∧ ¬ i ∈ J → C ⁡ I ∖ J mVar R ⁡ i ∈ Base T
70 60 69 ifclda ⊢ φ ∧ i ∈ I → if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i ∈ Base T
71 70 fmpttd ⊢ φ → i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i : I ⟶ Base T
72 55 5 71 elmapdd ⊢ φ → i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i ∈ Base T I
73 fvex ⊢ C ⁡ algSc ⁡ U ⁡ X ∈ V
74 73 fvconst2 ⊢ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i ∈ Base T I → Base T I × C ⁡ algSc ⁡ U ⁡ X ⁡ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i = C ⁡ algSc ⁡ U ⁡ X
75 72 74 syl ⊢ φ → Base T I × C ⁡ algSc ⁡ U ⁡ X ⁡ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i = C ⁡ algSc ⁡ U ⁡ X
76 52 75 eqtrd ⊢ φ → I eval T ⁡ D ∘ A ⁡ X ⁡ i ∈ I ⟼ if i ∈ 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 ⊢ φ → P ∈ Ring
80 2 5 31 mpllmodd ⊢ φ → P ∈ LMod
81 eqid ⊢ Base Scalar ⁡ P = Base Scalar ⁡ P
82 3 78 79 80 81 77 asclf ⊢ φ → A : Base Scalar ⁡ P ⟶ Base P
83 2 5 31 mplsca ⊢ φ → R = Scalar ⁡ P
84 83 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
85 1 84 eqtr2id ⊢ φ → Base Scalar ⁡ P = B
86 6 85 eleqtrrd ⊢ φ → X ∈ Base Scalar ⁡ P
87 82 86 ffvelcdmd ⊢ φ → A ⁡ X ∈ Base P
88 2 77 7 8 4 9 10 11 87 selvval2 ⊢ φ → I selectVars R ⁡ J ⁡ A ⁡ X = I eval T ⁡ D ∘ A ⁡ X ⁡ i ∈ I ⟼ if i ∈ J J mVar U ⁡ i C ⁡ I ∖ J mVar R ⁡ i
89 35 ffund ⊢ φ → Fun ⁡ algSc ⁡ U
90 35 fdmd ⊢ φ → dom ⁡ algSc ⁡ U = Base Scalar ⁡ U
91 39 90 eleqtrrd ⊢ φ → X ∈ dom ⁡ algSc ⁡ U
92 89 91 9 fvcod ⊢ φ → D ⁡ X = C ⁡ algSc ⁡ U ⁡ X
93 76 88 92 3eqtr4d ⊢ φ → I selectVars R ⁡ J ⁡ A ⁡ X = D ⁡ X