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 e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfldext
 |-  /FldExt
1 ve
 |-  e
2 vf
 |-  f
3 1 cv
 |-  e
4 cfield
 |-  Field
5 3 4 wcel
 |-  e e. Field
6 2 cv
 |-  f
7 6 4 wcel
 |-  f e. Field
8 5 7 wa
 |-  ( e e. Field /\ f e. Field )
9 cress
 |-  |`s
10 cbs
 |-  Base
11 6 10 cfv
 |-  ( Base ` f )
12 3 11 9 co
 |-  ( e |`s ( Base ` f ) )
13 6 12 wceq
 |-  f = ( e |`s ( Base ` f ) )
14 csubrg
 |-  SubRing
15 3 14 cfv
 |-  ( SubRing ` e )
16 11 15 wcel
 |-  ( Base ` f ) e. ( SubRing ` e )
17 13 16 wa
 |-  ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) )
18 8 17 wa
 |-  ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) )
19 18 1 2 copab
 |-  { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }
20 0 19 wceq
 |-  /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }