Metamath Proof Explorer

Theorem algextdeg

Description: The degree of an algebraic field extension (noted [ L : K ] ) is the degree of the minimal polynomial M ( A ) , whereas L is the field generated by K and the algebraic element A . (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses algextdeg.k 
|- K = ( E |`s F )
algextdeg.l 
|- L = ( E |`s ( E fldGen ( F u. { A } ) ) )
algextdeg.d 
|- D = ( deg1 ` E )
algextdeg.m 
|- M = ( E minPoly F )
algextdeg.f 
|- ( ph -> E e. Field )
algextdeg.e 
|- ( ph -> F e. ( SubDRing ` E ) )
algextdeg.a 
|- ( ph -> A e. ( E IntgRing F ) )
Assertion algextdeg 
|- ( ph -> ( L [:] K ) = ( D ` ( M ` A ) ) )

Proof

Step Hyp Ref Expression
1 algextdeg.k 
 |-  K = ( E |`s F )
2 algextdeg.l 
 |-  L = ( E |`s ( E fldGen ( F u. { A } ) ) )
3 algextdeg.d 
 |-  D = ( deg1 ` E )
4 algextdeg.m 
 |-  M = ( E minPoly F )
5 algextdeg.f 
 |-  ( ph -> E e. Field )
6 algextdeg.e 
 |-  ( ph -> F e. ( SubDRing ` E ) )
7 algextdeg.a 
 |-  ( ph -> A e. ( E IntgRing F ) )
8 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
9 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
10 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
11 fveq2 
 |-  ( q = p -> ( ( E evalSub1 F ) ` q ) = ( ( E evalSub1 F ) ` p ) )
12 11 fveq1d 
 |-  ( q = p -> ( ( ( E evalSub1 F ) ` q ) ` A ) = ( ( ( E evalSub1 F ) ` p ) ` A ) )
13 12 cbvmptv 
 |-  ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) = ( p e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` p ) ` A ) )
14 eceq1 
 |-  ( y = x -> [ y ] ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) = [ x ] ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) )
15 14 cbvmptv 
 |-  ( y e. ( Base ` ( Poly1 ` K ) ) |-> [ y ] ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) = ( x e. ( Base ` ( Poly1 ` K ) ) |-> [ x ] ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) )
16 eqid 
 |-  ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) = ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } )
17 eqid 
 |-  ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) = ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) )
18 imaeq2 
 |-  ( r = p -> ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " r ) = ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " p ) )
19 18 unieqd 
 |-  ( r = p -> U. ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " r ) = U. ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " p ) )
20 19 cbvmptv 
 |-  ( r e. ( Base ` ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) ) |-> U. ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " r ) ) = ( p e. ( Base ` ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) ) |-> U. ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " p ) )
21 eqid 
 |-  ( rem1p ` K ) = ( rem1p ` K )
22 oveq1 
 |-  ( q = p -> ( q ( rem1p ` K ) ( M ` A ) ) = ( p ( rem1p ` K ) ( M ` A ) ) )
23 22 cbvmptv 
 |-  ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( q ( rem1p ` K ) ( M ` A ) ) ) = ( p e. ( Base ` ( Poly1 ` K ) ) |-> ( p ( rem1p ` K ) ( M ` A ) ) )
24 1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23 algextdeglem6 
 |-  ( ph -> ( dim ` ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) ) = ( dim ` ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( q ( rem1p ` K ) ( M ` A ) ) ) "s ( Poly1 ` K ) ) ) )
25 1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 algextdeglem4 
 |-  ( ph -> ( dim ` ( ( Poly1 ` K ) /s ( ( Poly1 ` K ) ~QG ( `' ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( ( ( E evalSub1 F ) ` q ) ` A ) ) " { ( 0g ` L ) } ) ) ) ) = ( L [:] K ) )
26 eqid 
 |-  ( `' ( deg1 ` K ) " ( -oo [,) ( D ` ( M ` A ) ) ) ) = ( `' ( deg1 ` K ) " ( -oo [,) ( D ` ( M ` A ) ) ) )
27 1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23 26 algextdeglem8 
 |-  ( ph -> ( dim ` ( ( q e. ( Base ` ( Poly1 ` K ) ) |-> ( q ( rem1p ` K ) ( M ` A ) ) ) "s ( Poly1 ` K ) ) ) = ( D ` ( M ` A ) ) )
28 24 25 27 3eqtr3d 
 |-  ( ph -> ( L [:] K ) = ( D ` ( M ` A ) ) )