Metamath Proof Explorer

Theorem rtelextdg2

Description: If an element X is a solution of a quadratic equation, then it is either in the base field, or the degree of its field extension is exactly 2. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses rtelextdg2.1 
|- K = ( E |`s F )
rtelextdg2.2 
|- L = ( E |`s ( E fldGen ( F u. { X } ) ) )
rtelextdg2.3 
|- .0. = ( 0g ` E )
rtelextdg2.4 
|- P = ( Poly1 ` K )
rtelextdg2.5 
|- V = ( Base ` E )
rtelextdg2.6 
|- .x. = ( .r ` E )
rtelextdg2.7 
|- .+ = ( +g ` E )
rtelextdg2.8 
|- .^ = ( .g ` ( mulGrp ` E ) )
rtelextdg2.9 
|- ( ph -> E e. Field )
rtelextdg2.10 
|- ( ph -> F e. ( SubDRing ` E ) )
rtelextdg2.11 
|- ( ph -> X e. V )
rtelextdg2.12 
|- ( ph -> A e. F )
rtelextdg2.13 
|- ( ph -> B e. F )
rtelextdg2.14 
|- ( ph -> ( ( 2 .^ X ) .+ ( ( A .x. X ) .+ B ) ) = .0. )
Assertion rtelextdg2 
|- ( ph -> ( X e. F \/ ( L [:] K ) = 2 ) )

Proof

Step Hyp Ref Expression
1 rtelextdg2.1 
 |-  K = ( E |`s F )
2 rtelextdg2.2 
 |-  L = ( E |`s ( E fldGen ( F u. { X } ) ) )
3 rtelextdg2.3 
 |-  .0. = ( 0g ` E )
4 rtelextdg2.4 
 |-  P = ( Poly1 ` K )
5 rtelextdg2.5 
 |-  V = ( Base ` E )
6 rtelextdg2.6 
 |-  .x. = ( .r ` E )
7 rtelextdg2.7 
 |-  .+ = ( +g ` E )
8 rtelextdg2.8 
 |-  .^ = ( .g ` ( mulGrp ` E ) )
9 rtelextdg2.9 
 |-  ( ph -> E e. Field )
10 rtelextdg2.10 
 |-  ( ph -> F e. ( SubDRing ` E ) )
11 rtelextdg2.11 
 |-  ( ph -> X e. V )
12 rtelextdg2.12 
 |-  ( ph -> A e. F )
13 rtelextdg2.13 
 |-  ( ph -> B e. F )
14 rtelextdg2.14 
 |-  ( ph -> ( ( 2 .^ X ) .+ ( ( A .x. X ) .+ B ) ) = .0. )
15 9 flddrngd 
 |-  ( ph -> E e. DivRing )
16 5 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ V )
17 10 16 syl 
 |-  ( ph -> F C_ V )
18 11 snssd 
 |-  ( ph -> { X } C_ V )
19 17 18 unssd 
 |-  ( ph -> ( F u. { X } ) C_ V )
20 5 15 19 fldgenssid 
 |-  ( ph -> ( F u. { X } ) C_ ( E fldGen ( F u. { X } ) ) )
21 ssun2 
 |-  { X } C_ ( F u. { X } )
22 snidg 
 |-  ( X e. V -> X e. { X } )
23 11 22 syl 
 |-  ( ph -> X e. { X } )
24 21 23 sselid 
 |-  ( ph -> X e. ( F u. { X } ) )
25 20 24 sseldd 
 |-  ( ph -> X e. ( E fldGen ( F u. { X } ) ) )
26 25 adantr 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> X e. ( E fldGen ( F u. { X } ) ) )
27 5 1 2 9 10 18 fldgenfldext 
 |-  ( ph -> L /FldExt K )
28 extdg1id 
 |-  ( ( L /FldExt K /\ ( L [:] K ) = 1 ) -> L = K )
29 27 28 sylan 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> L = K )
30 29 fveq2d 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> ( Base ` L ) = ( Base ` K ) )
31 5 15 19 fldgenssv 
 |-  ( ph -> ( E fldGen ( F u. { X } ) ) C_ V )
32 2 5 ressbas2 
 |-  ( ( E fldGen ( F u. { X } ) ) C_ V -> ( E fldGen ( F u. { X } ) ) = ( Base ` L ) )
33 31 32 syl 
 |-  ( ph -> ( E fldGen ( F u. { X } ) ) = ( Base ` L ) )
34 33 adantr 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> ( E fldGen ( F u. { X } ) ) = ( Base ` L ) )
35 1 5 ressbas2 
 |-  ( F C_ V -> F = ( Base ` K ) )
36 17 35 syl 
 |-  ( ph -> F = ( Base ` K ) )
37 36 adantr 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> F = ( Base ` K ) )
38 30 34 37 3eqtr4d 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> ( E fldGen ( F u. { X } ) ) = F )
39 26 38 eleqtrd 
 |-  ( ( ph /\ ( L [:] K ) = 1 ) -> X e. F )
40 simpr 
 |-  ( ( ph /\ ( L [:] K ) = 2 ) -> ( L [:] K ) = 2 )
41 1zzd 
 |-  ( ph -> 1 e. ZZ )
42 2z 
 |-  2 e. ZZ
43 42 a1i 
 |-  ( ph -> 2 e. ZZ )
44 extdgcl 
 |-  ( L /FldExt K -> ( L [:] K ) e. NN0* )
45 27 44 syl 
 |-  ( ph -> ( L [:] K ) e. NN0* )
46 2nn0 
 |-  2 e. NN0
47 46 a1i 
 |-  ( ph -> 2 e. NN0 )
48 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
49 eqid 
 |-  ( +g ` P ) = ( +g ` P )
50 eqid 
 |-  ( .r ` P ) = ( .r ` P )
51 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
52 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
53 eqid 
 |-  ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` K ) ) ( +g ` P ) ( ( ( ( algSc ` P ) ` A ) ( .r ` P ) ( var1 ` K ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` K ) ) ( +g ` P ) ( ( ( ( algSc ` P ) ` A ) ( .r ` P ) ( var1 ` K ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 48 49 50 51 52 53 rtelextdg2lem 
 |-  ( ph -> ( L [:] K ) <_ 2 )
55 xnn0lenn0nn0 
 |-  ( ( ( L [:] K ) e. NN0* /\ 2 e. NN0 /\ ( L [:] K ) <_ 2 ) -> ( L [:] K ) e. NN0 )
56 45 47 54 55 syl3anc 
 |-  ( ph -> ( L [:] K ) e. NN0 )
57 56 nn0zd 
 |-  ( ph -> ( L [:] K ) e. ZZ )
58 extdggt0 
 |-  ( L /FldExt K -> 0 < ( L [:] K ) )
59 27 58 syl 
 |-  ( ph -> 0 < ( L [:] K ) )
60 zgt0ge1 
 |-  ( ( L [:] K ) e. ZZ -> ( 0 < ( L [:] K ) <-> 1 <_ ( L [:] K ) ) )
61 60 biimpa 
 |-  ( ( ( L [:] K ) e. ZZ /\ 0 < ( L [:] K ) ) -> 1 <_ ( L [:] K ) )
62 57 59 61 syl2anc 
 |-  ( ph -> 1 <_ ( L [:] K ) )
63 41 43 57 62 54 elfzd 
 |-  ( ph -> ( L [:] K ) e. ( 1 ... 2 ) )
64 fz12pr 
 |-  ( 1 ... 2 ) = { 1 , 2 }
65 63 64 eleqtrdi 
 |-  ( ph -> ( L [:] K ) e. { 1 , 2 } )
66 elpri 
 |-  ( ( L [:] K ) e. { 1 , 2 } -> ( ( L [:] K ) = 1 \/ ( L [:] K ) = 2 ) )
67 65 66 syl 
 |-  ( ph -> ( ( L [:] K ) = 1 \/ ( L [:] K ) = 2 ) )
68 39 40 67 orim12da 
 |-  ( ph -> ( X e. F \/ ( L [:] K ) = 2 ) )