let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))
set E = FAdj (F,{(sqrt (DC p))});
K:
F is Subring of FAdj (F,{(sqrt (DC p))})
by FIELD_4:def 1;
then H:
not FAdj (F,{(sqrt (DC p))}) is 2 -characteristic
;
then
for a being non zero Element of (FAdj (F,{(sqrt (DC p))}))
for b, c, w being Element of (FAdj (F,{(sqrt (DC p))})) st w ^2 = (b ^2) - ((4 '*' a) * c) holds
for r1, r2 being Element of (FAdj (F,{(sqrt (DC p))})) st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))
by lemred;
consider a being non zero Element of F, b, c being Element of F such that
A:
p = <%c,b,a%>
by qua5;
I:
( @ (c,(FAdj (F,{(sqrt (DC p))}))) = c & @ (b,(FAdj (F,{(sqrt (DC p))}))) = b & @ (a,(FAdj (F,{(sqrt (DC p))}))) = a )
by FIELD_7:def 4;
then B:
p = <%(@ (c,(FAdj (F,{(sqrt (DC p))})))),(@ (b,(FAdj (F,{(sqrt (DC p))})))),(@ (a,(FAdj (F,{(sqrt (DC p))}))))%>
by A, eval2;
C:
Root1 p = ((- (@ (b,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) ")
by E, B, Z2;
D:
Root2 p = ((- (@ (b,(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) ")
by E, B, Z2;
J: (RootDC p) ^2 =
(RootDC p) * (RootDC p)
by O_RING_1:def 1
.=
DC p
by Z1
.=
(b ^2) - ((4 '*' a) * c)
by A, defDC
;
J1: b ^2 =
b * b
by O_RING_1:def 1
.=
(@ (b,(FAdj (F,{(sqrt (DC p))})))) * (@ (b,(FAdj (F,{(sqrt (DC p))}))))
by I, K, FIELD_6:16
.=
(@ (b,(FAdj (F,{(sqrt (DC p))})))) ^2
by O_RING_1:def 1
;
(4 '*' a) * c =
4 '*' (a * c)
by REALALG2:5
.=
4 '*' ((@ (a,(FAdj (F,{(sqrt (DC p))})))) * (@ (c,(FAdj (F,{(sqrt (DC p))})))))
by Z3, I, K, FIELD_6:16
.=
(4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))}))))
by REALALG2:5
;
then
- ((4 '*' a) * c) = - ((4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))})))))
by K, FIELD_6:17;
then F:
(b ^2) - ((4 '*' a) * c) = ((@ (b,(FAdj (F,{(sqrt (DC p))})))) ^2) - ((4 '*' (@ (a,(FAdj (F,{(sqrt (DC p))}))))) * (@ (c,(FAdj (F,{(sqrt (DC p))})))))
by K, J1, FIELD_6:15;
len p = 3
by A, qua3;
then G:
(len p) -' 1 = 3 - 1
by XREAL_0:def 2;
@ (a,(FAdj (F,{(sqrt (DC p))}))) =
a
by FIELD_7:def 4
.=
p . 2
by A, qua1
.=
LC p
by G, RATFUNC1:def 6
.=
@ ((LC p),(FAdj (F,{(sqrt (DC p))})))
by FIELD_7:def 4
;
hence
p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((X- (Root1 p)) *' (X- (Root2 p)))
by F, J, H, E, D, C, B, lemred; verum