Detailed syntax breakdown of Definition df-sfl1
Step | Hyp | Ref
| Expression |
1 | | csf1 35599 |
. 2
class
splitFld1 |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vj |
. . 3
setvar 𝑗 |
4 | | cvv 3488 |
. . 3
class
V |
5 | | vp |
. . . 4
setvar 𝑝 |
6 | 2 | cv 1536 |
. . . . 5
class 𝑟 |
7 | | cpl1 22199 |
. . . . 5
class
Poly1 |
8 | 6, 7 | cfv 6573 |
. . . 4
class
(Poly1‘𝑟) |
9 | | c1 11185 |
. . . . . . 7
class
1 |
10 | 5 | cv 1536 |
. . . . . . . 8
class 𝑝 |
11 | | cdg1 26113 |
. . . . . . . 8
class
deg1 |
12 | 6, 10, 11 | co 7448 |
. . . . . . 7
class (𝑟deg1𝑝) |
13 | | cfz 13567 |
. . . . . . 7
class
... |
14 | 9, 12, 13 | co 7448 |
. . . . . 6
class
(1...(𝑟deg1𝑝)) |
15 | | ccrd 10004 |
. . . . . 6
class
card |
16 | 14, 15 | cfv 6573 |
. . . . 5
class
(card‘(1...(𝑟deg1𝑝))) |
17 | | vs |
. . . . . . 7
setvar 𝑠 |
18 | | vf |
. . . . . . 7
setvar 𝑓 |
19 | | vm |
. . . . . . . 8
setvar 𝑚 |
20 | 17 | cv 1536 |
. . . . . . . . 9
class 𝑠 |
21 | 20, 7 | cfv 6573 |
. . . . . . . 8
class
(Poly1‘𝑠) |
22 | | vb |
. . . . . . . . 9
setvar 𝑏 |
23 | | vg |
. . . . . . . . . . . . 13
setvar 𝑔 |
24 | 23 | cv 1536 |
. . . . . . . . . . . 12
class 𝑔 |
25 | 18 | cv 1536 |
. . . . . . . . . . . . 13
class 𝑓 |
26 | 10, 25 | ccom 5704 |
. . . . . . . . . . . 12
class (𝑝 ∘ 𝑓) |
27 | 19 | cv 1536 |
. . . . . . . . . . . . 13
class 𝑚 |
28 | | cdsr 20380 |
. . . . . . . . . . . . 13
class
∥r |
29 | 27, 28 | cfv 6573 |
. . . . . . . . . . . 12
class
(∥r‘𝑚) |
30 | 24, 26, 29 | wbr 5166 |
. . . . . . . . . . 11
wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) |
31 | 20, 24, 11 | co 7448 |
. . . . . . . . . . . 12
class (𝑠deg1𝑔) |
32 | | clt 11324 |
. . . . . . . . . . . 12
class
< |
33 | 9, 31, 32 | wbr 5166 |
. . . . . . . . . . 11
wff 1 <
(𝑠deg1𝑔) |
34 | 30, 33 | wa 395 |
. . . . . . . . . 10
wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔)) |
35 | | cmn1 26185 |
. . . . . . . . . . . 12
class
Monic1p |
36 | 20, 35 | cfv 6573 |
. . . . . . . . . . 11
class
(Monic1p‘𝑠) |
37 | | cir 20382 |
. . . . . . . . . . . 12
class
Irred |
38 | 27, 37 | cfv 6573 |
. . . . . . . . . . 11
class
(Irred‘𝑚) |
39 | 36, 38 | cin 3975 |
. . . . . . . . . 10
class
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) |
40 | 34, 23, 39 | crab 3443 |
. . . . . . . . 9
class {𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} |
41 | | c0g 17499 |
. . . . . . . . . . . . 13
class
0g |
42 | 27, 41 | cfv 6573 |
. . . . . . . . . . . 12
class
(0g‘𝑚) |
43 | 26, 42 | wceq 1537 |
. . . . . . . . . . 11
wff (𝑝 ∘ 𝑓) = (0g‘𝑚) |
44 | 22 | cv 1536 |
. . . . . . . . . . . 12
class 𝑏 |
45 | | c0 4352 |
. . . . . . . . . . . 12
class
∅ |
46 | 44, 45 | wceq 1537 |
. . . . . . . . . . 11
wff 𝑏 = ∅ |
47 | 43, 46 | wo 846 |
. . . . . . . . . 10
wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅) |
48 | 20, 25 | cop 4654 |
. . . . . . . . . 10
class
〈𝑠, 𝑓〉 |
49 | | vh |
. . . . . . . . . . 11
setvar ℎ |
50 | | cglb 18380 |
. . . . . . . . . . . 12
class
glb |
51 | 44, 50 | cfv 6573 |
. . . . . . . . . . 11
class
(glb‘𝑏) |
52 | | vt |
. . . . . . . . . . . 12
setvar 𝑡 |
53 | 49 | cv 1536 |
. . . . . . . . . . . . 13
class ℎ |
54 | | cpfl 35598 |
. . . . . . . . . . . . 13
class
polyFld |
55 | 20, 53, 54 | co 7448 |
. . . . . . . . . . . 12
class (𝑠 polyFld ℎ) |
56 | 52 | cv 1536 |
. . . . . . . . . . . . . 14
class 𝑡 |
57 | | c1st 8028 |
. . . . . . . . . . . . . 14
class
1st |
58 | 56, 57 | cfv 6573 |
. . . . . . . . . . . . 13
class
(1st ‘𝑡) |
59 | | c2nd 8029 |
. . . . . . . . . . . . . . 15
class
2nd |
60 | 56, 59 | cfv 6573 |
. . . . . . . . . . . . . 14
class
(2nd ‘𝑡) |
61 | 25, 60 | ccom 5704 |
. . . . . . . . . . . . 13
class (𝑓 ∘ (2nd
‘𝑡)) |
62 | 58, 61 | cop 4654 |
. . . . . . . . . . . 12
class
〈(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))〉 |
63 | 52, 55, 62 | csb 3921 |
. . . . . . . . . . 11
class
⦋(𝑠
polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉 |
64 | 49, 51, 63 | csb 3921 |
. . . . . . . . . 10
class
⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉 |
65 | 47, 48, 64 | cif 4548 |
. . . . . . . . 9
class
if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
66 | 22, 40, 65 | csb 3921 |
. . . . . . . 8
class
⦋{𝑔
∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
67 | 19, 21, 66 | csb 3921 |
. . . . . . 7
class
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉) |
68 | 17, 18, 4, 4, 67 | cmpo 7450 |
. . . . . 6
class (𝑠 ∈ V, 𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)) |
69 | 3 | cv 1536 |
. . . . . 6
class 𝑗 |
70 | 68, 69 | crdg 8465 |
. . . . 5
class
rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗) |
71 | 16, 70 | cfv 6573 |
. . . 4
class
(rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))) |
72 | 5, 8, 71 | cmpt 5249 |
. . 3
class (𝑝 ∈
(Poly1‘𝑟)
↦ (rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))) |
73 | 2, 3, 4, 4, 72 | cmpo 7450 |
. 2
class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))))) |
74 | 1, 73 | wceq 1537 |
1
wff
splitFld1 = (𝑟
∈ V, 𝑗 ∈ V
↦ (𝑝 ∈
(Poly1‘𝑟)
↦ (rec((𝑠 ∈ V,
𝑓 ∈ V ↦
⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈
((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), 〈𝑠, 𝑓〉, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌〈(1st
‘𝑡), (𝑓 ∘ (2nd
‘𝑡))〉)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))))) |