This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-fldext

Description: Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion df-fldext ⊢ /FldExt = e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfldext class /FldExt
1 ve setvar e
2 vf setvar f
3 1 cv setvar e
4 cfield class Field
5 3 4 wcel wff e ∈ Field
6 2 cv setvar f
7 6 4 wcel wff f ∈ Field
8 5 7 wa wff e ∈ Field ∧ f ∈ Field
9 cress class ↾ 𝑠
10 cbs class Base
11 6 10 cfv class Base f
12 3 11 9 co class e ↾ 𝑠 Base f
13 6 12 wceq wff f = e ↾ 𝑠 Base f
14 csubrg class SubRing
15 3 14 cfv class SubRing ⁡ e
16 11 15 wcel wff Base f ∈ SubRing ⁡ e
17 13 16 wa wff f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
18 8 17 wa wff e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
19 18 1 2 copab class e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e
20 0 19 wceq wff /FldExt = e f | e ∈ Field ∧ f ∈ Field ∧ f = e ↾ 𝑠 Base f ∧ Base f ∈ SubRing ⁡ e