Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psl Structured version   Visualization version   GIF version

Definition df-psl 30584
Description: Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring 𝑟, a strict order on 𝑟, and a sequence 𝑝:ℕ⟶(𝒫 𝑟 ∩ Fin) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-psl polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑𝑚 ℕ) ↦ (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓((1st ∘ (𝑓 shift 1)) HomLim (2nd𝑓)))
Distinct variable group:   𝑒,𝑓,𝑔,𝑝,𝑞,𝑟,𝑠,𝑥

Detailed syntax breakdown of Definition df-psl
StepHypRef Expression
1 cpsl 30576 . 2 class polySplitLim
2 vr . . 3 setvar 𝑟
3 vp . . 3 setvar 𝑝
4 cvv 3172 . . 3 class V
52cv 1473 . . . . . . 7 class 𝑟
6 cbs 15643 . . . . . . 7 class Base
75, 6cfv 5789 . . . . . 6 class (Base‘𝑟)
87cpw 4107 . . . . 5 class 𝒫 (Base‘𝑟)
9 cfn 7818 . . . . 5 class Fin
108, 9cin 3538 . . . 4 class (𝒫 (Base‘𝑟) ∩ Fin)
11 cn 10869 . . . 4 class
12 cmap 7721 . . . 4 class 𝑚
1310, 11, 12co 6526 . . 3 class ((𝒫 (Base‘𝑟) ∩ Fin) ↑𝑚 ℕ)
14 vf . . . 4 setvar 𝑓
15 c1st 7034 . . . . 5 class 1st
16 vg . . . . . . 7 setvar 𝑔
17 vq . . . . . . 7 setvar 𝑞
18 ve . . . . . . . 8 setvar 𝑒
1916cv 1473 . . . . . . . . 9 class 𝑔
2019, 15cfv 5789 . . . . . . . 8 class (1st𝑔)
21 vs . . . . . . . . 9 setvar 𝑠
2218cv 1473 . . . . . . . . . 10 class 𝑒
2322, 15cfv 5789 . . . . . . . . 9 class (1st𝑒)
2421cv 1473 . . . . . . . . . . 11 class 𝑠
25 vx . . . . . . . . . . . . 13 setvar 𝑥
2617cv 1473 . . . . . . . . . . . . 13 class 𝑞
2725cv 1473 . . . . . . . . . . . . . 14 class 𝑥
28 c2nd 7035 . . . . . . . . . . . . . . 15 class 2nd
2919, 28cfv 5789 . . . . . . . . . . . . . 14 class (2nd𝑔)
3027, 29ccom 5031 . . . . . . . . . . . . 13 class (𝑥 ∘ (2nd𝑔))
3125, 26, 30cmpt 4637 . . . . . . . . . . . 12 class (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))
3231crn 5028 . . . . . . . . . . 11 class ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))
33 csf 30575 . . . . . . . . . . 11 class splitFld
3424, 32, 33co 6526 . . . . . . . . . 10 class (𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔))))
3514cv 1473 . . . . . . . . . . 11 class 𝑓
3635, 28cfv 5789 . . . . . . . . . . . 12 class (2nd𝑓)
3729, 36ccom 5031 . . . . . . . . . . 11 class ((2nd𝑔) ∘ (2nd𝑓))
3835, 37cop 4130 . . . . . . . . . 10 class 𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩
3914, 34, 38csb 3498 . . . . . . . . 9 class (𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩
4021, 23, 39csb 3498 . . . . . . . 8 class (1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩
4118, 20, 40csb 3498 . . . . . . 7 class (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩
4216, 17, 4, 4, 41cmpt2 6528 . . . . . 6 class (𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩)
433cv 1473 . . . . . . 7 class 𝑝
44 cc0 9792 . . . . . . . . 9 class 0
45 c0 3873 . . . . . . . . . . 11 class
465, 45cop 4130 . . . . . . . . . 10 class 𝑟, ∅⟩
47 cid 4937 . . . . . . . . . . 11 class I
4847, 7cres 5029 . . . . . . . . . 10 class ( I ↾ (Base‘𝑟))
4946, 48cop 4130 . . . . . . . . 9 class ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩
5044, 49cop 4130 . . . . . . . 8 class ⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩
5150csn 4124 . . . . . . 7 class {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}
5243, 51cun 3537 . . . . . 6 class (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩})
5342, 52, 44cseq 12620 . . . . 5 class seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))
5415, 53ccom 5031 . . . 4 class (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩})))
55 c1 9793 . . . . . . 7 class 1
56 cshi 13602 . . . . . . 7 class shift
5735, 55, 56co 6526 . . . . . 6 class (𝑓 shift 1)
5815, 57ccom 5031 . . . . 5 class (1st ∘ (𝑓 shift 1))
5928, 35ccom 5031 . . . . 5 class (2nd𝑓)
60 chlim 30572 . . . . 5 class HomLim
6158, 59, 60co 6526 . . . 4 class ((1st ∘ (𝑓 shift 1)) HomLim (2nd𝑓))
6214, 54, 61csb 3498 . . 3 class (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓((1st ∘ (𝑓 shift 1)) HomLim (2nd𝑓))
632, 3, 4, 13, 62cmpt2 6528 . 2 class (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑𝑚 ℕ) ↦ (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓((1st ∘ (𝑓 shift 1)) HomLim (2nd𝑓)))
641, 63wceq 1474 1 wff polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑𝑚 ℕ) ↦ (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ (1st𝑔) / 𝑒(1st𝑒) / 𝑠(𝑠 splitFld ran (𝑥𝑞 ↦ (𝑥 ∘ (2nd𝑔)))) / 𝑓𝑓, ((2nd𝑔) ∘ (2nd𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓((1st ∘ (𝑓 shift 1)) HomLim (2nd𝑓)))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator