let L be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; :: thesis: for z being rational_function of L st z is irreducible holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
let z be rational_function of L; :: thesis: ( z is irreducible implies ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) )
assume A1: z is irreducible ; :: thesis: ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
take z ; :: thesis: ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z `1)),(z2 *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
reconsider e = 1_. L as non zero Polynomial of L ;
take e ; :: thesis: ( z = [(e *' (z `1)),(e *' (z `2))] & z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
reconsider f = <*> the carrier of (Polynom-Ring L) as FinSequence of (Polynom-Ring L) ;
thus z = [(z `1),(z `2)] by Th19
.= [(e *' (z `1)),(z `2)] by POLYNOM3:35
.= [(e *' (z `1)),(e *' (z `2))] by POLYNOM3:35 ; :: thesis: ( z is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
thus z is irreducible by A1; :: thesis: ex f being FinSequence of (Polynom-Ring L) st
( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) )
take f ; :: thesis: ( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) )
Product f = 1_ (Polynom-Ring L) by GROUP_4:8;
hence ( e = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) by POLYNOM3:def 10; :: thesis: verum