Definition df-fldext 34153

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

Step	Hyp	Ref	Expression
1		cfldext 34150	. 2 class /FldExt
2		ve	. . . . . . 7 setvar 𝑒
3	2	cv 1569	. . . . . 6 class 𝑒
4		cfield 20895	. . . . . 6 class Field
5	3, 4	wcel 2145	. . . . 5 wff 𝑒 ∈ Field
6		vf	. . . . . . 7 setvar 𝑓
7	6	cv 1569	. . . . . 6 class 𝑓
8	7, 4	wcel 2145	. . . . 5 wff 𝑓 ∈ Field
9	5, 8	wa 401	. . . 4 wff (𝑒 ∈ Field ∧ 𝑓 ∈ Field)
10		cbs 17305	. . . . . . . 8 class Base
11	7, 10	cfv 6537	. . . . . . 7 class (Base‘𝑓)
12		cress 17326	. . . . . . 7 class ↾s
13	3, 11, 12	co 7416	. . . . . 6 class (𝑒 ↾s (Base‘𝑓))
14	7, 13	wceq 1570	. . . . 5 wff 𝑓 = (𝑒 ↾s (Base‘𝑓))
15		csubrg 20735	. . . . . . 7 class SubRing
16	3, 15	cfv 6537	. . . . . 6 class (SubRing‘𝑒)
17	11, 16	wcel 2145	. . . . 5 wff (Base‘𝑓) ∈ (SubRing‘𝑒)
18	14, 17	wa 401	. . . 4 wff (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒))
19	9, 18	wa 401	. . 3 wff ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))
20	19, 2, 6	copab 5171	. 2 class {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
21	1, 20	wceq 1570	1 wff /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}

This definition is used by:  relfldext  34156  brfldext  34157  fldextfld1  34159  fldextfld2  34160