Metamath Proof Explorer

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 /\ A. x e. ( Base ` e ) E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` 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 vx 
 |-  x
8 cbs 
 |-  Base
9 3 8 cfv 
 |-  ( Base ` e )
10 vp 
 |-  p
11 cpl1 
 |-  Poly1
12 5 11 cfv 
 |-  ( Poly1 ` f )
13 ce1 
 |-  eval1
14 5 13 cfv 
 |-  ( eval1 ` f )
15 10 cv 
 |-  p
16 15 14 cfv 
 |-  ( ( eval1 ` f ) ` p )
17 7 cv 
 |-  x
18 17 16 cfv 
 |-  ( ( ( eval1 ` f ) ` p ) ` x )
19 c0g 
 |-  0g
20 3 19 cfv 
 |-  ( 0g ` e )
21 18 20 wceq 
 |-  ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e )
22 21 10 12 wrex 
 |-  E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e )
23 22 7 9 wral 
 |-  A. x e. ( Base ` e ) E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e )
24 6 23 wa 
 |-  ( e /FldExt f /\ A. x e. ( Base ` e ) E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e ) )
25 24 1 2 copab 
 |-  { <. e , f >. | ( e /FldExt f /\ A. x e. ( Base ` e ) E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e ) ) }
26 0 25 wceq 
 |-  /AlgExt = { <. e , f >. | ( e /FldExt f /\ A. x e. ( Base ` e ) E. p e. ( Poly1 ` f ) ( ( ( eval1 ` f ) ` p ) ` x ) = ( 0g ` e ) ) }