Definition df-algext

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

	Ref	Expression
Assertion	df-algext	|- /AlgExt = { <. e , f >. | ( e /FldExt f /\ ( e IntgRing f ) = ( Base ` e ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		calgext	|- /AlgExt
1		ve	|- e
2		vf	|- f
3	1	cv	|- e
4		cfldext	|- /FldExt
5	2	cv	|- f
6	3 5 4	wbr	|- e /FldExt f
7		cirng	|- IntgRing
8	3 5 7	co	|- ( e IntgRing f )
9		cbs	|- Base
10	3 9	cfv	|- ( Base ` e )
11	8 10	wceq	|- ( e IntgRing f ) = ( Base ` e )
12	6 11	wa	|- ( e /FldExt f /\ ( e IntgRing f ) = ( Base ` e ) )
13	12 1 2	copab	|- { <. e , f >. | ( e /FldExt f /\ ( e IntgRing f ) = ( Base ` e ) ) }
14	0 13	wceq	|- /AlgExt = { <. e , f >. | ( e /FldExt f /\ ( e IntgRing f ) = ( Base ` e ) ) }