let L be Field; 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; 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; ( 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
; ( 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
; eval ((NF p),x) = eval (p,x)
per cases
( p is zero or not p is zero )
;
suppose
not
p is
zero
;
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 not eval (z2,x) = 0. Lassume A10:
eval (
z2,
x)
= 0. L
;
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;
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;
verum end; end;