Detailed syntax breakdown of Definition df-selv
Step | Hyp | Ref
| Expression |
1 | | cslv 19539 |
. 2
class
selectVars |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3200 |
. . 3
class
V |
5 | | vj |
. . . 4
setvar 𝑗 |
6 | 2 | cv 1482 |
. . . . 5
class 𝑖 |
7 | 6 | cpw 4158 |
. . . 4
class 𝒫
𝑖 |
8 | | vf |
. . . . 5
setvar 𝑓 |
9 | 3 | cv 1482 |
. . . . . 6
class 𝑟 |
10 | | cmpl 19353 |
. . . . . 6
class
mPoly |
11 | 6, 9, 10 | co 6650 |
. . . . 5
class (𝑖 mPoly 𝑟) |
12 | | vs |
. . . . . 6
setvar 𝑠 |
13 | 5 | cv 1482 |
. . . . . . . 8
class 𝑗 |
14 | 6, 13 | cdif 3571 |
. . . . . . 7
class (𝑖 ∖ 𝑗) |
15 | 14, 9, 10 | co 6650 |
. . . . . 6
class ((𝑖 ∖ 𝑗) mPoly 𝑟) |
16 | | vc |
. . . . . . 7
setvar 𝑐 |
17 | | vx |
. . . . . . . 8
setvar 𝑥 |
18 | 12 | cv 1482 |
. . . . . . . . 9
class 𝑠 |
19 | | csca 15944 |
. . . . . . . . 9
class
Scalar |
20 | 18, 19 | cfv 5888 |
. . . . . . . 8
class
(Scalar‘𝑠) |
21 | 17 | cv 1482 |
. . . . . . . . 9
class 𝑥 |
22 | | cur 18501 |
. . . . . . . . . 10
class
1r |
23 | 18, 22 | cfv 5888 |
. . . . . . . . 9
class
(1r‘𝑠) |
24 | | cvsca 15945 |
. . . . . . . . . 10
class
·𝑠 |
25 | 18, 24 | cfv 5888 |
. . . . . . . . 9
class (
·𝑠 ‘𝑠) |
26 | 21, 23, 25 | co 6650 |
. . . . . . . 8
class (𝑥(
·𝑠 ‘𝑠)(1r‘𝑠)) |
27 | 17, 20, 26 | cmpt 4729 |
. . . . . . 7
class (𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) |
28 | 17, 5 | wel 1991 |
. . . . . . . . . 10
wff 𝑥 ∈ 𝑗 |
29 | | cmvr 19352 |
. . . . . . . . . . . 12
class
mVar |
30 | 13, 15, 29 | co 6650 |
. . . . . . . . . . 11
class (𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟)) |
31 | 21, 30 | cfv 5888 |
. . . . . . . . . 10
class ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥) |
32 | 16 | cv 1482 |
. . . . . . . . . . 11
class 𝑐 |
33 | 14, 9, 29 | co 6650 |
. . . . . . . . . . . 12
class ((𝑖 ∖ 𝑗) mVar 𝑟) |
34 | 21, 33 | cfv 5888 |
. . . . . . . . . . 11
class (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥) |
35 | 32, 34 | ccom 5118 |
. . . . . . . . . 10
class (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)) |
36 | 28, 31, 35 | cif 4086 |
. . . . . . . . 9
class if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))) |
37 | 17, 6, 36 | cmpt 4729 |
. . . . . . . 8
class (𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))) |
38 | 8 | cv 1482 |
. . . . . . . . . 10
class 𝑓 |
39 | 32, 38 | ccom 5118 |
. . . . . . . . 9
class (𝑐 ∘ 𝑓) |
40 | | cimas 16164 |
. . . . . . . . . . 11
class
“s |
41 | 32, 9, 40 | co 6650 |
. . . . . . . . . 10
class (𝑐 “s
𝑟) |
42 | | ces 19504 |
. . . . . . . . . . 11
class
evalSub |
43 | 6, 18, 42 | co 6650 |
. . . . . . . . . 10
class (𝑖 evalSub 𝑠) |
44 | 41, 43 | cfv 5888 |
. . . . . . . . 9
class ((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟)) |
45 | 39, 44 | cfv 5888 |
. . . . . . . 8
class (((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓)) |
46 | 37, 45 | cfv 5888 |
. . . . . . 7
class ((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))) |
47 | 16, 27, 46 | csb 3533 |
. . . . . 6
class
⦋(𝑥
∈ (Scalar‘𝑠)
↦ (𝑥(
·𝑠 ‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))) |
48 | 12, 15, 47 | csb 3533 |
. . . . 5
class
⦋((𝑖
∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))) |
49 | 8, 11, 48 | cmpt 4729 |
. . . 4
class (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))) |
50 | 5, 7, 49 | cmpt 4729 |
. . 3
class (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥))))))) |
51 | 2, 3, 4, 4, 50 | cmpt2 6652 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))))) |
52 | 1, 51 | wceq 1483 |
1
wff selectVars
= (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑓 ∈ (𝑖 mPoly 𝑟) ↦ ⦋((𝑖 ∖ 𝑗) mPoly 𝑟) / 𝑠⦌⦋(𝑥 ∈ (Scalar‘𝑠) ↦ (𝑥( ·𝑠
‘𝑠)(1r‘𝑠))) / 𝑐⦌((((𝑖 evalSub 𝑠)‘(𝑐 “s 𝑟))‘(𝑐 ∘ 𝑓))‘(𝑥 ∈ 𝑖 ↦ if(𝑥 ∈ 𝑗, ((𝑗 mVar ((𝑖 ∖ 𝑗) mPoly 𝑟))‘𝑥), (𝑐 ∘ (((𝑖 ∖ 𝑗) mVar 𝑟)‘𝑥)))))))) |