Metamath Proof Explorer

Theorem selvval

Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023)

Ref Expression
Hypotheses selvval.p ⊢ P = I mPoly R
selvval.b ⊢ B = Base P
selvval.u ⊢ U = I ∖ J mPoly R
selvval.t ⊢ T = J mPoly U
selvval.c ⊢ C = algSc ⁡ T
selvval.d ⊢ D = C ∘ algSc ⁡ U
selvval.j ⊢ φ → J ⊆ I
selvval.f ⊢ φ → F ∈ B
Assertion selvval ⊢ φ → I selectVars R ⁡ J ⁡ F = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x

Proof

Step Hyp Ref Expression
1 selvval.p ⊢ P = I mPoly R
2 selvval.b ⊢ B = Base P
3 selvval.u ⊢ U = I ∖ J mPoly R
4 selvval.t ⊢ T = J mPoly U
5 selvval.c ⊢ C = algSc ⁡ T
6 selvval.d ⊢ D = C ∘ algSc ⁡ U
7 selvval.j ⊢ φ → J ⊆ I
8 selvval.f ⊢ φ → F ∈ B
9 coeq2 ⊢ f = F → d ∘ f = d ∘ F
10 9 fveq2d ⊢ f = F → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F
11 10 fveq1d ⊢ f = F → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
12 11 csbeq2dv ⊢ f = F → ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
13 12 csbeq2dv ⊢ f = F → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
14 13 csbeq2dv ⊢ f = F → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
15 14 csbeq2dv ⊢ f = F → ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
16 reldmmpl ⊢ Rel ⁡ dom ⁡ mPoly
17 16 1 2 elbasov ⊢ F ∈ B → I ∈ V ∧ R ∈ V
18 8 17 syl ⊢ φ → I ∈ V ∧ R ∈ V
19 18 simpld ⊢ φ → I ∈ V
20 18 simprd ⊢ φ → R ∈ V
21 19 20 7 selvfval ⊢ φ → I selectVars R ⁡ J = f ∈ Base I mPoly R ⟼ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ f ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
22 1 fveq2i ⊢ Base P = Base I mPoly R
23 2 22 eqtri ⊢ B = Base I mPoly R
24 8 23 eleqtrdi ⊢ φ → F ∈ Base I mPoly R
25 fvex ⊢ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
26 25 csbex ⊢ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
27 26 csbex ⊢ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
28 27 csbex ⊢ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
29 28 csbex ⊢ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
30 29 a1i ⊢ φ → ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x ∈ V
31 15 21 24 30 fvmptd4 ⊢ φ → I selectVars R ⁡ J ⁡ F = ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x
32 ovex ⊢ I ∖ J mPoly R ∈ V
33 3 eqeq2i ⊢ u = U ↔ u = I ∖ J mPoly R
34 oveq2 ⊢ u = U → J mPoly u = J mPoly U
35 fveq2 ⊢ u = U → algSc ⁡ u = algSc ⁡ U
36 35 coeq2d ⊢ u = U → c ∘ algSc ⁡ u = c ∘ algSc ⁡ U
37 oveq2 ⊢ u = U → J mVar u = J mVar U
38 37 fveq1d ⊢ u = U → J mVar u ⁡ x = J mVar U ⁡ x
39 38 ifeq1d ⊢ u = U → if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
40 39 mpteq2dv ⊢ u = U → x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
41 40 fveq2d ⊢ u = U → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
42 36 41 csbeq12dv ⊢ u = U → ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
43 42 csbeq2dv ⊢ u = U → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
44 34 43 csbeq12dv ⊢ u = U → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ J mPoly U / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
45 ovex ⊢ J mPoly U ∈ V
46 4 eqeq2i ⊢ t = T ↔ t = J mPoly U
47 fveq2 ⊢ t = T → algSc ⁡ t = algSc ⁡ T
48 oveq2 ⊢ t = T → I evalSub t = I evalSub T
49 48 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d = I evalSub T ⁡ ran ⁡ d
50 49 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F
51 50 fveq1d ⊢ t = T → I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
52 51 csbeq2dv ⊢ t = T → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
53 47 52 csbeq12dv ⊢ t = T → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ algSc ⁡ T / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x
54 fvex ⊢ algSc ⁡ T ∈ V
55 5 eqeq2i ⊢ c = C ↔ c = algSc ⁡ T
56 coeq1 ⊢ c = C → c ∘ algSc ⁡ U = C ∘ algSc ⁡ U
57 fveq1 ⊢ c = C → c ⁡ I ∖ J mVar R ⁡ x = C ⁡ I ∖ J mVar R ⁡ x
58 57 ifeq2d ⊢ c = C → if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
59 58 mpteq2dv ⊢ c = C → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
60 59 fveq2d ⊢ c = C → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
61 56 60 csbeq12dv ⊢ c = C → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = ⦋ C ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
62 5 fvexi ⊢ C ∈ V
63 fvex ⊢ algSc ⁡ U ∈ V
64 62 63 coex ⊢ C ∘ algSc ⁡ U ∈ V
65 6 eqeq2i ⊢ d = D ↔ d = C ∘ algSc ⁡ U
66 rneq ⊢ d = D → ran ⁡ d = ran ⁡ D
67 66 fveq2d ⊢ d = D → I evalSub T ⁡ ran ⁡ d = I evalSub T ⁡ ran ⁡ D
68 coeq1 ⊢ d = D → d ∘ F = D ∘ F
69 67 68 fveq12d ⊢ d = D → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F
70 69 fveq1d ⊢ d = D → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
71 65 70 sylbir ⊢ d = C ∘ algSc ⁡ U → I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
72 64 71 csbie ⊢ ⦋ C ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
73 61 72 eqtrdi ⊢ c = C → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
74 55 73 sylbir ⊢ c = algSc ⁡ T → ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
75 54 74 csbie ⊢ ⦋ algSc ⁡ T / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub T ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
76 53 75 eqtrdi ⊢ t = T → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
77 46 76 sylbir ⊢ t = J mPoly U → ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
78 45 77 csbie ⊢ ⦋ J mPoly U / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ U / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
79 44 78 eqtrdi ⊢ u = U → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
80 33 79 sylbir ⊢ u = I ∖ J mPoly R → ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
81 32 80 csbie ⊢ ⦋ I ∖ J mPoly R / u⦌ ⦋ J mPoly u / t⦌ ⦋ algSc ⁡ t / c⦌ ⦋ c ∘ algSc ⁡ u / d⦌ I evalSub t ⁡ ran ⁡ d ⁡ d ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar u ⁡ x c ⁡ I ∖ J mVar R ⁡ x = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
82 31 81 eqtrdi ⊢ φ → I selectVars R ⁡ J ⁡ F = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x