Theorem brfldext

Description: The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	brfldext	|- ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( e = E /\ f = F ) -> e = E )
2	1	eleq1d	|- ( ( e = E /\ f = F ) -> ( e e. Field <-> E e. Field ) )
3		simpr	|- ( ( e = E /\ f = F ) -> f = F )
4	3	eleq1d	|- ( ( e = E /\ f = F ) -> ( f e. Field <-> F e. Field ) )
5	2 4	anbi12d	|- ( ( e = E /\ f = F ) -> ( ( e e. Field /\ f e. Field ) <-> ( E e. Field /\ F e. Field ) ) )
6	3	fveq2d	|- ( ( e = E /\ f = F ) -> ( Base ` f ) = ( Base ` F ) )
7	1 6	oveq12d	|- ( ( e = E /\ f = F ) -> ( e |`s ( Base ` f ) ) = ( E |`s ( Base ` F ) ) )
8	3 7	eqeq12d	|- ( ( e = E /\ f = F ) -> ( f = ( e |`s ( Base ` f ) ) <-> F = ( E |`s ( Base ` F ) ) ) )
9	1	fveq2d	|- ( ( e = E /\ f = F ) -> ( SubRing ` e ) = ( SubRing ` E ) )
10	6 9	eleq12d	|- ( ( e = E /\ f = F ) -> ( ( Base ` f ) e. ( SubRing ` e ) <-> ( Base ` F ) e. ( SubRing ` E ) ) )
11	8 10	anbi12d	|- ( ( e = E /\ f = F ) -> ( ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
12	5 11	anbi12d	|- ( ( e = E /\ f = F ) -> ( ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) <-> ( ( E e. Field /\ F e. Field ) /\ ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) )
13		df-fldext	|- /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }
14	12 13	brabga	|- ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( ( E e. Field /\ F e. Field ) /\ ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) )
15	14	bianabs	|- ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )