Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fldext Structured version   Visualization version   GIF version

Definition df-fldext 31089
 Description: Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
Assertion
Ref Expression
df-fldext /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Distinct variable group:   𝑒,𝑓

Detailed syntax breakdown of Definition df-fldext
StepHypRef Expression
1 cfldext 31085 . 2 class /FldExt
2 ve . . . . . . 7 setvar 𝑒
32cv 1537 . . . . . 6 class 𝑒
4 cfield 19494 . . . . . 6 class Field
53, 4wcel 2114 . . . . 5 wff 𝑒 ∈ Field
6 vf . . . . . . 7 setvar 𝑓
76cv 1537 . . . . . 6 class 𝑓
87, 4wcel 2114 . . . . 5 wff 𝑓 ∈ Field
95, 8wa 399 . . . 4 wff (𝑒 ∈ Field ∧ 𝑓 ∈ Field)
10 cbs 16474 . . . . . . . 8 class Base
117, 10cfv 6334 . . . . . . 7 class (Base‘𝑓)
12 cress 16475 . . . . . . 7 class s
133, 11, 12co 7140 . . . . . 6 class (𝑒s (Base‘𝑓))
147, 13wceq 1538 . . . . 5 wff 𝑓 = (𝑒s (Base‘𝑓))
15 csubrg 19522 . . . . . . 7 class SubRing
163, 15cfv 6334 . . . . . 6 class (SubRing‘𝑒)
1711, 16wcel 2114 . . . . 5 wff (Base‘𝑓) ∈ (SubRing‘𝑒)
1814, 17wa 399 . . . 4 wff (𝑓 = (𝑒s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒))
199, 18wa 399 . . 3 wff ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))
2019, 2, 6copab 5104 . 2 class {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
211, 20wceq 1538 1 wff /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
 Colors of variables: wff setvar class This definition is referenced by:  relfldext  31093  brfldext  31094  fldextfld1  31096  fldextfld2  31097
 Copyright terms: Public domain W3C validator