Metamath Proof Explorer

Theorem rtelextdg2lem

Description: Lemma for rtelextdg2 : If an element X is a solution of a quadratic equation, then the degree of its field extension is at most 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. )
rtelextdg2lem.1 
|- Y = ( var1 ` K )
rtelextdg2lem.2 
|- .(+) = ( +g ` P )
rtelextdg2lem.3 
|- .(x) = ( .r ` P )
rtelextdg2lem.4 
|- ./\ = ( .g ` ( mulGrp ` P ) )
rtelextdg2lem.5 
|- U = ( algSc ` P )
rtelextdg2lem.6 
|- G = ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) )
Assertion rtelextdg2lem 
|- ( ph -> ( 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 rtelextdg2lem.1 
 |-  Y = ( var1 ` K )
16 rtelextdg2lem.2 
 |-  .(+) = ( +g ` P )
17 rtelextdg2lem.3 
 |-  .(x) = ( .r ` P )
18 rtelextdg2lem.4 
 |-  ./\ = ( .g ` ( mulGrp ` P ) )
19 rtelextdg2lem.5 
 |-  U = ( algSc ` P )
20 rtelextdg2lem.6 
 |-  G = ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) )
21 eqid 
 |-  ( deg1 ` E ) = ( deg1 ` E )
22 eqid 
 |-  ( E minPoly F ) = ( E minPoly F )
23 fveq2 
 |-  ( p = G -> ( ( E evalSub1 F ) ` p ) = ( ( E evalSub1 F ) ` G ) )
24 23 fveq1d 
 |-  ( p = G -> ( ( ( E evalSub1 F ) ` p ) ` X ) = ( ( ( E evalSub1 F ) ` G ) ` X ) )
25 24 eqeq1d 
 |-  ( p = G -> ( ( ( ( E evalSub1 F ) ` p ) ` X ) = .0. <-> ( ( ( E evalSub1 F ) ` G ) ` X ) = .0. ) )
26 eqid 
 |-  ( Base ` P ) = ( Base ` P )
27 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
28 9 10 27 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
29 28 fldcrngd 
 |-  ( ph -> ( E |`s F ) e. CRing )
30 1 29 eqeltrid 
 |-  ( ph -> K e. CRing )
31 30 crngringd 
 |-  ( ph -> K e. Ring )
32 4 ply1ring 
 |-  ( K e. Ring -> P e. Ring )
33 31 32 syl 
 |-  ( ph -> P e. Ring )
34 33 ringgrpd 
 |-  ( ph -> P e. Grp )
35 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
36 35 26 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
37 35 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
38 33 37 syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
39 2nn0 
 |-  2 e. NN0
40 39 a1i 
 |-  ( ph -> 2 e. NN0 )
41 15 4 26 vr1cl 
 |-  ( K e. Ring -> Y e. ( Base ` P ) )
42 31 41 syl 
 |-  ( ph -> Y e. ( Base ` P ) )
43 36 18 38 40 42 mulgnn0cld 
 |-  ( ph -> ( 2 ./\ Y ) e. ( Base ` P ) )
44 9 fldcrngd 
 |-  ( ph -> E e. CRing )
45 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
46 10 45 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
47 4 1 19 26 44 46 12 ressasclcl 
 |-  ( ph -> ( U ` A ) e. ( Base ` P ) )
48 26 17 33 47 42 ringcld 
 |-  ( ph -> ( ( U ` A ) .(x) Y ) e. ( Base ` P ) )
49 4 1 19 26 44 46 13 ressasclcl 
 |-  ( ph -> ( U ` B ) e. ( Base ` P ) )
50 26 16 34 48 49 grpcld 
 |-  ( ph -> ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) e. ( Base ` P ) )
51 26 16 34 43 50 grpcld 
 |-  ( ph -> ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) e. ( Base ` P ) )
52 20 51 eqeltrid 
 |-  ( ph -> G e. ( Base ` P ) )
53 20 fveq2i 
 |-  ( coe1 ` G ) = ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) )
54 53 fveq1i 
 |-  ( ( coe1 ` G ) ` 2 ) = ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 2 )
55 eqid 
 |-  ( +g ` K ) = ( +g ` K )
56 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( 2 ./\ Y ) e. ( Base ` P ) /\ ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) e. ( Base ` P ) ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 2 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) ) )
57 31 43 50 40 56 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 2 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) ) )
58 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
59 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
60 4 15 18 31 40 58 59 coe1mon 
 |-  ( ph -> ( coe1 ` ( 2 ./\ Y ) ) = ( i e. NN0 |-> if ( i = 2 , ( 1r ` K ) , ( 0g ` K ) ) ) )
61 simpr 
 |-  ( ( ph /\ i = 2 ) -> i = 2 )
62 61 iftrued 
 |-  ( ( ph /\ i = 2 ) -> if ( i = 2 , ( 1r ` K ) , ( 0g ` K ) ) = ( 1r ` K ) )
63 fvexd 
 |-  ( ph -> ( 1r ` K ) e. _V )
64 60 62 40 63 fvmptd 
 |-  ( ph -> ( ( coe1 ` ( 2 ./\ Y ) ) ` 2 ) = ( 1r ` K ) )
65 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( ( U ` A ) .(x) Y ) e. ( Base ` P ) /\ ( U ` B ) e. ( Base ` P ) ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 2 ) ) )
66 31 48 49 40 65 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 2 ) ) )
67 5 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ V )
68 1 5 ressbas2 
 |-  ( F C_ V -> F = ( Base ` K ) )
69 10 67 68 3syl 
 |-  ( ph -> F = ( Base ` K ) )
70 12 69 eleqtrd 
 |-  ( ph -> A e. ( Base ` K ) )
71 eqid 
 |-  ( Base ` K ) = ( Base ` K )
72 eqid 
 |-  ( .r ` K ) = ( .r ` K )
73 4 26 71 19 17 72 coe1sclmulfv 
 |-  ( ( K e. Ring /\ ( A e. ( Base ` K ) /\ Y e. ( Base ` P ) ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 2 ) ) )
74 31 70 42 40 73 syl121anc 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 2 ) ) )
75 4 15 31 58 59 coe1vr1 
 |-  ( ph -> ( coe1 ` Y ) = ( i e. NN0 |-> if ( i = 1 , ( 1r ` K ) , ( 0g ` K ) ) ) )
76 1ne2 
 |-  1 =/= 2
77 76 nesymi 
 |-  -. 2 = 1
78 eqeq1 
 |-  ( i = 2 -> ( i = 1 <-> 2 = 1 ) )
79 77 78 mtbiri 
 |-  ( i = 2 -> -. i = 1 )
80 79 adantl 
 |-  ( ( ph /\ i = 2 ) -> -. i = 1 )
81 80 iffalsed 
 |-  ( ( ph /\ i = 2 ) -> if ( i = 1 , ( 1r ` K ) , ( 0g ` K ) ) = ( 0g ` K ) )
82 fvexd 
 |-  ( ph -> ( 0g ` K ) e. _V )
83 75 81 40 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` Y ) ` 2 ) = ( 0g ` K ) )
84 83 oveq2d 
 |-  ( ph -> ( A ( .r ` K ) ( ( coe1 ` Y ) ` 2 ) ) = ( A ( .r ` K ) ( 0g ` K ) ) )
85 71 72 58 31 70 ringrzd 
 |-  ( ph -> ( A ( .r ` K ) ( 0g ` K ) ) = ( 0g ` K ) )
86 74 84 85 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) = ( 0g ` K ) )
87 13 69 eleqtrd 
 |-  ( ph -> B e. ( Base ` K ) )
88 4 19 71 58 coe1scl 
 |-  ( ( K e. Ring /\ B e. ( Base ` K ) ) -> ( coe1 ` ( U ` B ) ) = ( i e. NN0 |-> if ( i = 0 , B , ( 0g ` K ) ) ) )
89 31 87 88 syl2anc 
 |-  ( ph -> ( coe1 ` ( U ` B ) ) = ( i e. NN0 |-> if ( i = 0 , B , ( 0g ` K ) ) ) )
90 0ne2 
 |-  0 =/= 2
91 90 neii 
 |-  -. 0 = 2
92 eqeq1 
 |-  ( i = 0 -> ( i = 2 <-> 0 = 2 ) )
93 91 92 mtbiri 
 |-  ( i = 0 -> -. i = 2 )
94 93 61 nsyl3 
 |-  ( ( ph /\ i = 2 ) -> -. i = 0 )
95 94 iffalsed 
 |-  ( ( ph /\ i = 2 ) -> if ( i = 0 , B , ( 0g ` K ) ) = ( 0g ` K ) )
96 89 95 40 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` ( U ` B ) ) ` 2 ) = ( 0g ` K ) )
97 86 96 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 2 ) ) = ( ( 0g ` K ) ( +g ` K ) ( 0g ` K ) ) )
98 31 ringgrpd 
 |-  ( ph -> K e. Grp )
99 71 58 grpidcl 
 |-  ( K e. Grp -> ( 0g ` K ) e. ( Base ` K ) )
100 98 99 syl 
 |-  ( ph -> ( 0g ` K ) e. ( Base ` K ) )
101 71 55 58 98 100 grpridd 
 |-  ( ph -> ( ( 0g ` K ) ( +g ` K ) ( 0g ` K ) ) = ( 0g ` K ) )
102 66 97 101 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) = ( 0g ` K ) )
103 64 102 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 2 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 2 ) ) = ( ( 1r ` K ) ( +g ` K ) ( 0g ` K ) ) )
104 71 59 ringidcl 
 |-  ( K e. Ring -> ( 1r ` K ) e. ( Base ` K ) )
105 31 104 syl 
 |-  ( ph -> ( 1r ` K ) e. ( Base ` K ) )
106 71 55 58 98 105 grpridd 
 |-  ( ph -> ( ( 1r ` K ) ( +g ` K ) ( 0g ` K ) ) = ( 1r ` K ) )
107 44 crngringd 
 |-  ( ph -> E e. Ring )
108 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
109 108 subrg1cl 
 |-  ( F e. ( SubRing ` E ) -> ( 1r ` E ) e. F )
110 46 109 syl 
 |-  ( ph -> ( 1r ` E ) e. F )
111 10 67 syl 
 |-  ( ph -> F C_ V )
112 1 5 108 ress1r 
 |-  ( ( E e. Ring /\ ( 1r ` E ) e. F /\ F C_ V ) -> ( 1r ` E ) = ( 1r ` K ) )
113 107 110 111 112 syl3anc 
 |-  ( ph -> ( 1r ` E ) = ( 1r ` K ) )
114 106 113 eqtr4d 
 |-  ( ph -> ( ( 1r ` K ) ( +g ` K ) ( 0g ` K ) ) = ( 1r ` E ) )
115 57 103 114 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 2 ) = ( 1r ` E ) )
116 54 115 eqtrid 
 |-  ( ph -> ( ( coe1 ` G ) ` 2 ) = ( 1r ` E ) )
117 9 flddrngd 
 |-  ( ph -> E e. DivRing )
118 drngnzr 
 |-  ( E e. DivRing -> E e. NzRing )
119 108 3 nzrnz 
 |-  ( E e. NzRing -> ( 1r ` E ) =/= .0. )
120 117 118 119 3syl 
 |-  ( ph -> ( 1r ` E ) =/= .0. )
121 116 120 eqnetrd 
 |-  ( ph -> ( ( coe1 ` G ) ` 2 ) =/= .0. )
122 fveq2 
 |-  ( G = ( 0g ` P ) -> ( coe1 ` G ) = ( coe1 ` ( 0g ` P ) ) )
123 122 fveq1d 
 |-  ( G = ( 0g ` P ) -> ( ( coe1 ` G ) ` 2 ) = ( ( coe1 ` ( 0g ` P ) ) ` 2 ) )
124 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
125 4 124 58 31 40 coe1zfv 
 |-  ( ph -> ( ( coe1 ` ( 0g ` P ) ) ` 2 ) = ( 0g ` K ) )
126 107 ringgrpd 
 |-  ( ph -> E e. Grp )
127 126 grpmndd 
 |-  ( ph -> E e. Mnd )
128 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
129 46 128 syl 
 |-  ( ph -> F e. ( SubGrp ` E ) )
130 3 subg0cl 
 |-  ( F e. ( SubGrp ` E ) -> .0. e. F )
131 129 130 syl 
 |-  ( ph -> .0. e. F )
132 1 5 3 ress0g 
 |-  ( ( E e. Mnd /\ .0. e. F /\ F C_ V ) -> .0. = ( 0g ` K ) )
133 127 131 111 132 syl3anc 
 |-  ( ph -> .0. = ( 0g ` K ) )
134 125 133 eqtr4d 
 |-  ( ph -> ( ( coe1 ` ( 0g ` P ) ) ` 2 ) = .0. )
135 123 134 sylan9eqr 
 |-  ( ( ph /\ G = ( 0g ` P ) ) -> ( ( coe1 ` G ) ` 2 ) = .0. )
136 121 135 mteqand 
 |-  ( ph -> G =/= ( 0g ` P ) )
137 20 fveq2i 
 |-  ( ( deg1 ` K ) ` G ) = ( ( deg1 ` K ) ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) )
138 eqid 
 |-  ( deg1 ` K ) = ( deg1 ` K )
139 2re 
 |-  2 e. RR
140 139 rexri 
 |-  2 e. RR*
141 140 a1i 
 |-  ( ph -> 2 e. RR* )
142 138 4 26 deg1xrcl 
 |-  ( ( ( U ` A ) .(x) Y ) e. ( Base ` P ) -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) e. RR* )
143 48 142 syl 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) e. RR* )
144 1xr 
 |-  1 e. RR*
145 144 a1i 
 |-  ( ph -> 1 e. RR* )
146 138 4 71 26 17 19 deg1mul3le 
 |-  ( ( K e. Ring /\ A e. ( Base ` K ) /\ Y e. ( Base ` P ) ) -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) <_ ( ( deg1 ` K ) ` Y ) )
147 31 70 42 146 syl3anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) <_ ( ( deg1 ` K ) ` Y ) )
148 1 28 eqeltrid 
 |-  ( ph -> K e. Field )
149 148 flddrngd 
 |-  ( ph -> K e. DivRing )
150 drngnzr 
 |-  ( K e. DivRing -> K e. NzRing )
151 149 150 syl 
 |-  ( ph -> K e. NzRing )
152 138 4 15 151 deg1vr 
 |-  ( ph -> ( ( deg1 ` K ) ` Y ) = 1 )
153 147 152 breqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) <_ 1 )
154 1lt2 
 |-  1 < 2
155 154 a1i 
 |-  ( ph -> 1 < 2 )
156 143 145 141 153 155 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( U ` A ) .(x) Y ) ) < 2 )
157 138 4 26 deg1xrcl 
 |-  ( ( U ` B ) e. ( Base ` P ) -> ( ( deg1 ` K ) ` ( U ` B ) ) e. RR* )
158 49 157 syl 
 |-  ( ph -> ( ( deg1 ` K ) ` ( U ` B ) ) e. RR* )
159 0xr 
 |-  0 e. RR*
160 159 a1i 
 |-  ( ph -> 0 e. RR* )
161 138 4 71 19 deg1sclle 
 |-  ( ( K e. Ring /\ B e. ( Base ` K ) ) -> ( ( deg1 ` K ) ` ( U ` B ) ) <_ 0 )
162 31 87 161 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( U ` B ) ) <_ 0 )
163 2pos 
 |-  0 < 2
164 163 a1i 
 |-  ( ph -> 0 < 2 )
165 158 160 141 162 164 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( U ` B ) ) < 2 )
166 4 138 31 26 16 48 49 141 156 165 deg1addlt 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) < 2 )
167 138 4 15 35 18 deg1pw 
 |-  ( ( K e. NzRing /\ 2 e. NN0 ) -> ( ( deg1 ` K ) ` ( 2 ./\ Y ) ) = 2 )
168 151 40 167 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( 2 ./\ Y ) ) = 2 )
169 166 168 breqtrrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) < ( ( deg1 ` K ) ` ( 2 ./\ Y ) ) )
170 4 138 31 26 16 43 50 169 deg1add 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) = ( ( deg1 ` K ) ` ( 2 ./\ Y ) ) )
171 170 168 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) = 2 )
172 137 171 eqtrid 
 |-  ( ph -> ( ( deg1 ` K ) ` G ) = 2 )
173 172 fveq2d 
 |-  ( ph -> ( ( coe1 ` G ) ` ( ( deg1 ` K ) ` G ) ) = ( ( coe1 ` G ) ` 2 ) )
174 173 116 113 3eqtrd 
 |-  ( ph -> ( ( coe1 ` G ) ` ( ( deg1 ` K ) ` G ) ) = ( 1r ` K ) )
175 eqid 
 |-  ( Monic1p ` K ) = ( Monic1p ` K )
176 4 26 124 138 175 59 ismon1p 
 |-  ( G e. ( Monic1p ` K ) <-> ( G e. ( Base ` P ) /\ G =/= ( 0g ` P ) /\ ( ( coe1 ` G ) ` ( ( deg1 ` K ) ` G ) ) = ( 1r ` K ) ) )
177 52 136 174 176 syl3anbrc 
 |-  ( ph -> G e. ( Monic1p ` K ) )
178 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
179 eqid 
 |-  ( eval1 ` E ) = ( eval1 ` E )
180 178 5 4 1 26 179 44 46 ressply1evl 
 |-  ( ph -> ( E evalSub1 F ) = ( ( eval1 ` E ) |` ( Base ` P ) ) )
181 180 fveq1d 
 |-  ( ph -> ( ( E evalSub1 F ) ` G ) = ( ( ( eval1 ` E ) |` ( Base ` P ) ) ` G ) )
182 52 fvresd 
 |-  ( ph -> ( ( ( eval1 ` E ) |` ( Base ` P ) ) ` G ) = ( ( eval1 ` E ) ` G ) )
183 181 182 eqtrd 
 |-  ( ph -> ( ( E evalSub1 F ) ` G ) = ( ( eval1 ` E ) ` G ) )
184 183 fveq1d 
 |-  ( ph -> ( ( ( E evalSub1 F ) ` G ) ` X ) = ( ( ( eval1 ` E ) ` G ) ` X ) )
185 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
186 eqid 
 |-  ( Base ` ( Poly1 ` E ) ) = ( Base ` ( Poly1 ` E ) )
187 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
188 eqid 
 |-  ( ( coe1 ` G ) ` 2 ) = ( ( coe1 ` G ) ` 2 )
189 eqid 
 |-  ( ( coe1 ` G ) ` 1 ) = ( ( coe1 ` G ) ` 1 )
190 eqid 
 |-  ( ( coe1 ` G ) ` 0 ) = ( ( coe1 ` G ) ` 0 )
191 eqid 
 |-  ( PwSer1 ` K ) = ( PwSer1 ` K )
192 eqid 
 |-  ( Base ` ( PwSer1 ` K ) ) = ( Base ` ( PwSer1 ` K ) )
193 185 1 4 26 46 191 192 186 ressply1bas2 
 |-  ( ph -> ( Base ` P ) = ( ( Base ` ( PwSer1 ` K ) ) i^i ( Base ` ( Poly1 ` E ) ) ) )
194 52 193 eleqtrd 
 |-  ( ph -> G e. ( ( Base ` ( PwSer1 ` K ) ) i^i ( Base ` ( Poly1 ` E ) ) ) )
195 194 elin2d 
 |-  ( ph -> G e. ( Base ` ( Poly1 ` E ) ) )
196 1 21 4 26 52 46 ressdeg1 
 |-  ( ph -> ( ( deg1 ` E ) ` G ) = ( ( deg1 ` K ) ` G ) )
197 196 172 eqtrd 
 |-  ( ph -> ( ( deg1 ` E ) ` G ) = 2 )
198 185 179 5 186 6 7 8 187 21 188 189 190 44 195 197 11 evl1deg2 
 |-  ( ph -> ( ( ( eval1 ` E ) ` G ) ` X ) = ( ( ( ( coe1 ` G ) ` 2 ) .x. ( 2 .^ X ) ) .+ ( ( ( ( coe1 ` G ) ` 1 ) .x. X ) .+ ( ( coe1 ` G ) ` 0 ) ) ) )
199 116 oveq1d 
 |-  ( ph -> ( ( ( coe1 ` G ) ` 2 ) .x. ( 2 .^ X ) ) = ( ( 1r ` E ) .x. ( 2 .^ X ) ) )
200 eqid 
 |-  ( mulGrp ` E ) = ( mulGrp ` E )
201 200 5 mgpbas 
 |-  V = ( Base ` ( mulGrp ` E ) )
202 200 ringmgp 
 |-  ( E e. Ring -> ( mulGrp ` E ) e. Mnd )
203 107 202 syl 
 |-  ( ph -> ( mulGrp ` E ) e. Mnd )
204 201 8 203 40 11 mulgnn0cld 
 |-  ( ph -> ( 2 .^ X ) e. V )
205 5 6 108 107 204 ringlidmd 
 |-  ( ph -> ( ( 1r ` E ) .x. ( 2 .^ X ) ) = ( 2 .^ X ) )
206 199 205 eqtrd 
 |-  ( ph -> ( ( ( coe1 ` G ) ` 2 ) .x. ( 2 .^ X ) ) = ( 2 .^ X ) )
207 53 fveq1i 
 |-  ( ( coe1 ` G ) ` 1 ) = ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 1 )
208 1nn0 
 |-  1 e. NN0
209 208 a1i 
 |-  ( ph -> 1 e. NN0 )
210 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( 2 ./\ Y ) e. ( Base ` P ) /\ ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) e. ( Base ` P ) ) /\ 1 e. NN0 ) -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 1 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) ) )
211 31 43 50 209 210 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 1 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) ) )
212 76 neii 
 |-  -. 1 = 2
213 eqeq1 
 |-  ( i = 1 -> ( i = 2 <-> 1 = 2 ) )
214 213 notbid 
 |-  ( i = 1 -> ( -. i = 2 <-> -. 1 = 2 ) )
215 214 adantl 
 |-  ( ( ph /\ i = 1 ) -> ( -. i = 2 <-> -. 1 = 2 ) )
216 212 215 mpbiri 
 |-  ( ( ph /\ i = 1 ) -> -. i = 2 )
217 216 iffalsed 
 |-  ( ( ph /\ i = 1 ) -> if ( i = 2 , ( 1r ` K ) , ( 0g ` K ) ) = ( 0g ` K ) )
218 60 217 209 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` ( 2 ./\ Y ) ) ` 1 ) = ( 0g ` K ) )
219 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( ( U ` A ) .(x) Y ) e. ( Base ` P ) /\ ( U ` B ) e. ( Base ` P ) ) /\ 1 e. NN0 ) -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 1 ) ) )
220 31 48 49 209 219 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 1 ) ) )
221 4 26 71 19 17 72 coe1sclmulfv 
 |-  ( ( K e. Ring /\ ( A e. ( Base ` K ) /\ Y e. ( Base ` P ) ) /\ 1 e. NN0 ) -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 1 ) ) )
222 31 70 42 209 221 syl121anc 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 1 ) ) )
223 simpr 
 |-  ( ( ph /\ i = 1 ) -> i = 1 )
224 223 iftrued 
 |-  ( ( ph /\ i = 1 ) -> if ( i = 1 , ( 1r ` K ) , ( 0g ` K ) ) = ( 1r ` K ) )
225 75 224 209 63 fvmptd 
 |-  ( ph -> ( ( coe1 ` Y ) ` 1 ) = ( 1r ` K ) )
226 225 oveq2d 
 |-  ( ph -> ( A ( .r ` K ) ( ( coe1 ` Y ) ` 1 ) ) = ( A ( .r ` K ) ( 1r ` K ) ) )
227 71 72 59 31 70 ringridmd 
 |-  ( ph -> ( A ( .r ` K ) ( 1r ` K ) ) = A )
228 222 226 227 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) = A )
229 0ne1 
 |-  0 =/= 1
230 229 nesymi 
 |-  -. 1 = 0
231 eqeq1 
 |-  ( i = 1 -> ( i = 0 <-> 1 = 0 ) )
232 230 231 mtbiri 
 |-  ( i = 1 -> -. i = 0 )
233 232 adantl 
 |-  ( ( ph /\ i = 1 ) -> -. i = 0 )
234 233 iffalsed 
 |-  ( ( ph /\ i = 1 ) -> if ( i = 0 , B , ( 0g ` K ) ) = ( 0g ` K ) )
235 89 234 209 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` ( U ` B ) ) ` 1 ) = ( 0g ` K ) )
236 228 235 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 1 ) ) = ( A ( +g ` K ) ( 0g ` K ) ) )
237 71 55 58 98 70 grpridd 
 |-  ( ph -> ( A ( +g ` K ) ( 0g ` K ) ) = A )
238 220 236 237 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) = A )
239 218 238 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 1 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 1 ) ) = ( ( 0g ` K ) ( +g ` K ) A ) )
240 71 55 58 98 70 grplidd 
 |-  ( ph -> ( ( 0g ` K ) ( +g ` K ) A ) = A )
241 211 239 240 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 1 ) = A )
242 207 241 eqtrid 
 |-  ( ph -> ( ( coe1 ` G ) ` 1 ) = A )
243 242 oveq1d 
 |-  ( ph -> ( ( ( coe1 ` G ) ` 1 ) .x. X ) = ( A .x. X ) )
244 53 fveq1i 
 |-  ( ( coe1 ` G ) ` 0 ) = ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 0 )
245 0nn0 
 |-  0 e. NN0
246 245 a1i 
 |-  ( ph -> 0 e. NN0 )
247 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( 2 ./\ Y ) e. ( Base ` P ) /\ ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) e. ( Base ` P ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 0 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) ) )
248 31 43 50 246 247 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 0 ) = ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) ) )
249 93 adantl 
 |-  ( ( ph /\ i = 0 ) -> -. i = 2 )
250 249 iffalsed 
 |-  ( ( ph /\ i = 0 ) -> if ( i = 2 , ( 1r ` K ) , ( 0g ` K ) ) = ( 0g ` K ) )
251 60 250 246 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` ( 2 ./\ Y ) ) ` 0 ) = ( 0g ` K ) )
252 4 26 16 55 coe1addfv 
 |-  ( ( ( K e. Ring /\ ( ( U ` A ) .(x) Y ) e. ( Base ` P ) /\ ( U ` B ) e. ( Base ` P ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 0 ) ) )
253 31 48 49 246 252 syl31anc 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) = ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 0 ) ) )
254 4 26 71 19 17 72 coe1sclmulfv 
 |-  ( ( K e. Ring /\ ( A e. ( Base ` K ) /\ Y e. ( Base ` P ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 0 ) ) )
255 31 70 42 246 254 syl121anc 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) = ( A ( .r ` K ) ( ( coe1 ` Y ) ` 0 ) ) )
256 229 neii 
 |-  -. 0 = 1
257 eqeq1 
 |-  ( i = 0 -> ( i = 1 <-> 0 = 1 ) )
258 256 257 mtbiri 
 |-  ( i = 0 -> -. i = 1 )
259 258 adantl 
 |-  ( ( ph /\ i = 0 ) -> -. i = 1 )
260 259 iffalsed 
 |-  ( ( ph /\ i = 0 ) -> if ( i = 1 , ( 1r ` K ) , ( 0g ` K ) ) = ( 0g ` K ) )
261 75 260 246 82 fvmptd 
 |-  ( ph -> ( ( coe1 ` Y ) ` 0 ) = ( 0g ` K ) )
262 261 oveq2d 
 |-  ( ph -> ( A ( .r ` K ) ( ( coe1 ` Y ) ` 0 ) ) = ( A ( .r ` K ) ( 0g ` K ) ) )
263 255 262 85 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) = ( 0g ` K ) )
264 4 19 71 ply1sclid 
 |-  ( ( K e. Ring /\ B e. ( Base ` K ) ) -> B = ( ( coe1 ` ( U ` B ) ) ` 0 ) )
265 31 87 264 syl2anc 
 |-  ( ph -> B = ( ( coe1 ` ( U ` B ) ) ` 0 ) )
266 265 eqcomd 
 |-  ( ph -> ( ( coe1 ` ( U ` B ) ) ` 0 ) = B )
267 263 266 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( ( U ` A ) .(x) Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( U ` B ) ) ` 0 ) ) = ( ( 0g ` K ) ( +g ` K ) B ) )
268 71 55 58 98 87 grplidd 
 |-  ( ph -> ( ( 0g ` K ) ( +g ` K ) B ) = B )
269 253 267 268 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) = B )
270 251 269 oveq12d 
 |-  ( ph -> ( ( ( coe1 ` ( 2 ./\ Y ) ) ` 0 ) ( +g ` K ) ( ( coe1 ` ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ` 0 ) ) = ( ( 0g ` K ) ( +g ` K ) B ) )
271 248 270 268 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( 2 ./\ Y ) .(+) ( ( ( U ` A ) .(x) Y ) .(+) ( U ` B ) ) ) ) ` 0 ) = B )
272 244 271 eqtrid 
 |-  ( ph -> ( ( coe1 ` G ) ` 0 ) = B )
273 243 272 oveq12d 
 |-  ( ph -> ( ( ( ( coe1 ` G ) ` 1 ) .x. X ) .+ ( ( coe1 ` G ) ` 0 ) ) = ( ( A .x. X ) .+ B ) )
274 206 273 oveq12d 
 |-  ( ph -> ( ( ( ( coe1 ` G ) ` 2 ) .x. ( 2 .^ X ) ) .+ ( ( ( ( coe1 ` G ) ` 1 ) .x. X ) .+ ( ( coe1 ` G ) ` 0 ) ) ) = ( ( 2 .^ X ) .+ ( ( A .x. X ) .+ B ) ) )
275 274 14 eqtrd 
 |-  ( ph -> ( ( ( ( coe1 ` G ) ` 2 ) .x. ( 2 .^ X ) ) .+ ( ( ( ( coe1 ` G ) ` 1 ) .x. X ) .+ ( ( coe1 ` G ) ` 0 ) ) ) = .0. )
276 184 198 275 3eqtrd 
 |-  ( ph -> ( ( ( E evalSub1 F ) ` G ) ` X ) = .0. )
277 25 177 276 rspcedvdw 
 |-  ( ph -> E. p e. ( Monic1p ` K ) ( ( ( E evalSub1 F ) ` p ) ` X ) = .0. )
278 178 1 5 3 44 46 elirng 
 |-  ( ph -> ( X e. ( E IntgRing F ) <-> ( X e. V /\ E. p e. ( Monic1p ` K ) ( ( ( E evalSub1 F ) ` p ) ` X ) = .0. ) ) )
279 11 277 278 mpbir2and 
 |-  ( ph -> X e. ( E IntgRing F ) )
280 1 2 21 22 9 10 279 algextdeg 
 |-  ( ph -> ( L [:] K ) = ( ( deg1 ` E ) ` ( ( E minPoly F ) ` X ) ) )
281 1 fveq2i 
 |-  ( Poly1 ` K ) = ( Poly1 ` ( E |`s F ) )
282 4 281 eqtri 
 |-  P = ( Poly1 ` ( E |`s F ) )
283 eqid 
 |-  { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` X ) = .0. } = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` X ) = .0. }
284 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
285 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
286 178 282 5 9 10 11 3 283 284 285 22 minplycl 
 |-  ( ph -> ( ( E minPoly F ) ` X ) e. ( Base ` P ) )
287 1 21 4 26 286 46 ressdeg1 
 |-  ( ph -> ( ( deg1 ` E ) ` ( ( E minPoly F ) ` X ) ) = ( ( deg1 ` K ) ` ( ( E minPoly F ) ` X ) ) )
288 280 287 eqtrd 
 |-  ( ph -> ( L [:] K ) = ( ( deg1 ` K ) ` ( ( E minPoly F ) ` X ) ) )
289 1 fveq2i 
 |-  ( deg1 ` K ) = ( deg1 ` ( E |`s F ) )
290 178 282 5 9 10 11 3 22 289 124 26 276 52 136 minplymindeg 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( E minPoly F ) ` X ) ) <_ ( ( deg1 ` K ) ` G ) )
291 288 290 eqbrtrd 
 |-  ( ph -> ( L [:] K ) <_ ( ( deg1 ` K ) ` G ) )
292 291 172 breqtrd 
 |-  ( ph -> ( L [:] K ) <_ 2 )