let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being rational_function of L
for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
let p be rational_function of L; :: thesis: for a being non zero Element of L holds
( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
let a be non zero Element of L; :: thesis: ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible )
set ap = [(a * (p `1)),(a * (p `2))];
A1: now :: thesis: ( p is irreducible & [(a * (p `1)),(a * (p `2))] is reducible implies [(a * (p `1)),(a * (p `2))] is irreducible )
assume A2: p is irreducible ; :: thesis: ( [(a * (p `1)),(a * (p `2))] is reducible implies [(a * (p `1)),(a * (p `2))] is irreducible )
assume [(a * (p `1)),(a * (p `2))] is reducible ; :: thesis: [(a * (p `1)),(a * (p `2))] is irreducible
then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots ;
then consider x being Element of L such that
A3: x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 ;
( x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 & x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 ) by A3;
then A4: ( eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L & eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ) by POLYNOM5:def 7;
then eval ((a * (p `1)),x) = 0. L ;
then a * (eval ((p `1),x)) = 0. L by POLYNOM5:30;
then eval ((p `1),x) = 0. L by VECTSP_2:def 1;
then A5: x is_a_root_of p `1 by POLYNOM5:def 7;
eval ((a * (p `2)),x) = 0. L by A4;
then a * (eval ((p `2),x)) = 0. L by POLYNOM5:30;
then eval ((p `2),x) = 0. L by VECTSP_2:def 1;
then x is_a_root_of p `2 by POLYNOM5:def 7;
then x is_a_common_root_of p `1 ,p `2 by A5;
then p `1 ,p `2 have_common_roots ;
hence [(a * (p `1)),(a * (p `2))] is irreducible by A2; :: thesis: verum
end;
now :: thesis: ( [(a * (p `1)),(a * (p `2))] is irreducible & p is reducible implies p is irreducible )
assume A6: [(a * (p `1)),(a * (p `2))] is irreducible ; :: thesis: ( p is reducible implies p is irreducible )
assume p is reducible ; :: thesis: p is irreducible
then p `1 ,p `2 have_common_roots ;
then consider x being Element of L such that
A7: x is_a_common_root_of p `1 ,p `2 ;
( x is_a_root_of p `1 & x is_a_root_of p `2 ) by A7;
then A8: ( eval ((p `1),x) = 0. L & eval ((p `2),x) = 0. L ) by POLYNOM5:def 7;
then a * (eval ((p `1),x)) = 0. L ;
then eval ((a * (p `1)),x) = 0. L by POLYNOM5:30;
then eval (([(a * (p `1)),(a * (p `2))] `1),x) = 0. L ;
then A9: x is_a_root_of [(a * (p `1)),(a * (p `2))] `1 by POLYNOM5:def 7;
a * (eval ((p `2),x)) = 0. L by A8;
then eval ((a * (p `2)),x) = 0. L by POLYNOM5:30;
then eval (([(a * (p `1)),(a * (p `2))] `2),x) = 0. L ;
then x is_a_root_of [(a * (p `1)),(a * (p `2))] `2 by POLYNOM5:def 7;
then x is_a_common_root_of [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 by A9;
then [(a * (p `1)),(a * (p `2))] `1 ,[(a * (p `1)),(a * (p `2))] `2 have_common_roots ;
hence p is irreducible by A6; :: thesis: verum
end;
hence ( [(a * (p `1)),(a * (p `2))] is irreducible iff p is irreducible ) by A1; :: thesis: verum