This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) }