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 ( Base ` 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		cbs	|- Base
9	5 8	cfv	|- ( Base ` f )
10	3 9 7	co	|- ( e IntgRing ( Base ` f ) )
11	3 8	cfv	|- ( Base ` e )
12	10 11	wceq	|- ( e IntgRing ( Base ` f ) ) = ( Base ` e )
13	6 12	wa	|- ( e /FldExt f /\ ( e IntgRing ( Base ` f ) ) = ( Base ` e ) )
14	13 1 2	copab	|- { <. e , f >. | ( e /FldExt f /\ ( e IntgRing ( Base ` f ) ) = ( Base ` e ) ) }
15	0 14	wceq	|- /AlgExt = { <. e , f >. | ( e /FldExt f /\ ( e IntgRing ( Base ` f ) ) = ( Base ` e ) ) }