Detailed syntax breakdown of Definition df-sfl1
Step | Hyp | Ref
| Expression |
1 | | csf1 33330 |
. 2
class
splitFld1 |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vj |
. . 3
setvar 𝑗 |
4 | | cvv 3420 |
. . 3
class
V |
5 | | vp |
. . . 4
setvar 𝑝 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑟 |
7 | | cpl1 21122 |
. . . . 5
class
Poly1 |
8 | 6, 7 | cfv 6397 |
. . . 4
class
(Poly1‘𝑟) |
9 | | c1 10754 |
. . . . . . 7
class
1 |
10 | 5 | cv 1542 |
. . . . . . . 8
class 𝑝 |
11 | | cdg1 24973 |
. . . . . . . 8
class
deg1 |
12 | 6, 10, 11 | co 7231 |
. . . . . . 7
class (𝑟 deg1 𝑝) |
13 | | cfz 13119 |
. . . . . . 7
class
... |
14 | 9, 12, 13 | co 7231 |
. . . . . 6
class
(1...(𝑟
deg1 𝑝)) |
15 | | ccrd 9575 |
. . . . . 6
class
card |
16 | 14, 15 | cfv 6397 |
. . . . 5
class
(card‘(1...(𝑟
deg1 𝑝))) |
17 | | vs |
. . . . . . 7
setvar 𝑠 |
18 | | vf |
. . . . . . 7
setvar 𝑓 |
19 | | vm |
. . . . . . . 8
setvar 𝑚 |
20 | 17 | cv 1542 |
. . . . . . . . 9
class 𝑠 |
21 | | cmpl 20889 |
. . . . . . . . 9
class
mPoly |
22 | 20, 21 | cfv 6397 |
. . . . . . . 8
class ( mPoly
‘𝑠) |
23 | | vb |
. . . . . . . . 9
setvar 𝑏 |
24 | | vg |
. . . . . . . . . . . . 13
setvar 𝑔 |
25 | 24 | cv 1542 |
. . . . . . . . . . . 12
class 𝑔 |
26 | 18 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑓 |
27 | 10, 26 | ccom 5569 |
. . . . . . . . . . . 12
class (𝑝 ∘ 𝑓) |
28 | 19 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑚 |
29 | | cdsr 19680 |
. . . . . . . . . . . . 13
class
∥r |
30 | 28, 29 | cfv 6397 |
. . . . . . . . . . . 12
class
(∥r‘𝑚) |
31 | 25, 27, 30 | wbr 5067 |
. . . . . . . . . . 11
wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) |
32 | 20, 25, 11 | co 7231 |
. . . . . . . . . . . 12
class (𝑠 deg1 𝑔) |
33 | | clt 10891 |
. . . . . . . . . . . 12
class
< |
34 | 9, 32, 33 | wbr 5067 |
. . . . . . . . . . 11
wff 1 <
(𝑠 deg1 𝑔) |
35 | 31, 34 | wa 399 |
. . . . . . . . . 10
wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔)) |
36 | | cmn1 25047 |
. . . . . . . . . . . 12
class
Monic1p |
37 | 20, 36 | cfv 6397 |
. . . . . . . . . . 11
class
(Monic1p‘𝑠) |
38 | | cir 19682 |
. . . . . . . . . . . 12
class
Irred |
39 | 28, 38 | cfv 6397 |
. . . . . . . . . . 11
class
(Irred‘𝑚) |
40 | 37, 39 | cin 3879 |
. . . . . . . . . 10
class
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) |
41 | 35, 24, 40 | crab 3066 |
. . . . . . . . 9
class {𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} |
42 | | c0g 16968 |
. . . . . . . . . . . . 13
class
0g |
43 | 28, 42 | cfv 6397 |
. . . . . . . . . . . 12
class
(0g‘𝑚) |
44 | 27, 43 | wceq 1543 |
. . . . . . . . . . 11
wff (𝑝 ∘ 𝑓) = (0g‘𝑚) |
45 | 23 | cv 1542 |
. . . . . . . . . . . 12
class 𝑏 |
46 | | c0 4251 |
. . . . . . . . . . . 12
class
∅ |
47 | 45, 46 | wceq 1543 |
. . . . . . . . . . 11
wff 𝑏 = ∅ |
48 | 44, 47 | wo 847 |
. . . . . . . . . 10
wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅) |
49 | 20, 26 | cop 4561 |
. . . . . . . . . 10
class
〈𝑠, 𝑓〉 |
50 | | vh |
. . . . . . . . . . 11
setvar ℎ |
51 | | cglb 17841 |
. . . . . . . . . . . 12
class
glb |
52 | 45, 51 | cfv 6397 |
. . . . . . . . . . 11
class
(glb‘𝑏) |
53 | | vt |
. . . . . . . . . . . 12
setvar 𝑡 |
54 | 50 | cv 1542 |
. . . . . . . . . . . . 13
class ℎ |
55 | | cpfl 33329 |
. . . . . . . . . . . . 13
class
polyFld |
56 | 20, 54, 55 | co 7231 |
. . . . . . . . . . . 12
class (𝑠 polyFld ℎ) |
57 | 53 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑡 |
58 | | c1st 7777 |
. . . . . . . . . . . . . 14
class
1st |
59 | 57, 58 | cfv 6397 |
. . . . . . . . . . . . 13
class
(1st ‘𝑡) |
60 | | c2nd 7778 |
. . . . . . . . . . . . . . 15
class
2nd |
61 | 57, 60 | cfv 6397 |
. . . . . . . . . . . . . 14
class
(2nd ‘𝑡) |
62 | 26, 61 | ccom 5569 |
. . . . . . . . . . . . 13
class (𝑓 ∘ (2nd
‘𝑡)) |
63 | 59, 62 | cop 4561 |
. . . . . . . . . . . 12
class
〈(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))〉 |
64 | 53, 56, 63 | csb 3825 |
. . . . . . . . . . 11
class
⦋(𝑠
polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉 |
65 | 50, 52, 64 | csb 3825 |
. . . . . . . . . 10
class
⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉 |
66 | 48, 49, 65 | cif 4453 |
. . . . . . . . 9
class
if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
67 | 23, 41, 66 | csb 3825 |
. . . . . . . 8
class
⦋{𝑔
∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
68 | 19, 22, 67 | csb 3825 |
. . . . . . 7
class
⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
69 | 17, 18, 4, 4, 68 | cmpo 7233 |
. . . . . 6
class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly
‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)) |
70 | 3 | cv 1542 |
. . . . . 6
class 𝑗 |
71 | 69, 70 | crdg 8165 |
. . . . 5
class
rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗) |
72 | 16, 71 | cfv 6397 |
. . . 4
class
(rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝)))) |
73 | 5, 8, 72 | cmpt 5149 |
. . 3
class (𝑝 ∈
(Poly1‘𝑟)
↦ (rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))) |
74 | 2, 3, 4, 4, 73 | cmpo 7233 |
. 2
class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly
‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝)))))) |
75 | 1, 74 | wceq 1543 |
1
wff
splitFld1 = (𝑟
∈ V, 𝑗 ∈ V
↦ (𝑝 ∈
(Poly1‘𝑟)
↦ (rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝)))))) |