let L be domRing; :: thesis: for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)

let p, q be Polynomial of L; :: thesis: Roots (p *' q) = (Roots p) \/ (Roots q)

let p, q be Polynomial of L; :: thesis: Roots (p *' q) = (Roots p) \/ (Roots q)

now :: thesis: for x being object holds

( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies x in Roots (p *' q) ) )

hence
Roots (p *' q) = (Roots p) \/ (Roots q)
by TARSKI:2; :: thesis: verum( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies x in Roots (p *' q) ) )

let x be object ; :: thesis: ( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies b_{1} in Roots (p *' q) ) )

_{1} in Roots (p *' q)

end;hereby :: thesis: ( x in (Roots p) \/ (Roots q) implies b_{1} in Roots (p *' q) )

assume A3:
x in (Roots p) \/ (Roots q)
; :: thesis: bassume A1:
x in Roots (p *' q)
; :: thesis: x in (Roots p) \/ (Roots q)

then reconsider a = x as Element of L ;

a is_a_root_of p *' q by A1, POLYNOM5:def 10;

then eval ((p *' q),a) = 0. L ;

then A2: (eval (p,a)) * (eval (q,a)) = 0. L by POLYNOM4:24;

end;then reconsider a = x as Element of L ;

a is_a_root_of p *' q by A1, POLYNOM5:def 10;

then eval ((p *' q),a) = 0. L ;

then A2: (eval (p,a)) * (eval (q,a)) = 0. L by POLYNOM4:24;

per cases
( eval (p,a) = 0. L or eval (q,a) = 0. L )
by A2, VECTSP_2:def 1;

end;

suppose
eval (p,a) = 0. L
; :: thesis: x in (Roots p) \/ (Roots q)

then
a is_a_root_of p
;

then a in Roots p by POLYNOM5:def 10;

hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis: verum

end;then a in Roots p by POLYNOM5:def 10;

hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis: verum

suppose
eval (q,a) = 0. L
; :: thesis: x in (Roots p) \/ (Roots q)

then
a is_a_root_of q
;

then a in Roots q by POLYNOM5:def 10;

hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis: verum

end;then a in Roots q by POLYNOM5:def 10;

hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis: verum

per cases
( x in Roots p or x in Roots q )
by A3, XBOOLE_0:def 3;

end;

suppose A4:
x in Roots p
; :: thesis: b_{1} in Roots (p *' q)

then reconsider a = x as Element of L ;

a is_a_root_of p by A4, POLYNOM5:def 10;

then eval (p,a) = 0. L ;

then (eval (p,a)) * (eval (q,a)) = 0. L ;

then eval ((p *' q),a) = 0. L by POLYNOM4:24;

then a is_a_root_of p *' q ;

hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

end;a is_a_root_of p by A4, POLYNOM5:def 10;

then eval (p,a) = 0. L ;

then (eval (p,a)) * (eval (q,a)) = 0. L ;

then eval ((p *' q),a) = 0. L by POLYNOM4:24;

then a is_a_root_of p *' q ;

hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

suppose A5:
x in Roots q
; :: thesis: b_{1} in Roots (p *' q)

then reconsider a = x as Element of L ;

a is_a_root_of q by A5, POLYNOM5:def 10;

then eval (q,a) = 0. L ;

then (eval (p,a)) * (eval (q,a)) = 0. L ;

then eval ((p *' q),a) = 0. L by POLYNOM4:24;

then a is_a_root_of p *' q ;

hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

end;a is_a_root_of q by A5, POLYNOM5:def 10;

then eval (q,a) = 0. L ;

then (eval (p,a)) * (eval (q,a)) = 0. L ;

then eval ((p *' q),a) = 0. L by POLYNOM4:24;

then a is_a_root_of p *' q ;

hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum