let F be non 2 -characteristic Field; :: thesis: for p being quadratic Element of the carrier of (Polynom-Ring F) holds
( p is reducible iff DC p is square )
let p be quadratic Element of the carrier of (Polynom-Ring F); :: thesis: ( p is reducible iff DC p is square )
consider a being non zero Element of F, b, c being Element of F such that
H0: p = <%c,b,a%> by qua5;

Z: now :: thesis: ( DC p is square implies p is reducible )

assume DC p is square ; :: thesis: p is reducible
then consider w being Element of F such that
A: w ^2 = DC p by O_RING_1:def 2;
A1: DC p = (b ^2) - ((4 '*' a) * c) by H0, defDC;
set r1 = ((- b) + w) * ((2 '*' a) ");
set r2 = ((- b) - w) * ((2 '*' a) ");
set q1 = X- (((- b) + w) * ((2 '*' a) "));
set q2 = X- (((- b) - w) * ((2 '*' a) "));
reconsider qq1 = X- (((- b) + w) * ((2 '*' a) ")), qq2 = a * (X- (((- b) - w) * ((2 '*' a) "))), p1 = p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
p = a * ((X- (((- b) + w) * ((2 '*' a) "))) *' (X- (((- b) - w) * ((2 '*' a) ")))) by H0, A, A1, lemred
.= (X- (((- b) + w) * ((2 '*' a) "))) *' (a * (X- (((- b) - w) * ((2 '*' a) ")))) by RING_4:10
.= qq1 * qq2 by POLYNOM3:def 10 ;
then B: qq1 divides p1 by GCD_1:def 1;
C: deg (X- (((- b) + w) * ((2 '*' a) "))) = 1 by HURWITZ:27;
deg p = 2 by defquadr;
hence p is reducible by C, B, RING_4:40, RING_4:def 3; :: thesis: verum

end;

now :: thesis: ( p is reducible implies DC p is square )

assume Y: p is reducible ; :: thesis: DC p is square
( p <> 0_. F & not p is unital ) ;
then consider q being Element of the carrier of (Polynom-Ring F) such that
A: ( q divides p & 1 <= deg q & deg q < deg p ) by Y, RING_4:41;
reconsider pp = p, qq = q as Polynomial of F ;
consider rr being Polynomial of F such that
B: pp = qq *' rr by A, RING_4:1;
reconsider degq = deg q as Element of NAT by A, INT_1:3;
E: deg p = 2 by defquadr;
degq < 1 + 1 by A, defquadr;
then E0: ( degq >= 1 & degq <= 1 ) by A, NAT_1:13;
then E0a: degq = 1 by XXREAL_0:1;
consider x1, c1 being Element of F such that
E1: ( x1 <> 0. F & q = x1 * (rpoly (1,c1)) ) by E0, XXREAL_0:1, HURWITZ:28;
E2: qq <> 0_. F by A, HURWITZ:20;
rr <> 0_. F by B;
then (deg qq) + (deg rr) = 2 by B, E, E2, HURWITZ:23;
then consider x2, c2 being Element of F such that
E3: ( x2 <> 0. F & rr = x2 * (rpoly (1,c2)) ) by E0a, HURWITZ:28;
reconsider x = x1 * x2 as non zero Element of F by E3, E1, VECTSP_2:def 1, STRUCT_0:def 12;
qq *' rr = x2 * ((rpoly (1,c2)) *' (x1 * (rpoly (1,c1)))) by E1, E3, RATFUNC1:6
.= x2 * (x1 * ((rpoly (1,c2)) *' (rpoly (1,c1)))) by RATFUNC1:6
.= (x2 * x1) * ((rpoly (1,c2)) *' (rpoly (1,c1))) by RING_4:11
.= x * ((rpoly (1,c2)) *' (rpoly (1,c1))) by GROUP_1:def 12
.= x * <%(c1 * c2),(- (c1 + c2)),(1. F)%> by lemred3z
.= <%(x * (c1 * c2)),(x * (- (c1 + c2))),(x * (1. F))%> by qua6 ;
then DC p = ((x * (- (c1 + c2))) ^2) - ((4 '*' x) * (x * (c1 * c2))) by B, defDC
.= ((x * ((- c1) + (- c2))) ^2) - ((4 '*' x) * (x * (c1 * c2))) by RLVECT_1:31
.= (((x * (- c1)) + (x * (- c2))) ^2) - ((4 '*' x) * (x * (c1 * c2))) by VECTSP_1:def 2
.= ((((x * (- c1)) ^2) + ((2 '*' (x * (- c1))) * (x * (- c2)))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by REALALG2:7
.= ((((x * (- c1)) ^2) + (2 '*' ((x * (- c1)) * (x * (- c2))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by REALALG2:5
.= ((((x * (- c1)) ^2) + (2 '*' (x * ((- c1) * (x * (- c2)))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by GROUP_1:def 3
.= ((((x * (- c1)) ^2) + (2 '*' (x * ((x * (- c2)) * (- c1))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by GROUP_1:def 12
.= ((((x * (- c1)) ^2) + (2 '*' (x * (x * ((- c2) * (- c1)))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by GROUP_1:def 3
.= ((((x * (- c1)) ^2) + (2 '*' (x * (x * (c2 * c1))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by VECTSP_1:10
.= ((((x * (- c1)) ^2) + (2 '*' (x * (x * (c1 * c2))))) + ((x * (- c2)) ^2)) - ((4 '*' x) * (x * (c1 * c2))) by GROUP_1:def 12
.= ((((x * (- c1)) ^2) + (2 '*' (x * (x * (c1 * c2))))) + (- ((4 '*' x) * (x * (c1 * c2))))) + ((x * (- c2)) ^2) by RLVECT_1:def 3
.= (((x * (- c1)) ^2) + ((2 '*' (x * (x * (c1 * c2)))) + (- ((4 '*' x) * (x * (c1 * c2)))))) + ((x * (- c2)) ^2) by RLVECT_1:def 3
.= (((x * (- c1)) ^2) + ((2 '*' (x * (x * (c1 * c2)))) + (- (4 '*' (x * (x * (c1 * c2))))))) + ((x * (- c2)) ^2) by REALALG2:5
.= (((x * (- c1)) ^2) + ((2 '*' (x * (x * (c1 * c2)))) + ((- 4) '*' (x * (x * (c1 * c2)))))) + ((x * (- c2)) ^2) by RING_3:63
.= (((x * (- c1)) ^2) + ((2 + (- 4)) '*' (x * (x * (c1 * c2))))) + ((x * (- c2)) ^2) by RING_3:62
.= (((x * (- c1)) ^2) + ((- 2) '*' (x * (x * (c1 * c2))))) + ((x * (- c2)) ^2)
.= (((x * (- c1)) ^2) + (- (2 '*' (x * (x * (c1 * c2)))))) + ((x * (- c2)) ^2) by RING_3:63
.= (((x * (- c1)) ^2) + (- (2 '*' (x * (x * ((- c1) * (- c2))))))) + ((x * (- c2)) ^2) by VECTSP_1:10
.= (((x * (- c1)) ^2) + (- (2 '*' (x * (x * ((- c2) * (- c1))))))) + ((x * (- c2)) ^2) by GROUP_1:def 12
.= (((x * (- c1)) ^2) - (2 '*' (x * ((x * (- c2)) * (- c1))))) + ((x * (- c2)) ^2) by GROUP_1:def 3
.= (((x * (- c1)) ^2) - (2 '*' (x * ((- c1) * (x * (- c2)))))) + ((x * (- c2)) ^2) by GROUP_1:def 12
.= (((x * (- c1)) ^2) - (2 '*' ((x * (- c1)) * (x * (- c2))))) + ((x * (- c2)) ^2) by GROUP_1:def 3
.= (((x * (- c1)) ^2) - ((2 '*' (x * (- c1))) * (x * (- c2)))) + ((x * (- c2)) ^2) by REALALG2:5
.= ((x * (- c1)) - (x * (- c2))) ^2 by REALALG2:8 ;
hence DC p is square ; :: thesis: verum

end;

hence ( p is reducible iff DC p is square ) by Z; :: thesis: verum