Step | Hyp | Ref
| Expression |
1 | | cpfl 34616 |
. 2
class
polyFld |
2 | | vr |
. . 3
setvar π |
3 | | vp |
. . 3
setvar π |
4 | | cvv 3474 |
. . 3
class
V |
5 | | vs |
. . . 4
setvar π |
6 | 2 | cv 1540 |
. . . . 5
class π |
7 | | cpl1 21700 |
. . . . 5
class
Poly1 |
8 | 6, 7 | cfv 6543 |
. . . 4
class
(Poly1βπ) |
9 | | vi |
. . . . 5
setvar π |
10 | 3 | cv 1540 |
. . . . . . 7
class π |
11 | 10 | csn 4628 |
. . . . . 6
class {π} |
12 | 5 | cv 1540 |
. . . . . . 7
class π |
13 | | crsp 20783 |
. . . . . . 7
class
RSpan |
14 | 12, 13 | cfv 6543 |
. . . . . 6
class
(RSpanβπ ) |
15 | 11, 14 | cfv 6543 |
. . . . 5
class
((RSpanβπ )β{π}) |
16 | | vf |
. . . . . 6
setvar π |
17 | | vz |
. . . . . . 7
setvar π§ |
18 | | cbs 17143 |
. . . . . . . 8
class
Base |
19 | 6, 18 | cfv 6543 |
. . . . . . 7
class
(Baseβπ) |
20 | 17 | cv 1540 |
. . . . . . . . 9
class π§ |
21 | | cur 20003 |
. . . . . . . . . 10
class
1r |
22 | 12, 21 | cfv 6543 |
. . . . . . . . 9
class
(1rβπ ) |
23 | | cvsca 17200 |
. . . . . . . . . 10
class
Β·π |
24 | 12, 23 | cfv 6543 |
. . . . . . . . 9
class (
Β·π βπ ) |
25 | 20, 22, 24 | co 7408 |
. . . . . . . 8
class (π§(
Β·π βπ )(1rβπ )) |
26 | 9 | cv 1540 |
. . . . . . . . 9
class π |
27 | | cqg 19001 |
. . . . . . . . 9
class
~QG |
28 | 12, 26, 27 | co 7408 |
. . . . . . . 8
class (π ~QG π) |
29 | 25, 28 | cec 8700 |
. . . . . . 7
class [(π§(
Β·π βπ )(1rβπ ))](π ~QG π) |
30 | 17, 19, 29 | cmpt 5231 |
. . . . . 6
class (π§ β (Baseβπ) β¦ [(π§( Β·π
βπ )(1rβπ ))](π ~QG π)) |
31 | | vt |
. . . . . . . 8
setvar π‘ |
32 | | cqus 17450 |
. . . . . . . . 9
class
/s |
33 | 12, 28, 32 | co 7408 |
. . . . . . . 8
class (π /s (π ~QG π)) |
34 | 31 | cv 1540 |
. . . . . . . . . 10
class π‘ |
35 | | vn |
. . . . . . . . . . . . . 14
setvar π |
36 | 35 | cv 1540 |
. . . . . . . . . . . . 13
class π |
37 | 16 | cv 1540 |
. . . . . . . . . . . . 13
class π |
38 | 36, 37 | ccom 5680 |
. . . . . . . . . . . 12
class (π β π) |
39 | | cnm 24084 |
. . . . . . . . . . . . 13
class
norm |
40 | 6, 39 | cfv 6543 |
. . . . . . . . . . . 12
class
(normβπ) |
41 | 38, 40 | wceq 1541 |
. . . . . . . . . . 11
wff (π β π) = (normβπ) |
42 | | cabv 20423 |
. . . . . . . . . . . 12
class
AbsVal |
43 | 34, 42 | cfv 6543 |
. . . . . . . . . . 11
class
(AbsValβπ‘) |
44 | 41, 35, 43 | crio 7363 |
. . . . . . . . . 10
class
(β©π
β (AbsValβπ‘)(π β π) = (normβπ)) |
45 | | ctng 24086 |
. . . . . . . . . 10
class
toNrmGrp |
46 | 34, 44, 45 | co 7408 |
. . . . . . . . 9
class (π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) |
47 | | cnx 17125 |
. . . . . . . . . . 11
class
ndx |
48 | | cple 17203 |
. . . . . . . . . . 11
class
le |
49 | 47, 48 | cfv 6543 |
. . . . . . . . . 10
class
(leβndx) |
50 | | vg |
. . . . . . . . . . 11
setvar π |
51 | 34, 18 | cfv 6543 |
. . . . . . . . . . . 12
class
(Baseβπ‘) |
52 | | vq |
. . . . . . . . . . . . . . . 16
setvar π |
53 | 52 | cv 1540 |
. . . . . . . . . . . . . . 15
class π |
54 | | cdg1 25568 |
. . . . . . . . . . . . . . 15
class
deg1 |
55 | 6, 53, 54 | co 7408 |
. . . . . . . . . . . . . 14
class (π deg1 π) |
56 | 6, 10, 54 | co 7408 |
. . . . . . . . . . . . . 14
class (π deg1 π) |
57 | | clt 11247 |
. . . . . . . . . . . . . 14
class
< |
58 | 55, 56, 57 | wbr 5148 |
. . . . . . . . . . . . 13
wff (π deg1 π) < (π deg1 π) |
59 | 58, 52, 20 | crio 7363 |
. . . . . . . . . . . 12
class
(β©π
β π§ (π deg1 π) < (π deg1 π)) |
60 | 17, 51, 59 | cmpt 5231 |
. . . . . . . . . . 11
class (π§ β (Baseβπ‘) β¦ (β©π β π§ (π deg1 π) < (π deg1 π))) |
61 | 50 | cv 1540 |
. . . . . . . . . . . . 13
class π |
62 | 61 | ccnv 5675 |
. . . . . . . . . . . 12
class β‘π |
63 | 12, 48 | cfv 6543 |
. . . . . . . . . . . . 13
class
(leβπ ) |
64 | 63, 61 | ccom 5680 |
. . . . . . . . . . . 12
class
((leβπ )
β π) |
65 | 62, 64 | ccom 5680 |
. . . . . . . . . . 11
class (β‘π β ((leβπ ) β π)) |
66 | 50, 60, 65 | csb 3893 |
. . . . . . . . . 10
class
β¦(π§
β (Baseβπ‘)
β¦ (β©π
β π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π)) |
67 | 49, 66 | cop 4634 |
. . . . . . . . 9
class
β¨(leβndx), β¦(π§ β (Baseβπ‘) β¦ (β©π β π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β© |
68 | | csts 17095 |
. . . . . . . . 9
class
sSet |
69 | 46, 67, 68 | co 7408 |
. . . . . . . 8
class ((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β
π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©) |
70 | 31, 33, 69 | csb 3893 |
. . . . . . 7
class
β¦(π
/s (π
~QG π)) /
π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β
π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©) |
71 | 70, 37 | cop 4634 |
. . . . . 6
class
β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β
π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ© |
72 | 16, 30, 71 | csb 3893 |
. . . . 5
class
β¦(π§
β (Baseβπ)
β¦ [(π§(
Β·π βπ )(1rβπ ))](π ~QG π)) / πβ¦β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β
π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ© |
73 | 9, 15, 72 | csb 3893 |
. . . 4
class
β¦((RSpanβπ )β{π}) / πβ¦β¦(π§ β (Baseβπ) β¦ [(π§( Β·π
βπ )(1rβπ ))](π ~QG π)) / πβ¦β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β
π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ© |
74 | 5, 8, 73 | csb 3893 |
. . 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 7410 |
. 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 1541 |
1
wff polyFld =
(π β V, π β V β¦
β¦(Poly1βπ) / π β¦β¦((RSpanβπ )β{π}) / πβ¦β¦(π§ β (Baseβπ) β¦ [(π§( Β·π
βπ )(1rβπ ))](π ~QG π)) / πβ¦β¨β¦(π /s (π ~QG π)) / π‘β¦((π‘ toNrmGrp (β©π β (AbsValβπ‘)(π β π) = (normβπ))) sSet β¨(leβndx),
β¦(π§ β
(Baseβπ‘) β¦
(β©π β π§ (π deg1 π) < (π deg1 π))) / πβ¦(β‘π β ((leβπ ) β π))β©), πβ©) |