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 \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\}$

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 \in Field$
6	2	cv	$setvar f$
7	6 4	wcel	$wff f \in Field$
8	5 7	wa	$wff (e \in Field \land f \in 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} \in SubRing (e)$
17	13 16	wa	$wff (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e))$
18	8 17	wa	$wff ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))$
19	18 1 2	copab	$class \{⟨e, f⟩ \| ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\}$
20	0 19	wceq	$wff /_{FldExt} = \{⟨e, f⟩ \| ((e \in Field \land f \in Field) \land (f = e ↾_{𝑠} {Base}_{f} \land {Base}_{f} \in SubRing (e)))\}$

Metamath Proof Explorer