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 32716
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 32712 . 2 class /FldExt
2 ve . . . . . . 7 setvar 𝑒
32cv 1540 . . . . . 6 class 𝑒
4 cfield 20357 . . . . . 6 class Field
53, 4wcel 2106 . . . . 5 wff 𝑒 ∈ Field
6 vf . . . . . . 7 setvar 𝑓
76cv 1540 . . . . . 6 class 𝑓
87, 4wcel 2106 . . . . 5 wff 𝑓 ∈ Field
95, 8wa 396 . . . 4 wff (𝑒 ∈ Field ∧ 𝑓 ∈ Field)
10 cbs 17143 . . . . . . . 8 class Base
117, 10cfv 6543 . . . . . . 7 class (Baseβ€˜π‘“)
12 cress 17172 . . . . . . 7 class β†Ύs
133, 11, 12co 7408 . . . . . 6 class (𝑒 β†Ύs (Baseβ€˜π‘“))
147, 13wceq 1541 . . . . 5 wff 𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“))
15 csubrg 20314 . . . . . . 7 class SubRing
163, 15cfv 6543 . . . . . 6 class (SubRingβ€˜π‘’)
1711, 16wcel 2106 . . . . 5 wff (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)
1814, 17wa 396 . . . 4 wff (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’))
199, 18wa 396 . . 3 wff ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))
2019, 2, 6copab 5210 . 2 class {βŸ¨π‘’, π‘“βŸ© ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))}
211, 20wceq 1541 1 wff /FldExt = {βŸ¨π‘’, π‘“βŸ© ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 β†Ύs (Baseβ€˜π‘“)) ∧ (Baseβ€˜π‘“) ∈ (SubRingβ€˜π‘’)))}
Colors of variables: wff setvar class
This definition is referenced by:  relfldext  32720  brfldext  32721  fldextfld1  32723  fldextfld2  32724
  Copyright terms: Public domain W3C validator