Detailed syntax breakdown of Definition df-plfl
Step | Hyp | Ref
| Expression |
1 | | cpfl 33329 |
. 2
class
polyFld |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vp |
. . 3
setvar 𝑝 |
4 | | cvv 3421 |
. . 3
class
V |
5 | | vs |
. . . 4
setvar 𝑠 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑟 |
7 | | cpl1 21122 |
. . . . 5
class
Poly1 |
8 | 6, 7 | cfv 6398 |
. . . 4
class
(Poly1‘𝑟) |
9 | | vi |
. . . . 5
setvar 𝑖 |
10 | 3 | cv 1542 |
. . . . . . 7
class 𝑝 |
11 | 10 | csn 4556 |
. . . . . 6
class {𝑝} |
12 | 5 | cv 1542 |
. . . . . . 7
class 𝑠 |
13 | | crsp 20233 |
. . . . . . 7
class
RSpan |
14 | 12, 13 | cfv 6398 |
. . . . . 6
class
(RSpan‘𝑠) |
15 | 11, 14 | cfv 6398 |
. . . . 5
class
((RSpan‘𝑠)‘{𝑝}) |
16 | | vf |
. . . . . 6
setvar 𝑓 |
17 | | vz |
. . . . . . 7
setvar 𝑧 |
18 | | cbs 16785 |
. . . . . . . 8
class
Base |
19 | 6, 18 | cfv 6398 |
. . . . . . 7
class
(Base‘𝑟) |
20 | 17 | cv 1542 |
. . . . . . . . 9
class 𝑧 |
21 | | cur 19541 |
. . . . . . . . . 10
class
1r |
22 | 12, 21 | cfv 6398 |
. . . . . . . . 9
class
(1r‘𝑠) |
23 | | cvsca 16831 |
. . . . . . . . . 10
class
·𝑠 |
24 | 12, 23 | cfv 6398 |
. . . . . . . . 9
class (
·𝑠 ‘𝑠) |
25 | 20, 22, 24 | co 7232 |
. . . . . . . 8
class (𝑧(
·𝑠 ‘𝑠)(1r‘𝑠)) |
26 | 9 | cv 1542 |
. . . . . . . . 9
class 𝑖 |
27 | | cqg 18564 |
. . . . . . . . 9
class
~QG |
28 | 12, 26, 27 | co 7232 |
. . . . . . . 8
class (𝑠 ~QG 𝑖) |
29 | 25, 28 | cec 8410 |
. . . . . . 7
class [(𝑧(
·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖) |
30 | 17, 19, 29 | cmpt 5150 |
. . . . . 6
class (𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠
‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) |
31 | | vt |
. . . . . . . 8
setvar 𝑡 |
32 | | cqus 17035 |
. . . . . . . . 9
class
/s |
33 | 12, 28, 32 | co 7232 |
. . . . . . . 8
class (𝑠 /s (𝑠 ~QG 𝑖)) |
34 | 31 | cv 1542 |
. . . . . . . . . 10
class 𝑡 |
35 | | vn |
. . . . . . . . . . . . . 14
setvar 𝑛 |
36 | 35 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑛 |
37 | 16 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑓 |
38 | 36, 37 | ccom 5570 |
. . . . . . . . . . . 12
class (𝑛 ∘ 𝑓) |
39 | | cnm 23498 |
. . . . . . . . . . . . 13
class
norm |
40 | 6, 39 | cfv 6398 |
. . . . . . . . . . . 12
class
(norm‘𝑟) |
41 | 38, 40 | wceq 1543 |
. . . . . . . . . . 11
wff (𝑛 ∘ 𝑓) = (norm‘𝑟) |
42 | | cabv 19877 |
. . . . . . . . . . . 12
class
AbsVal |
43 | 34, 42 | cfv 6398 |
. . . . . . . . . . 11
class
(AbsVal‘𝑡) |
44 | 41, 35, 43 | crio 7188 |
. . . . . . . . . 10
class
(℩𝑛
∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟)) |
45 | | ctng 23500 |
. . . . . . . . . 10
class
toNrmGrp |
46 | 34, 44, 45 | co 7232 |
. . . . . . . . 9
class (𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) |
47 | | cnx 16769 |
. . . . . . . . . . 11
class
ndx |
48 | | cple 16834 |
. . . . . . . . . . 11
class
le |
49 | 47, 48 | cfv 6398 |
. . . . . . . . . 10
class
(le‘ndx) |
50 | | vg |
. . . . . . . . . . 11
setvar 𝑔 |
51 | 34, 18 | cfv 6398 |
. . . . . . . . . . . 12
class
(Base‘𝑡) |
52 | | vq |
. . . . . . . . . . . . . . . 16
setvar 𝑞 |
53 | 52 | cv 1542 |
. . . . . . . . . . . . . . 15
class 𝑞 |
54 | | cdg1 24973 |
. . . . . . . . . . . . . . 15
class
deg1 |
55 | 6, 53, 54 | co 7232 |
. . . . . . . . . . . . . 14
class (𝑟 deg1 𝑞) |
56 | 6, 10, 54 | co 7232 |
. . . . . . . . . . . . . 14
class (𝑟 deg1 𝑝) |
57 | | clt 10892 |
. . . . . . . . . . . . . 14
class
< |
58 | 55, 56, 57 | wbr 5068 |
. . . . . . . . . . . . 13
wff (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝) |
59 | 58, 52, 20 | crio 7188 |
. . . . . . . . . . . 12
class
(℩𝑞
∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝)) |
60 | 17, 51, 59 | cmpt 5150 |
. . . . . . . . . . 11
class (𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) |
61 | 50 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑔 |
62 | 61 | ccnv 5565 |
. . . . . . . . . . . 12
class ◡𝑔 |
63 | 12, 48 | cfv 6398 |
. . . . . . . . . . . . 13
class
(le‘𝑠) |
64 | 63, 61 | ccom 5570 |
. . . . . . . . . . . 12
class
((le‘𝑠)
∘ 𝑔) |
65 | 62, 64 | ccom 5570 |
. . . . . . . . . . 11
class (◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔)) |
66 | 50, 60, 65 | csb 3826 |
. . . . . . . . . 10
class
⦋(𝑧
∈ (Base‘𝑡)
↦ (℩𝑞
∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔)) |
67 | 49, 66 | cop 4562 |
. . . . . . . . 9
class
〈(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉 |
68 | | csts 16741 |
. . . . . . . . 9
class
sSet |
69 | 46, 67, 68 | co 7232 |
. . . . . . . 8
class ((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈
𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉) |
70 | 31, 33, 69 | csb 3826 |
. . . . . . 7
class
⦋(𝑠
/s (𝑠
~QG 𝑖)) /
𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈
𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉) |
71 | 70, 37 | cop 4562 |
. . . . . 6
class
〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈
𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉 |
72 | 16, 30, 71 | csb 3826 |
. . . . 5
class
⦋(𝑧
∈ (Base‘𝑟)
↦ [(𝑧(
·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈
𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉 |
73 | 9, 15, 72 | csb 3826 |
. . . 4
class
⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠
‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈
𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉 |
74 | 5, 8, 73 | csb 3826 |
. . 3
class
⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠
‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉 |
75 | 2, 3, 4, 4, 74 | cmpo 7234 |
. 2
class (𝑟 ∈ V, 𝑝 ∈ V ↦
⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠
‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉) |
76 | 1, 75 | wceq 1543 |
1
wff polyFld =
(𝑟 ∈ V, 𝑝 ∈ V ↦
⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠
‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌〈⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet 〈(le‘ndx),
⦋(𝑧 ∈
(Base‘𝑡) ↦
(℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))〉), 𝑓〉) |