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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
selvascl.2 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
selvascl.3 ⊢ 𝐴 = ( algSc ‘ 𝑃 )
selvascl.4 ⊢ 𝐶 = ( algSc ‘ 𝑇 )
selvascl.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvascl.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
selvascl.7 ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvascl.8 ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvascl.9 ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
selvascl.10 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
selvascl.11 ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion selvascl ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 selvascl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 selvascl.2 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 selvascl.3 ⊢ 𝐴 = ( algSc ‘ 𝑃 )
4 selvascl.4 ⊢ 𝐶 = ( algSc ‘ 𝑇 )
5 selvascl.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 selvascl.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 selvascl.7 ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
8 selvascl.8 ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
9 selvascl.9 ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
10 selvascl.10 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
11 selvascl.11 ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
12 9 coeq1i ⊢ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐴 ‘ 𝑋 ) )
13 coass ⊢ ( ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐶 ∘ ( ( algSc ‘ 𝑈 ) ∘ ( 𝐴 ‘ 𝑋 ) ) )
14 12 13 eqtri ⊢ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐶 ∘ ( ( algSc ‘ 𝑈 ) ∘ ( 𝐴 ‘ 𝑋 ) ) )
15 eqid ⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly 𝑈 )
16 eqid ⊢ ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
17 eqid ⊢ ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) = ( algSc ‘ ( 𝐼 mPoly 𝑈 ) )
18 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
19 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
20 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ⊆ 𝐼 )
21 1 7 2 15 16 3 17 18 19 5 20 10 6 mplasclco ⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ∘ ( 𝐴 ‘ 𝑋 ) ) = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) )
22 21 coeq2d ⊢ ( 𝜑 → ( 𝐶 ∘ ( ( algSc ‘ 𝑈 ) ∘ ( 𝐴 ‘ 𝑋 ) ) ) = ( 𝐶 ∘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) )
23 14 22 eqtrid ⊢ ( 𝜑 → ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐶 ∘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) )
24 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
25 eqid ⊢ ( 𝐼 mPoly 𝑇 ) = ( 𝐼 mPoly 𝑇 )
26 eqid ⊢ ( algSc ‘ ( 𝐼 mPoly 𝑇 ) ) = ( algSc ‘ ( 𝐼 mPoly 𝑇 ) )
27 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
28 5 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
29 7 28 10 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
30 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
31 10 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
32 7 28 31 mplringd ⊢ ( 𝜑 → 𝑈 ∈ Ring )
33 7 28 31 mpllmodd ⊢ ( 𝜑 → 𝑈 ∈ LMod )
34 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
35 16 30 32 33 34 24 asclf ⊢ ( 𝜑 → ( algSc ‘ 𝑈 ) : ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟶ ( Base ‘ 𝑈 ) )
36 7 28 31 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑈 ) )
37 36 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
38 1 37 eqtr2id ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = 𝐵 )
39 6 38 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
40 35 39 ffvelcdmd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑈 ) )
41 24 8 15 25 4 17 26 18 27 5 11 29 40 mplasclco ⊢ ( 𝜑 → ( 𝐶 ∘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) = ( ( algSc ‘ ( 𝐼 mPoly 𝑇 ) ) ‘ ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) )
42 23 41 eqtrd ⊢ ( 𝜑 → ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) = ( ( algSc ‘ ( 𝐼 mPoly 𝑇 ) ) ‘ ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) )
43 42 fveq2d ⊢ ( 𝜑 → ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝐼 eval 𝑇 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑇 ) ) ‘ ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) ) )
44 eqid ⊢ ( 𝐼 eval 𝑇 ) = ( 𝐼 eval 𝑇 )
45 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
46 5 11 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
47 8 46 29 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
48 8 45 24 4 46 32 mplasclf ⊢ ( 𝜑 → 𝐶 : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) )
49 48 40 ffvelcdmd ⊢ ( 𝜑 → ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑇 ) )
50 44 25 45 26 5 47 49 evlsca ⊢ ( 𝜑 → ( ( 𝐼 eval 𝑇 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑇 ) ) ‘ ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ) ) = ( ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) × { ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) } ) )
51 43 50 eqtrd ⊢ ( 𝜑 → ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) × { ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) } ) )
52 51 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) = ( ( ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) × { ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) } ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) )
53 47 crngringd ⊢ ( 𝜑 → 𝑇 ∈ Ring )
54 45 subrgid ⊢ ( 𝑇 ∈ Ring → ( Base ‘ 𝑇 ) ∈ ( SubRing ‘ 𝑇 ) )
55 53 54 syl ⊢ ( 𝜑 → ( Base ‘ 𝑇 ) ∈ ( SubRing ‘ 𝑇 ) )
56 eqid ⊢ ( 𝐽 mVar 𝑈 ) = ( 𝐽 mVar 𝑈 )
57 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝐽 ) → 𝐽 ∈ V )
58 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝐽 ) → 𝑈 ∈ Ring )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝐽 ) → 𝑖 ∈ 𝐽 )
60 8 56 45 57 58 59 mvrcl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝐽 ) → ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝑇 ) )
61 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → 𝐶 : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) )
62 eqid ⊢ ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) = ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 )
63 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → ( 𝐼 ∖ 𝐽 ) ∈ V )
64 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → 𝑅 ∈ Ring )
65 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → 𝑖 ∈ 𝐼 )
66 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → ¬ 𝑖 ∈ 𝐽 )
67 65 66 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → 𝑖 ∈ ( 𝐼 ∖ 𝐽 ) )
68 7 62 24 63 64 67 mvrcl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝑈 ) )
69 61 68 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ 𝐽 ) → ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ∈ ( Base ‘ 𝑇 ) )
70 60 69 ifclda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ 𝑇 ) )
71 70 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑇 ) )
72 55 5 71 elmapdd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ∈ ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) )
73 fvex ⊢ ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) ∈ V
74 73 fvconst2 ⊢ ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ∈ ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) → ( ( ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) × { ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) } ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) )
75 72 74 syl ⊢ ( 𝜑 → ( ( ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) × { ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) } ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) )
76 52 75 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) = ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) )
77 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
78 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
79 2 5 31 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
80 2 5 31 mpllmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
81 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
82 3 78 79 80 81 77 asclf ⊢ ( 𝜑 → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
83 2 5 31 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
84 83 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
85 1 84 eqtr2id ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = 𝐵 )
86 6 85 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
87 82 86 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
88 2 77 7 8 4 9 10 11 87 selvval2 ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ ( 𝐴 ‘ 𝑋 ) ) ) ‘ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑖 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑖 ) ) ) ) ) )
89 35 ffund ⊢ ( 𝜑 → Fun ( algSc ‘ 𝑈 ) )
90 35 fdmd ⊢ ( 𝜑 → dom ( algSc ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
91 39 90 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ dom ( algSc ‘ 𝑈 ) )
92 89 91 9 fvcod ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ) )
93 76 88 92 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) )