Users' Mathboxes 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 32388
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 32384 . 2 class /FldExt
2 ve . . . . . . 7 setvar 𝑒
32cv 1541 . . . . . 6 class 𝑒
4 cfield 20198 . . . . . 6 class Field
53, 4wcel 2107 . . . . 5 wff 𝑒 ∈ Field
6 vf . . . . . . 7 setvar 𝑓
76cv 1541 . . . . . 6 class 𝑓
87, 4wcel 2107 . . . . 5 wff 𝑓 ∈ Field
95, 8wa 397 . . . 4 wff (𝑒 ∈ Field ∧ 𝑓 ∈ Field)
10 cbs 17088 . . . . . . . 8 class Base
117, 10cfv 6497 . . . . . . 7 class (Baseβ€˜π‘“)
12 cress 17117 . . . . . . 7 class β†Ύs
133, 11, 12co 7358 . . . . . 6 class (𝑒 β†Ύs (Baseβ€˜π‘“))
147, 13wceq 1542 . . . . 5 wff 𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“))
15 csubrg 20232 . . . . . . 7 class SubRing
163, 15cfv 6497 . . . . . 6 class (SubRingβ€˜π‘’)
1711, 16wcel 2107 . . . . 5 wff (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)
1814, 17wa 397 . . . 4 wff (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’))
199, 18wa 397 . . 3 wff ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))
2019, 2, 6copab 5168 . 2 class {βŸ¨π‘’, π‘“βŸ© ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))}
211, 20wceq 1542 1 wff /FldExt = {βŸ¨π‘’, π‘“βŸ© ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))}
Colors of variables: wff setvar class
This definition is referenced by:  relfldext  32392  brfldext  32393  fldextfld1  32395  fldextfld2  32396
  Copyright terms: Public domain W3C validator