let L be Field; :: thesis: for p being rational_function of L
for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let p be rational_function of L; :: thesis: for x being Element of L holds
( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
let x be Element of L; :: thesis: ( not eval ((p `2),x) <> 0. L or x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume A1: eval ((p `2),x) <> 0. L ; :: thesis: ( x is_a_common_root_of p `1 ,p `2 or eval ((NF p),x) = eval (p,x) )
assume A2: not x is_a_common_root_of p `1 ,p `2 ; :: thesis: eval ((NF p),x) = eval (p,x)
per cases ( p is zero or not p is zero ) ;
suppose A3: p is zero ; :: thesis: eval ((NF p),x) = eval (p,x)
then A4: p `1 = 0_. L ;
A5: NF p = 0._ L by A3, Def17;
thus eval (p,x) = (0. L) * ((eval ((p `2),x)) ") by A4, POLYNOM4:17
.= 0. L
.= eval ((NF p),x) by A5, Th31 ; :: thesis: verum
end;
suppose not p is zero ; :: thesis: eval ((NF p),x) = eval (p,x)
then consider z1 being rational_function of L, z2 being non zero Polynomial of L such that
A6: ( p = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & NF p = NormRatF z1 & 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 p `1 ,p `2 & f . i = rpoly (1,x) ) ) ) ) by Def17;
A7: p `1 = z2 *' (z1 `1) by A6;
A8: p `2 = z2 *' (z1 `2) by A6;
A9: now :: thesis: not eval (z2,x) = 0. L
assume A10: eval (z2,x) = 0. L ; :: thesis: contradiction
eval ((z2 *' (z1 `1)),x) = (eval (z2,x)) * (eval ((z1 `1),x)) by POLYNOM4:24
.= 0. L by A10 ;
then A11: x is_a_root_of p `1 by A7, POLYNOM5:def 7;
eval ((z2 *' (z1 `2)),x) = (eval (z2,x)) * (eval ((z1 `2),x)) by POLYNOM4:24
.= 0. L by A10 ;
then x is_a_root_of p `2 by A8, POLYNOM5:def 7;
hence contradiction by A2, A11; :: thesis: verum
end;
A12: now :: thesis: not eval ((z1 `2),x) = 0. L
assume eval ((z1 `2),x) = 0. L ; :: thesis: contradiction
then 0. L = (eval (z2,x)) * (eval ((z1 `2),x))
.= eval ((z2 *' (z1 `2)),x) by POLYNOM4:24 ;
hence contradiction by A6, A1; :: thesis: verum
end;
eval (p,x) = (eval ((z2 *' (z1 `1)),x)) * ((eval ((z2 *' (z1 `2)),x)) ") by A6
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * ((eval ((z2 *' (z1 `2)),x)) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval (z2,x)) * (eval ((z1 `2),x))) ") by POLYNOM4:24
.= ((eval (z2,x)) * (eval ((z1 `1),x))) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) ")) by A9, A12, VECTSP_2:11
.= (eval (z2,x)) * ((eval ((z1 `1),x)) * (((eval ((z1 `2),x)) ") * ((eval (z2,x)) "))) by GROUP_1:def 3
.= (eval (z2,x)) * (((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) * ((eval (z2,x)) ")) by GROUP_1:def 3
.= ((eval (z2,x)) * ((eval (z2,x)) ")) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by GROUP_1:def 3
.= (1. L) * ((eval ((z1 `1),x)) * ((eval ((z1 `2),x)) ")) by A9, VECTSP_1:def 10
.= eval (z1,x) ;
hence eval ((NF p),x) = eval (p,x) by A6, A12, Th35; :: thesis: verum
end;
end;