ring_5.miz
begin
reserve n for
Nat;
registration
cluster non
trivial non
prime for
Nat;
existence by
NAT_2:def 1,
INT_2: 29;
end
T8: for L be non
empty
ZeroStr, p be
Polynomial of L holds (
deg p) is
Element of
NAT iff p
<> (
0_. L)
proof
let L be non
empty
ZeroStr;
let p be
Polynomial of L;
now
assume p
<> (
0_. L);
then (
len p)
<>
0 by
POLYNOM4: 5;
then ((
len p)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
len p)
>= 1 by
NAT_1: 13;
then ((
len p)
- 1) is
Element of
NAT by
INT_1: 3;
hence (
deg p) is
Element of
NAT by
HURWITZ:def 2;
end;
hence thesis by
HURWITZ: 20;
end;
prl4: for R be
Ring, a be
Element of R holds (a
|^ 2)
= (a
* a)
proof
let R be
Ring, a be
Element of R;
(a
|^ (1
+ 1))
= ((a
|^ 1)
* (a
|^ 1)) by
BINOM: 10
.= (a
* (a
|^ 1)) by
BINOM: 8
.= (a
* a) by
BINOM: 8;
hence thesis;
end;
theorem ::
RING_5:1
XX: for n be
even
Nat, x be
Element of
F_Real holds (x
|^ n)
>= (
0.
F_Real )
proof
let n be
even
Nat, x be
Element of
F_Real ;
defpred
P[
Nat] means (x
|^ (2
* $1))
>= (
0.
F_Real );
(x
|^
0 )
= (
1_
F_Real ) by
BINOM: 8;
then
IA:
P[
0 ];
XX1: for x be
Element of
F_Real holds (x
|^ 2)
>= (
0.
F_Real )
proof
let x be
Element of
F_Real ;
per cases ;
suppose x
>=
0 ;
then (x
* x)
>= (
0
*
0 );
hence thesis by
prl4;
end;
suppose x
<=
0 ;
then (x
* x)
>= (
0
*
0 );
hence thesis by
prl4;
end;
end;
IS:
now
let k be
Nat;
assume
AS:
P[k];
H0: (x
|^ (2
* (k
+ 1)))
= (x
|^ ((2
* k)
+ 2))
.= ((x
|^ (2
* k))
* (x
|^ 2)) by
BINOM: 10;
(x
|^ 2)
>= (
0.
F_Real ) by
XX1;
hence
P[(k
+ 1)] by
H0,
AS;
end;
I: for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
ex k be
Nat st n
= (2
* k) by
ABIAN:def 2;
hence thesis by
I;
end;
theorem ::
RING_5:2
prl3: for R be
Ring, a be
Element of R holds (2
'*' a)
= (a
+ a)
proof
let R be
Ring, a be
Element of R;
thus (2
'*' a)
= ((1
+ 1)
'*' a)
.= ((1
'*' a)
+ (1
'*' a)) by
RING_3: 62
.= (a
+ (1
'*' a)) by
RING_3: 60
.= (a
+ a) by
RING_3: 60;
end;
theorem ::
RING_5:3
for R be
Ring, a be
Element of R holds (a
|^ 2)
= (a
* a) by
prl4;
registration
let F be
Field;
let a be
Element of F;
reduce (a
/ (
1. F)) to a;
reducibility
proof
thus a
= (a
* ((
1. F)
" ))
.= (a
/ (
1. F)) by
ALGSTR_0:def 43;
end;
end
registration
cluster (
Z/ 2) -> non
trivial
almost_left_invertible;
coherence by
INT_2: 28;
end
registration
let n be non
trivial non
prime
Nat;
cluster (
Z/ n) -> non
domRing-like;
coherence
proof
set R = (
Z/ n);
not (n
=
0 or ... or n
= 1) by
NAT_2:def 1;
then n
> 1;
then
consider u be
Nat such that
A: u
divides n & u
<> 1 & u
<> n by
INT_2:def 4;
consider v be
Integer such that
B: (u
* v)
= n by
A,
INT_1:def 3;
v
>=
0 by
B;
then v
in
NAT by
INT_1: 3;
then
reconsider v as
Nat;
A1: u
> 1 & u
< n
proof
not (u
=
0 or ... or u
= 1) by
A,
INT_2: 3;
hence u
> 1;
u
<= n by
A,
INT_2: 27;
hence u
< n by
A,
XXREAL_0: 1;
end;
then
reconsider u as
positive
Nat;
B1: v
> 1 & v
< n
proof
reconsider m = n as
Complex;
B2:
now
assume v
= n;
then ((u
* m)
/ m)
= 1 by
B,
XCMPLX_1: 60;
hence contradiction by
A,
XCMPLX_1: 89;
end;
not (v
=
0 or ... or v
= 1) by
A,
B;
hence v
> 1;
v
<= n by
B,
INT_1:def 3,
INT_2: 27;
hence v
< n by
B2,
XXREAL_0: 1;
end;
then
reconsider v as
positive
Nat;
V: (
Char R)
= n by
RING_3:def 6;
then
C: (
0. R)
= ((u
* v)
'*' (
1. R)) by
B,
RING_3:def 5
.= ((u
'*' (
1. R))
* (v
'*' (
1. R))) by
RING_3: 67;
D: (u
'*' (
1. R))
<> (
0. R) by
V,
A1,
RING_3:def 5;
(v
'*' (
1. R))
<> (
0. R) by
V,
B1,
RING_3:def 5;
hence thesis by
C,
D,
VECTSP_2:def 1;
end;
end
registration
cluster (
Z/ 6) -> non
degenerated;
coherence
proof
6 is non
trivial by
NAT_2:def 1;
hence thesis;
end;
end
begin
registration
let R be non
degenerated
Ring;
cluster ->
non-zero for non
zero
Polynomial of R;
coherence ;
cluster
monic -> non
zero for
Polynomial of R;
coherence ;
end
registration
let R be non
degenerated
Ring;
let p be non
zero
Polynomial of R;
cluster (
deg p) ->
natural;
coherence ;
end
registration
let R be
Ring;
let p be
zero
Polynomial of R;
let q be
Polynomial of R;
cluster (p
*' q) ->
zero;
coherence
proof
p
= (
0_. R) by
UPROOTS:def 5;
hence thesis by
POLYNOM4: 2;
end;
cluster (q
*' p) ->
zero;
coherence
proof
p
= (
0_. R) by
UPROOTS:def 5;
hence thesis by
POLYNOM3: 34;
end;
end
registration
let R be
Ring;
let p be
zero
Polynomial of R;
let q be
Polynomial of R;
reduce (p
+ q) to q;
reducibility
proof
p
= (
0_. R) by
UPROOTS:def 5;
hence thesis by
POLYNOM3: 28;
end;
reduce (q
+ p) to q;
reducibility ;
end
registration
let R be
Ring;
let p be
Polynomial of R;
reduce (p
*' (
0_. R)) to (
0_. R);
reducibility by
POLYNOM3: 34;
reduce (p
*' (
1_. R)) to p;
reducibility by
POLYNOM3: 35;
reduce ((
0_. R)
*' p) to (
0_. R);
reducibility by
POLYNOM4: 2;
reduce ((
1_. R)
*' p) to p;
reducibility by
RING_4: 12;
end
registration
let R be
Ring;
let p be
Polynomial of R;
reduce ((
1. R)
* p) to p;
reducibility by
POLYNOM5: 27;
end
Th28: for L be non
empty
ZeroStr, a be
Element of L holds ((a
| L)
.
0 )
= a
proof
let L be non
empty
ZeroStr, a be
Element of L;
0
in
NAT ;
then
0
in (
dom (
0_. L)) by
FUNCT_2:def 1;
hence a
= ((a
| L)
.
0 ) by
FUNCT_7: 31;
end;
Th25a: for R be
domRing, p be
Polynomial of R holds for a be non
zero
Element of R holds (
len (a
* p))
= (
len p)
proof
let L be
domRing, p be
Polynomial of L;
let v be non
zero
Element of L;
A2:
now
let n be
Nat;
assume
A3: n
is_at_least_length_of (v
* p);
n
is_at_least_length_of p
proof
let i be
Nat;
reconsider i1 = i as
Element of
NAT by
ORDINAL1:def 12;
assume i
>= n;
then ((v
* p)
. i)
= (
0. L) by
A3;
then (v
* (p
. i1))
= (
0. L) by
POLYNOM5:def 4;
hence thesis by
VECTSP_2:def 1;
end;
hence (
len p)
<= n by
ALGSEQ_1:def 3;
end;
(
len p)
is_at_least_length_of (v
* p)
proof
let i be
Nat;
assume
A4: i
>= (
len p);
reconsider ii = i as
Element of
NAT by
ORDINAL1:def 12;
thus ((v
* p)
. i)
= (v
* (p
. ii)) by
POLYNOM5:def 4
.= (v
* (
0. L)) by
A4,
ALGSEQ_1: 8
.= (
0. L);
end;
hence (
len (v
* p))
= (
len p) by
A2,
ALGSEQ_1:def 3;
end;
theorem ::
RING_5:4
Th25: for R be
domRing, p be
Polynomial of R holds for a be non
zero
Element of R holds (
deg (a
* p))
= (
deg p)
proof
let L be
domRing, p be
Polynomial of L;
let v be non
zero
Element of L;
(
len (v
* p))
= (
len p) by
Th25a;
hence (
deg (v
* p))
= ((
len p)
- 1) by
HURWITZ:def 2
.= (
deg p) by
HURWITZ:def 2;
end;
theorem ::
RING_5:5
prl0a: for R be
domRing, p be
Polynomial of R holds for a be
Element of R holds (
LC (a
* p))
= (a
* (
LC p))
proof
let R be
domRing, p be
Polynomial of R;
let a be
Element of R;
per cases ;
suppose
A1: a
= (
0. R);
(a
* p)
= (
0_. R) by
A1,
POLYNOM5: 26;
hence thesis by
A1,
FUNCOP_1: 7;
end;
suppose a
<> (
0. R);
then
A3: a is non
zero;
thus (
LC (a
* p))
= (a
* (p
. ((
len (a
* p))
-' 1))) by
POLYNOM5:def 4
.= (a
* (
LC p)) by
A3,
Th25a;
end;
end;
theorem ::
RING_5:6
for R be
domRing, a be
Element of R holds (
LC (a
| R))
= a
proof
let R be
domRing, a be
Element of R;
thus (
LC (a
| R))
= (
LC (a
* (
1_. R))) by
RING_4: 16
.= (a
* (
LC (
1_. R))) by
prl0a
.= (a
* (
1. R)) by
RATFUNC1:def 7
.= a;
end;
theorem ::
RING_5:7
Th30: for R be
domRing, p be
Polynomial of R holds for v,x be
Element of R holds (
eval ((v
* p),x))
= (v
* (
eval (p,x)))
proof
let L be
domRing;
let p be
Polynomial of L;
let v,x be
Element of L;
consider F1 be
FinSequence of the
carrier of L such that
A1: (
eval (p,x))
= (
Sum F1) and
A2: (
len F1)
= (
len p) and
A3: for n be
Element of
NAT st n
in (
dom F1) holds (F1
. n)
= ((p
. (n
-' 1))
* ((
power L)
. (x,(n
-' 1)))) by
POLYNOM4:def 2;
consider F2 be
FinSequence of the
carrier of L such that
A4: (
eval ((v
* p),x))
= (
Sum F2) and
A5: (
len F2)
= (
len (v
* p)) and
A6: for n be
Element of
NAT st n
in (
dom F2) holds (F2
. n)
= (((v
* p)
. (n
-' 1))
* ((
power L)
. (x,(n
-' 1)))) by
POLYNOM4:def 2;
per cases ;
suppose v
<> (
0. L);
then
reconsider v1 = v as non
zero
Element of L by
STRUCT_0:def 12;
(
deg p)
= (
deg (v1
* p)) by
Th25;
then ((
len F1)
- 1)
= (
deg (v
* p)) by
A2,
HURWITZ:def 2
.= ((
len F2)
- 1) by
A5,
HURWITZ:def 2;
then
A7: (
dom F1)
= (
dom F2) by
FINSEQ_3: 29;
now
let i be
object;
assume
A8: i
in (
dom F1);
then
reconsider i1 = i as
Element of
NAT ;
A9: ((p
. (i1
-' 1))
* ((
power L)
. (x,(i1
-' 1))))
= (F1
. i) by
A3,
A8
.= (F1
/. i) by
A8,
PARTFUN1:def 6;
thus (F2
/. i)
= (F2
. i) by
A7,
A8,
PARTFUN1:def 6
.= (((v
* p)
. (i1
-' 1))
* ((
power L)
. (x,(i1
-' 1)))) by
A6,
A7,
A8
.= ((v
* (p
. (i1
-' 1)))
* ((
power L)
. (x,(i1
-' 1)))) by
POLYNOM5:def 4
.= (v
* (F1
/. i)) by
A9,
GROUP_1:def 3;
end;
then F2
= (v
* F1) by
A7,
POLYNOM1:def 1;
hence thesis by
A1,
A4,
POLYNOM1: 12;
end;
suppose
A10: v
= (
0. L);
hence (
eval ((v
* p),x))
= (
eval ((
0_. L),x)) by
POLYNOM5: 26
.= (v
* (
eval (p,x))) by
A10,
POLYNOM4: 17;
end;
end;
theorem ::
RING_5:8
evconst: for R be
Ring, a,b be
Element of R holds (
eval ((a
| R),b))
= a
proof
let R be
Ring, a,x be
Element of R;
set q = (a
| R);
consider F be
FinSequence of R such that
A3: (
eval (q,x))
= (
Sum F) and
A4: (
len F)
= (
len q) and
A5: for j be
Element of
NAT st j
in (
dom F) holds (F
. j)
= ((q
. (j
-' 1))
* ((
power R)
. (x,(j
-' 1)))) by
POLYNOM4:def 2;
per cases ;
suppose
A0: q
= (
0_. R);
then q
= ((
0. R)
| R) by
RING_4: 13;
then a
= (
0. R) by
RING_4: 19;
hence (
eval (q,x))
= a by
POLYNOM4: 17,
A0;
end;
suppose q
<> (
0_. R);
then q
<> ((
0. R)
| R) by
RING_4: 13;
then
B:
0
= (
deg q) by
RING_4: 21
.= ((
len q)
- 1) by
HURWITZ:def 2;
then 1
in (
Seg (
len F)) by
A4,
FINSEQ_1: 1;
then 1
in (
dom F) by
FINSEQ_1:def 3;
then (F
. 1)
= ((q
. (1
-' 1))
* ((
power R)
. (x,(1
-' 1)))) by
A5;
then F
=
<*((q
. (1
-' 1))
* ((
power R)
. (x,(1
-' 1))))*> by
A4,
B,
FINSEQ_1: 40
.=
<*((q
.
0 )
* ((
power R)
. (x,(1
-' 1))))*> by
XREAL_1: 232
.=
<*((q
.
0 )
* ((
power R)
. (x,
0 )))*> by
XREAL_1: 232
.=
<*(a
* ((
power R)
. (x,
0 )))*> by
Th28
.=
<*(a
* (
1_ R))*> by
GROUP_1:def 7
.=
<*a*>;
hence thesis by
A3,
RLVECT_1: 44;
end;
end;
prl2: for R be non
degenerated
comRing holds for p,q be
Polynomial of R holds for a be
Element of R st a
is_a_root_of p holds a
is_a_root_of (p
*' q)
proof
let R be non
degenerated
comRing, p,q be
Polynomial of R;
let a be
Element of R;
assume a
is_a_root_of p;
then (
eval (p,a))
= (
0. R) by
POLYNOM5:def 7;
then (
eval ((p
*' q),a))
= ((
0. R)
* (
eval (q,a))) by
POLYNOM4: 24
.= (
0. R);
hence thesis by
POLYNOM5:def 7;
end;
registration
let R be
domRing;
let p,q be
monic
Polynomial of R;
cluster (p
*' q) ->
monic;
coherence
proof
(
LC (p
*' q))
= ((
LC p)
* (
LC q)) by
NIVEN: 46
.= ((
LC p)
* (
1. R)) by
RATFUNC1:def 7
.= ((
1. R)
* (
1. R)) by
RATFUNC1:def 7;
hence thesis;
end;
end
registration
let R be
domRing;
let a be
Element of R;
let k be
Nat;
cluster ((
rpoly (1,a))
`^ k) -> non
zero
monic;
coherence
proof
defpred
P[
Nat] means ((
rpoly (1,a))
`^ $1) is non
zero
monic;
((
rpoly (1,a))
`^
0 )
= (
1_. R) by
POLYNOM5: 15;
then
IA:
P[
0 ];
IS:
now
let k be
Nat;
assume
P[k];
then (((
rpoly (1,a))
`^ k)
*' (
rpoly (1,a))) is
monic;
hence
P[(k
+ 1)] by
POLYNOM5: 19;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
hence thesis;
end;
end
theorem ::
RING_5:9
lcrpol: for R be non
degenerated
Ring, a be
Element of R, k be non
zero
Element of
NAT holds (
LC (
rpoly (k,a)))
= (
1. R)
proof
let R be non
degenerated
Ring, a be
Element of R, k be non
zero
Element of
NAT ;
(
deg (
rpoly (k,a)))
= ((
len (
rpoly (k,a)))
- 1) by
HURWITZ:def 2;
then k
= ((
len (
rpoly (k,a)))
- 1) by
HURWITZ: 27;
hence (
LC (
rpoly (k,a)))
= ((
rpoly (k,a))
. k) by
XREAL_0:def 2
.= (
1_ R) by
HURWITZ: 25
.= (
1. R);
end;
theorem ::
RING_5:10
repr: for R be non
degenerated
well-unital non
empty
doubleLoopStr holds for a be
Element of R holds
<%(
- a), (
1. R)%>
= (
rpoly (1,a))
proof
let R be non
degenerated
well-unital non
empty
doubleLoopStr, a be
Element of R;
set p =
<%(
- a), (
1. R)%>, q = (
rpoly (1,a));
A: 1
= (
deg q) by
HURWITZ: 27
.= ((
len q)
- 1) by
HURWITZ:def 2;
D: (
1. R)
<> (
0. R);
now
let k be
Nat;
assume k
< (
len p);
then k
< (1
+ 1) by
D,
POLYNOM5: 40;
then
B: k
<= 1 by
NAT_1: 13;
per cases by
B,
NAT_1: 25;
suppose
C: k
=
0 ;
hence (p
. k)
= (
- ((
1_ R)
* a)) by
POLYNOM5: 38
.= (
- (((
power R)
. (a,
0 ))
* a)) by
GROUP_1:def 7
.= (
- ((
power R)
. (a,(
0
+ 1)))) by
GROUP_1:def 7
.= (q
. k) by
C,
HURWITZ: 25;
end;
suppose
C: k
= 1;
hence (p
. k)
= (
1_ R) by
POLYNOM5: 38
.= (q
. k) by
C,
HURWITZ: 25;
end;
end;
hence thesis by
A,
D,
POLYNOM5: 40,
ALGSEQ_1: 12;
end;
theorem ::
RING_5:11
Th9: for R be
domRing holds for p be
Polynomial of R holds for x be
Element of R holds (
eval (p,x))
= (
0. R) iff (
rpoly (1,x))
divides p
proof
let L be
domRing;
let p be
Polynomial of L;
let x be
Element of L;
A1:
now
assume (
rpoly (1,x))
divides p;
then
consider u be
Polynomial of L such that
A2: ((
rpoly (1,x))
*' u)
= p by
RING_4: 1;
A3: (
eval ((
rpoly (1,x)),x))
= (x
- x) by
HURWITZ: 29
.= (
0. L) by
RLVECT_1: 15;
thus (
eval (p,x))
= ((
eval ((
rpoly (1,x)),x))
* (
eval (u,x))) by
A2,
POLYNOM4: 24
.= (
0. L) by
A3;
end;
now
assume (
eval (p,x))
= (
0. L);
then
consider s be
Polynomial of L such that
A4: p
= ((
rpoly (1,x))
*' s) by
HURWITZ: 33,
POLYNOM5:def 7;
thus (
rpoly (1,x))
divides p by
RING_4: 1,
A4;
end;
hence thesis by
A1;
end;
theorem ::
RING_5:12
for F be
domRing, p,q be
Polynomial of F holds for a be
Element of F st (
rpoly (1,a))
divides (p
*' q) holds (
rpoly (1,a))
divides p or (
rpoly (1,a))
divides q
proof
let L be
domRing, p,q be
Polynomial of L;
let x be
Element of L;
assume (
rpoly (1,x))
divides (p
*' q);
then (
eval ((p
*' q),x))
= (
0. L) by
Th9;
then
A1: ((
eval (p,x))
* (
eval (q,x)))
= (
0. L) by
POLYNOM4: 24;
per cases by
A1,
VECTSP_2:def 1;
suppose (
eval (p,x))
= (
0. L);
hence thesis by
Th9;
end;
suppose (
eval (q,x))
= (
0. L);
hence thesis by
Th9;
end;
end;
theorem ::
RING_5:13
prl25: for R be
domRing, p be
Polynomial of R holds for q be non
zero
Polynomial of R st p
divides q holds (
deg p)
<= (
deg q)
proof
let R be
domRing, p be
Polynomial of R;
let q be non
zero
Polynomial of R;
assume p
divides q;
then
consider r be
Polynomial of R such that
A: q
= (p
*' r) by
RING_4: 1;
C: p
<> (
0_. R) & r
<> (
0_. R) by
A;
then
reconsider dq = (
deg q), dr = (
deg r), dp = (
deg p) as
Element of
NAT by
T8;
dq
= (dr
+ dp) by
A,
C,
HURWITZ: 23;
hence thesis by
NAT_1: 11;
end;
theorem ::
RING_5:14
divi1: for R be non
degenerated
comRing, q be
Polynomial of R holds for p be non
zero
Polynomial of R holds for b be non
zero
Element of R st q
divides p holds q
divides (b
* p)
proof
let F be non
degenerated
comRing, q be
Polynomial of F;
let p be non
zero
Polynomial of F;
let b be non
zero
Element of F;
assume q
divides p;
then
consider r be
Polynomial of F such that
A: p
= (q
*' r) by
RING_4: 1;
(b
* (r
*' q))
= ((b
* r)
*' q) by
HURWITZ: 19;
hence q
divides (b
* p) by
A,
RING_4: 1;
end;
theorem ::
RING_5:15
for F be
Field, q be
Polynomial of F holds for p be non
zero
Polynomial of F holds for b be non
zero
Element of F holds q
divides p iff q
divides (b
* p)
proof
let F be
Field, q be
Polynomial of F;
let p be non
zero
Polynomial of F;
let b be non
zero
Element of F;
X: b
<> (
0. F);
now
assume q
divides (b
* p);
then
consider r be
Polynomial of F such that
A: (b
* p)
= (q
*' r) by
RING_4: 1;
(q
*' ((b
" )
* r))
= ((b
" )
* (q
*' r)) by
HURWITZ: 19
.= (((b
" )
* b)
* p) by
A,
HURWITZ: 14
.= ((
1. F)
* p) by
X,
VECTSP_1:def 10
.= p;
hence q
divides p by
RING_4: 1;
end;
hence thesis by
divi1;
end;
theorem ::
RING_5:16
divi1b: for R be
domRing, p be non
zero
Polynomial of R holds for a be
Element of R, b be non
zero
Element of R holds (
rpoly (1,a))
divides p iff (
rpoly (1,a))
divides (b
* p)
proof
let F be
domRing, p be non
zero
Polynomial of F;
let a be
Element of F, b be non
zero
Element of F;
set q = (
rpoly (1,a));
now
assume q
divides (b
* p);
then (
0. F)
= (
eval ((b
* p),a)) by
Th9
.= (b
* (
eval (p,a))) by
Th30;
then (
eval (p,a))
= (
0. F) by
VECTSP_2:def 1;
hence q
divides p by
Th9;
end;
hence thesis by
divi1;
end;
theorem ::
RING_5:17
divi1ad: for R be
domRing, p be non
zero
Polynomial of R holds for a be
Element of R, b be non
zero
Element of R holds ((
rpoly (1,a))
`^ n)
divides p iff ((
rpoly (1,a))
`^ n)
divides (b
* p)
proof
let R be
domRing, p be non
zero
Polynomial of R;
let a be
Element of R, b be non
zero
Element of R;
defpred
P[
Nat] means ((
rpoly (1,a))
`^ $1)
divides (b
* p) implies ((
rpoly (1,a))
`^ $1)
divides p;
now
assume ((
rpoly (1,a))
`^
0 )
divides (b
* p);
((
rpoly (1,a))
`^
0 )
= (
1_. R) by
POLYNOM5: 15;
then (((
rpoly (1,a))
`^
0 )
*' p)
= p;
hence ((
rpoly (1,a))
`^
0 )
divides p by
RING_4: 1;
end;
then
IA:
P[
0 ];
IS:
now
let k be
Nat;
assume
AS:
P[k];
now
assume ((
rpoly (1,a))
`^ (k
+ 1))
divides (b
* p);
then
consider r be
Polynomial of R such that
A1: (((
rpoly (1,a))
`^ (k
+ 1))
*' r)
= (b
* p) by
RING_4: 1;
C: (((
rpoly (1,a))
`^ k)
*' ((
rpoly (1,a))
*' r))
= ((((
rpoly (1,a))
`^ k)
*' (
rpoly (1,a)))
*' r) by
POLYNOM3: 33
.= (b
* p) by
A1,
POLYNOM5: 19;
then
consider r1 be
Polynomial of R such that
A2: (((
rpoly (1,a))
`^ k)
*' r1)
= p by
AS,
RING_4: 1;
reconsider r1 as non
zero
Polynomial of R by
A2;
((b
* r1)
*' ((
rpoly (1,a))
`^ k))
= (((
rpoly (1,a))
*' r)
*' ((
rpoly (1,a))
`^ k)) by
C,
A2,
RATFUNC1: 5;
then (b
* r1)
= ((
rpoly (1,a))
*' r) by
RATFUNC1: 7;
then (
rpoly (1,a))
divides r1 by
divi1b,
RING_4: 1;
then
consider r2 be
Polynomial of R such that
A3: ((
rpoly (1,a))
*' r2)
= r1 by
RING_4: 1;
p
= ((((
rpoly (1,a))
`^ k)
*' (
rpoly (1,a)))
*' r2) by
A2,
A3,
POLYNOM3: 33
.= (((
rpoly (1,a))
`^ (k
+ 1))
*' r2) by
POLYNOM5: 19;
hence ((
rpoly (1,a))
`^ (k
+ 1))
divides p by
RING_4: 1;
end;
hence
P[(k
+ 1)];
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
hence thesis by
divi1;
end;
registration
let R be
domRing;
let p be non
zero
Polynomial of R;
let b be non
zero
Element of R;
cluster (b
* p) -> non
zero;
coherence
proof
for p be
Polynomial of R st (for a be
Element of
NAT holds (p
. a)
= (
0. R)) holds p
= (
0_. R)
proof
let p be
Polynomial of R;
assume
AS: for a be
Element of
NAT holds (p
. a)
= (
0. R);
now
assume (
len p)
<>
0 ;
then
consider k be
Nat such that
D3: (
len p)
= (k
+ 1) by
NAT_1: 6;
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
(p
. k)
<> (
0. R) by
D3,
ALGSEQ_1: 10;
hence contradiction by
AS;
end;
hence thesis by
POLYNOM4: 5;
end;
then
consider a be
Element of
NAT such that
A: (p
. a)
<> (
0. R);
(b
* (p
. a))
<> (
0. R) by
A,
VECTSP_2:def 1;
then ((b
* p)
. a)
<> (
0. R) by
POLYNOM5:def 4;
hence thesis by
FUNCOP_1: 7;
end;
end
begin
registration
let R be non
degenerated
Ring;
cluster (
1_. R) -> non
with_roots;
coherence
proof
set p = (
1_. R);
assume p is
with_roots;
then
consider x be
Element of R such that
A: x
is_a_root_of p by
POLYNOM5:def 8;
(
0. R)
= (
eval (p,x)) by
A,
POLYNOM5:def 7
.= (
1. R) by
POLYNOM4: 18;
hence contradiction;
end;
end
registration
let R be non
degenerated
Ring;
let a be non
zero
Element of R;
cluster (a
| R) -> non
with_roots;
coherence
proof
set p = (a
| R);
assume p is
with_roots;
then
consider x be
Element of R such that
A: x
is_a_root_of p by
POLYNOM5:def 8;
(
0. R)
= (
eval (p,x)) by
A,
POLYNOM5:def 7
.= a by
evconst;
hence contradiction;
end;
end
registration
let R be non
degenerated
Ring;
cluster non
zero
with_roots -> non
constant for
Polynomial of R;
coherence
proof
let q be
Polynomial of R;
assume
AS: q is non
zero
with_roots;
reconsider p = q as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
reconsider degp = (
deg p) as
Element of
NAT by
AS,
T8;
consider x be
Element of R such that
X: x
is_a_root_of p by
AS,
POLYNOM5:def 8;
H: (
eval (p,x))
= (
0. R) by
X,
POLYNOM5:def 7;
now
assume
A: p is
constant;
then
consider a be
Element of R such that
B: p
= (a
| R) by
RING_4: 20;
degp
=
0 by
A;
then a
<> (
0. R) by
B,
RING_4: 21;
hence contradiction by
H,
B,
evconst;
end;
hence thesis;
end;
end
registration
let R be non
degenerated
Ring;
cluster non
with_roots -> non
zero for
Polynomial of R;
coherence ;
end
registration
let R be non
degenerated
Ring;
let a be
Element of R;
cluster (
rpoly (1,a)) -> non
zero
with_roots;
coherence by
HURWITZ: 30,
POLYNOM5:def 8;
end
registration
let R be non
degenerated
Ring;
cluster non
zero non
with_roots for
Polynomial of R;
existence
proof
take (
1_. R);
thus thesis;
end;
cluster non
zero
with_roots for
Polynomial of R;
existence
proof
take (
rpoly (1,(
1. R)));
thus thesis;
end;
end
registration
let R be
domRing;
let p be non
with_roots
Polynomial of R;
let a be non
zero
Element of R;
cluster (a
* p) -> non
with_roots;
coherence
proof
now
assume (a
* p) is
with_roots;
then
consider b be
Element of R such that
A: b
is_a_root_of (a
* p) by
POLYNOM5:def 8;
(
0. R)
= (
eval ((a
* p),b)) by
A,
POLYNOM5:def 7
.= (a
* (
eval (p,b))) by
Th30;
then (
eval (p,b))
= (
0. R) by
VECTSP_2:def 1;
hence contradiction by
POLYNOM5:def 8,
POLYNOM5:def 7;
end;
hence thesis;
end;
end
registration
let R be
domRing;
let p be
with_roots
Polynomial of R;
let a be
Element of R;
cluster (a
* p) ->
with_roots;
coherence
proof
consider b be
Element of R such that
A: b
is_a_root_of p by
POLYNOM5:def 8;
(
eval ((a
* p),b))
= (a
* (
eval (p,b))) by
Th30
.= (a
* (
0. R)) by
A,
POLYNOM5:def 7;
hence thesis by
POLYNOM5:def 8,
POLYNOM5:def 7;
end;
end
registration
let R be non
degenerated
comRing;
let p be
with_roots
Polynomial of R;
let q be
Polynomial of R;
cluster (p
*' q) ->
with_roots;
coherence
proof
consider a be
Element of R such that
A: a
is_a_root_of p by
POLYNOM5:def 8;
thus thesis by
A,
prl2,
POLYNOM5:def 8;
end;
end
registration
let R be
domRing;
let p,q be non
with_roots
Polynomial of R;
cluster (p
*' q) -> non
with_roots;
coherence
proof
now
assume (p
*' q) is
with_roots;
then
consider a be
Element of R such that
H: a
is_a_root_of (p
*' q) by
POLYNOM5:def 8;
A: (
0. R)
= (
eval ((p
*' q),a)) by
H,
POLYNOM5:def 7
.= ((
eval (p,a))
* (
eval (q,a))) by
POLYNOM4: 24;
per cases by
A,
VECTSP_2:def 1;
suppose (
eval (p,a))
= (
0. R);
hence contradiction by
POLYNOM5:def 8,
POLYNOM5:def 7;
end;
suppose (
eval (q,a))
= (
0. R);
hence contradiction by
POLYNOM5:def 8,
POLYNOM5:def 7;
end;
end;
hence thesis;
end;
end
registration
let R be non
degenerated
comRing;
let a be
Element of R;
let k be non
zero
Element of
NAT ;
cluster (
rpoly (k,a)) -> non
constant
monic
with_roots;
coherence
proof
set p = (
rpoly (k,a));
thus p is non
constant by
HURWITZ: 27;
(
deg p)
>=
0 ;
then ((
len p)
- 1)
>=
0 by
HURWITZ:def 2;
then (
0
+ 1)
<= (((
len p)
- 1)
+ 1) by
XREAL_1: 6;
then
A: ((
len p)
-' 1)
= ((
len p)
- 1) by
XREAL_1: 233
.= (
deg p) by
HURWITZ:def 2;
(
LC p)
= (p
. k) by
A,
HURWITZ: 27
.= (
1_ R) by
HURWITZ: 25
.= (
1. R);
hence p is
monic;
per cases by
NAT_1: 53;
suppose k
= 1;
hence p is
with_roots;
end;
suppose k
> 1;
then ((
rpoly (1,a))
*' (
qpoly (k,a)))
= (
rpoly (k,a)) by
HURWITZ: 32;
hence p is
with_roots;
end;
end;
end
registration
let R be non
degenerated
Ring;
cluster non
constant
monic for
Polynomial of R;
existence
proof
take (
rpoly (1,(
1. R)));
thus thesis;
end;
end
registration
let R be
domRing;
let a be
Element of R;
let k be non
zero
Nat;
let n be non
zero
Element of
NAT ;
cluster ((
rpoly (n,a))
`^ k) -> non
constant
monic
with_roots;
coherence
proof
defpred
P[
Nat] means ((
rpoly (n,a))
`^ $1) is non
constant
monic
with_roots;
IA:
P[1] by
POLYNOM5: 16;
IS:
now
let k be
Nat;
assume 1
<= k;
assume
P[k];
then (((
rpoly (n,a))
`^ k)
*' (
rpoly (n,a))) is non
constant
monic
with_roots;
hence
P[(k
+ 1)] by
POLYNOM5: 19;
end;
I: for k be
Nat st 1
<= k holds
P[k] from
NAT_1:sch 8(
IA,
IS);
1
<= k by
NAT_1: 53;
hence thesis by
I;
end;
end
registration
let R be
Ring;
let p be
with_roots
Polynomial of R;
cluster (
Roots p) -> non
empty;
coherence
proof
ex x be
Element of R st x
is_a_root_of p by
POLYNOM5:def 8;
hence thesis by
POLYNOM5:def 10;
end;
end
registration
let R be non
degenerated
Ring;
let p be non
with_roots
Polynomial of R;
cluster (
Roots p) ->
empty;
coherence
proof
now
assume
A: (
Roots p)
<>
{} ;
let u be
Element of (
Roots p);
u
in (
Roots p) by
A;
then
reconsider x = u as
Element of R;
x
is_a_root_of p by
A,
POLYNOM5:def 10;
hence contradiction by
POLYNOM5:def 8;
end;
hence thesis;
end;
end
registration
let R be
domRing;
cluster
monic
with_roots for
Polynomial of R;
existence
proof
take (
rpoly (1,(
0. R)));
thus thesis;
end;
cluster
monic non
with_roots for
Polynomial of R;
existence
proof
take (
1_. R);
thus thesis;
end;
end
theorem ::
RING_5:18
ro4: for R be non
degenerated
Ring, a be
Element of R holds (
Roots (
rpoly (1,a)))
=
{a}
proof
let R be non
degenerated
Ring, a be
Element of R;
set p = (
rpoly (1,a));
A:
now
let u be
object;
assume u
in
{a};
then
A: u
= a by
TARSKI:def 1;
(
eval (p,a))
= (a
- a) by
HURWITZ: 29
.= (
0. R) by
RLVECT_1: 15;
then a
is_a_root_of p by
POLYNOM5:def 7;
hence u
in (
Roots p) by
A,
POLYNOM5:def 10;
end;
now
let u be
object;
assume
B: u
in (
Roots p);
then
reconsider x = u as
Element of R;
x
is_a_root_of p by
B,
POLYNOM5:def 10;
then (
0. R)
= (
eval (p,x)) by
POLYNOM5:def 7
.= (x
- a) by
HURWITZ: 29;
then a
= x by
RLVECT_1: 21;
hence u
in
{a} by
TARSKI:def 1;
end;
hence thesis by
A,
TARSKI: 2;
end;
theorem ::
RING_5:19
for F be
domRing, p be
Polynomial of F holds for b be non
zero
Element of F holds (
Roots (b
* p))
= (
Roots p)
proof
let R be
domRing, p be
Polynomial of R;
let b be non
zero
Element of R;
A:
now
let o be
object;
assume
B0: o
in (
Roots p);
then
reconsider a = o as
Element of R;
a
is_a_root_of p by
B0,
POLYNOM5:def 10;
then (
0. R)
= (
eval (p,a)) by
POLYNOM5:def 7;
then (
eval ((b
* p),a))
= (b
* (
0. R)) by
Th30
.= (
0. R);
then a
is_a_root_of (b
* p) by
POLYNOM5:def 7;
hence o
in (
Roots (b
* p)) by
POLYNOM5:def 10;
end;
now
let o be
object;
assume
B0: o
in (
Roots (b
* p));
then
reconsider a = o as
Element of R;
a
is_a_root_of (b
* p) by
B0,
POLYNOM5:def 10;
then (
0. R)
= (
eval ((b
* p),a)) by
POLYNOM5:def 7
.= (b
* (
eval (p,a))) by
Th30;
then (
eval (p,a))
= (
0. R) by
VECTSP_2:def 1;
then a
is_a_root_of p by
POLYNOM5:def 7;
hence o
in (
Roots p) by
POLYNOM5:def 10;
end;
hence thesis by
A,
TARSKI: 2;
end;
theorem ::
RING_5:20
ex p,q be
Polynomial of (
Z/ 6) st not (
Roots (p
*' q))
c= ((
Roots p)
\/ (
Roots q))
proof
set R = (
Z/ 6), z = (2
'*' (
1. (
Z/ 6))), d = (3
'*' (
1. (
Z/ 6)));
take p = (
rpoly (1,z)), q = (
rpoly (1,d));
C: (
Char R)
= 6 by
RING_3: 77;
(
eval ((p
*' q),(
0. R)))
= ((
eval (p,(
0. R)))
* (
eval (q,(
0. R)))) by
POLYNOM4: 24
.= (((
0. R)
- z)
* (
eval (q,(
0. R)))) by
HURWITZ: 29
.= (((
0. R)
- z)
* ((
0. R)
- d)) by
HURWITZ: 29
.= ((
- z)
* ((
0. R)
- d)) by
RLVECT_1: 14
.= ((
- z)
* (
- d)) by
RLVECT_1: 14
.= (z
* d) by
VECTSP_1: 10
.= ((2
* 3)
'*' (
1. R)) by
RING_3: 67
.= (
0. R) by
C,
RING_3:def 5;
then (
0. R)
is_a_root_of (p
*' q) by
POLYNOM5:def 7;
then
B: (
0. R)
in (
Roots (p
*' q)) by
POLYNOM5:def 10;
now
assume
AS: (
0. R)
in ((
Roots p)
\/ (
Roots q));
per cases by
AS,
XBOOLE_0:def 3;
suppose (
0. R)
in (
Roots p);
then (
0. R)
is_a_root_of p by
POLYNOM5:def 10;
then
B: (
0. R)
= (
eval (p,(
0. R))) by
POLYNOM5:def 7
.= ((
0. R)
- z) by
HURWITZ: 29
.= (
- z) by
RLVECT_1: 14;
z
= (
- (
- z))
.= (
0. R) by
B;
hence contradiction by
C,
RING_3:def 5;
end;
suppose (
0. R)
in (
Roots q);
then (
0. R)
is_a_root_of q by
POLYNOM5:def 10;
then
B: (
0. R)
= (
eval (q,(
0. R))) by
POLYNOM5:def 7
.= ((
0. R)
- d) by
HURWITZ: 29
.= (
- d) by
RLVECT_1: 14;
d
= (
- (
- d))
.= (
0. R) by
B;
hence contradiction by
C,
RING_3:def 5;
end;
end;
hence thesis by
B;
end;
theorem ::
RING_5:21
div100: for R be
domRing, a,b be
Element of R holds (
rpoly (1,a))
divides (
rpoly (1,b)) iff a
= b
proof
let R be
domRing, a,b be
Element of R;
X:
now
assume (
rpoly (1,a))
divides (
rpoly (1,b));
then
consider p be
Polynomial of R such that
A: ((
rpoly (1,a))
*' p)
= (
rpoly (1,b)) by
RING_4: 1;
B:
{b}
= (
Roots (
rpoly (1,b))) by
ro4
.= ((
Roots (
rpoly (1,a)))
\/ (
Roots p)) by
A,
UPROOTS: 23;
a
in
{a} by
TARSKI:def 1;
then a
in (
Roots (
rpoly (1,a))) by
ro4;
then a
in
{b} by
B,
XBOOLE_0:def 3;
hence a
= b by
TARSKI:def 1;
end;
now
assume a
= b;
then ((
rpoly (1,a))
*' (
1_. R))
= (
rpoly (1,b));
hence (
rpoly (1,a))
divides (
rpoly (1,b)) by
RING_4: 1;
end;
hence thesis by
X;
end;
degpol: for R be
domRing holds for p be non
zero
Polynomial of R holds ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p)
proof
let R be
domRing, p be non
zero
Polynomial of R;
defpred
P[
Nat] means for p be non
zero
Polynomial of R st (
deg p)
= $1 holds ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p);
IA:
P[
0 ]
proof
let p be non
zero
Polynomial of R;
assume
A1: (
deg p)
=
0 ;
reconsider q = p as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
consider a be
Element of R such that
A2: q
= (a
| R) by
A1,
RING_4:def 4,
RING_4: 20;
now
assume
A3: (
Roots p)
<>
{} ;
let u be
Element of (
Roots p);
u
in (
Roots p) by
A3;
then
reconsider u as
Element of R;
u
is_a_root_of p by
A3,
POLYNOM5:def 10;
then (
eval (p,u))
= (
0. R) by
POLYNOM5:def 7;
then a
= (
0. R) by
A2,
evconst;
hence contradiction by
A2;
end;
hence ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p);
end;
IS:
now
let k be
Nat;
assume
IV:
P[k];
now
let p be non
zero
Polynomial of R;
assume
A1: (
deg p)
= (k
+ 1);
per cases ;
suppose ex x be
Element of R st x
is_a_root_of p;
then
consider x be
Element of R such that
A2: x
is_a_root_of p;
consider q be
Polynomial of R such that
A3: p
= ((
rpoly (1,x))
*' q) by
A2,
HURWITZ: 33;
A4: q
<> (
0_. R) by
A3;
reconsider q as non
zero
Polynomial of R by
A3;
A7: (
deg p)
= ((
deg q)
+ (
deg (
rpoly (1,x)))) by
HURWITZ: 23,
A3,
A4
.= ((
deg q)
+ 1) by
HURWITZ: 27;
then
consider m be
natural
number such that
A5: m
= (
card (
Roots q)) & m
<= (
deg q) by
A1,
IV;
reconsider RQ = (
Roots q) as
finite
Subset of R;
now
per cases ;
case x
in (
Roots q);
then for o be
object st o
in
{x} holds o
in (
Roots q) by
TARSKI:def 1;
then
A6: (
card (RQ
\/
{x}))
= m by
A5,
XBOOLE_1: 12,
TARSKI:def 3;
(
Roots (
rpoly (1,x)))
=
{x} by
ro4;
then
A8: (
card (
Roots p))
= m by
A3,
A6,
UPROOTS: 23;
(
deg q)
<= ((
deg q)
+ 1) by
NAT_1: 11;
hence ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p) by
A7,
A8,
A5,
XXREAL_0: 2;
end;
case not (x
in (
Roots q));
then
A6: (
card (RQ
\/
{x}))
= (m
+ 1) by
A5,
CARD_2: 41;
(
Roots (
rpoly (1,x)))
=
{x} by
ro4;
then (
card (
Roots p))
= (m
+ 1) by
A3,
A6,
UPROOTS: 23;
hence ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p) by
A7,
A5,
XREAL_1: 6;
end;
end;
hence ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p);
end;
suppose
A2: not ex x be
Element of R st x
is_a_root_of p;
now
assume
A3: (
Roots p)
<>
{} ;
let x be
Element of (
Roots p);
x
in (
Roots p) by
A3;
then
reconsider x as
Element of R;
x
is_a_root_of p by
A3,
POLYNOM5:def 10;
hence contradiction by
A2;
end;
hence ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p);
end;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
p
<> (
0_. R);
then (
deg p) is
Element of
NAT by
T8;
hence thesis by
I;
end;
theorem ::
RING_5:22
degpoly: for R be
domRing, p be non
zero
Polynomial of R holds (
card (
Roots p))
<= (
deg p)
proof
let R be
domRing, p be non
zero
Polynomial of R;
ex n be
natural
number st n
= (
card (
Roots p)) & n
<= (
deg p) by
degpol;
hence thesis;
end;
begin
notation
let X be non
empty
set;
let B be
bag of X;
synonym
card B for
Sum B;
end
bbbag: for X be non
empty
set, b be
bag of X holds b is
zero iff (
rng b)
=
{
0 }
proof
let X be non
empty
set, b be
bag of X;
A:
now
assume
B: b is
zero;
C:
now
let o be
object;
assume o
in (
rng b);
then
consider y be
object such that
D: y
in (
dom b) & (b
. y)
= o by
FUNCT_1:def 3;
o
=
0 by
B,
D;
hence o
in
{
0 } by
TARSKI:def 1;
end;
now
let o be
object;
assume o
in
{
0 };
then
D: o
=
0 by
TARSKI:def 1;
set y = the
Element of X;
E: (
dom b)
= X by
PARTFUN1:def 2;
(b
. y)
=
0 by
B;
hence o
in (
rng b) by
D,
E,
FUNCT_1:def 3;
end;
hence (
rng b)
=
{
0 } by
C,
TARSKI: 2;
end;
now
assume
B: (
rng b)
=
{
0 };
now
let o be
object;
assume o
in X;
then o
in (
dom b) by
PARTFUN1:def 2;
then (b
. o)
in (
rng b) by
FUNCT_1: 3;
hence (b
. o)
=
{} by
B,
TARSKI:def 1;
end;
hence b is
zero by
PBOOLE: 6;
end;
hence thesis by
A;
end;
registration
let X be non
empty
set;
cluster
zero for
bag of X;
existence
proof
take (
EmptyBag X);
thus thesis;
end;
cluster non
zero for
bag of X;
existence
proof
set x = the
Element of X;
reconsider b = ((
{x},1)
-bag ) as
bag of X;
take b;
D: (
support b)
c= (
dom b) by
PRE_POLY: 37;
x
in
{x} by
TARSKI:def 1;
then
A: (b
. x)
= 1 by
UPROOTS: 7;
then
C: x
in (
support b) by
PRE_POLY:def 7;
now
assume (
rng b)
=
{
0 };
then (b
. x)
in
{
0 } by
C,
D,
FUNCT_1: 3;
hence contradiction by
A,
TARSKI:def 1;
end;
hence thesis by
bbbag;
end;
end
registration
let X be non
empty
set;
let b1 be
bag of X;
let b2 be
bag of X;
cluster (b1
+ b2) -> X
-defined;
coherence ;
end
registration
let X be non
empty
set;
let b1 be
bag of X;
let b2 be
bag of X;
cluster (b1
+ b2) ->
total;
coherence ;
end
theorem ::
RING_5:23
bag1a: for X be non
empty
set, b be
bag of X holds (
card b)
=
0 iff (
support b)
=
{}
proof
let X be non
empty
set, b be
bag of X;
A:
now
assume (
support b)
=
{} ;
then b
= (
EmptyBag X) by
PRE_POLY: 81;
hence (
card b)
=
0 by
UPROOTS: 11;
end;
now
assume (
card b)
=
0 ;
then b
= (
EmptyBag X) by
UPROOTS: 12;
hence (
support b)
=
{} ;
end;
hence thesis by
A;
end;
theorem ::
RING_5:24
bbag: for X be non
empty
set, b be
bag of X holds b is
zero iff (
support b)
=
{}
proof
let X be non
empty
set, b be
bag of X;
now
assume (
support b)
=
{} ;
then for o be
object st o
in X holds (b
. o)
=
{} by
PRE_POLY:def 7;
hence b is
zero by
PBOOLE: 6;
end;
hence thesis;
end;
theorem ::
RING_5:25
for X be non
empty
set, b be
bag of X holds b is
zero iff (
rng b)
=
{
0 } by
bbbag;
registration
let X be non
empty
set;
let b1 be non
zero
bag of X;
let b2 be
bag of X;
cluster (b1
+ b2) -> non
zero;
coherence
proof
A: (
support b1)
<>
{} by
bbag;
set o = the
Element of (
support b1);
D: (b1
. o)
<>
0 by
A,
PRE_POLY:def 7;
set b = (b1
+ b2);
(b
. o)
= ((b1
. o)
+ (b2
. o)) by
PRE_POLY:def 5;
hence thesis by
D;
end;
end
theorem ::
RING_5:26
bb7a: for X be non
empty
set, b be
bag of X, x be
Element of X holds (
support b)
=
{x} implies b
= ((
{x},(b
. x))
-bag )
proof
let X be non
empty
set, b be
bag of X, x be
Element of X;
assume
AS: (
support b)
=
{x};
now
let o be
object;
assume o
in X;
per cases ;
suppose
A: o
= x;
then o
in
{x} by
TARSKI:def 1;
hence (b
. o)
= (((
{x},(b
. x))
-bag )
. o) by
A,
UPROOTS: 7;
end;
suppose o
<> x;
then
B: not o
in
{x} by
TARSKI:def 1;
hence (((
{x},(b
. x))
-bag )
. o)
=
0 by
UPROOTS: 6
.= (b
. o) by
AS,
B,
PRE_POLY:def 7;
end;
end;
hence b
= ((
{x},(b
. x))
-bag ) by
PBOOLE: 3;
end;
theorem ::
RING_5:27
bb7: for X be non
empty
set, b be non
empty
bag of X, x be
Element of X holds (
support b)
=
{x} iff (b
= ((
{x},(b
. x))
-bag ) & (b
. x)
<>
0 )
proof
let X be non
empty
set, b be non
empty
bag of X, x be
Element of X;
now
assume
AS: (
support b)
=
{x};
then x
in (
support b) by
TARSKI:def 1;
hence b
= ((
{x},(b
. x))
-bag ) & (b
. x)
<>
0 by
AS,
bb7a,
PRE_POLY:def 7;
end;
hence thesis by
UPROOTS: 8;
end;
definition
let X be
set;
let S be
finite
Subset of X;
::
RING_5:def1
func
Bag S ->
bag of X equals ((S,1)
-bag );
coherence ;
end
registration
let X be non
empty
set;
let S be non
empty
finite
Subset of X;
cluster (
Bag S) -> non
zero;
coherence
proof
set x = the
Element of S;
reconsider x as
Element of X;
B: (
dom (
Bag S))
= X by
PARTFUN1:def 2;
((
Bag S)
. x)
= 1 by
UPROOTS: 7;
then 1
in (
rng (
Bag S)) by
B,
FUNCT_1: 3;
then (
rng (
Bag S))
<>
{
0 } by
TARSKI:def 1;
hence thesis by
bbbag;
end;
end
definition
let X be non
empty
set;
let b be
bag of X;
let a be
Element of X;
::
RING_5:def2
func b
\ a ->
bag of X equals (b
+* (a,
0 ));
coherence ;
end
bb1: for X be non
empty
set, b be
bag of X, a be
Element of X holds ((b
\ a)
. a)
=
0
proof
let X be non
empty
set, b be
bag of X, a be
Element of X;
X
= (
dom b) by
PARTFUN1:def 2;
hence thesis by
FUNCT_7: 31;
end;
theorem ::
RING_5:28
for X be non
empty
set, b be
bag of X, a be
Element of X holds (b
\ a)
= b iff not a
in (
support b)
proof
let X be non
empty
set, b be
bag of X, a be
Element of X;
A:
now
assume
B: not a
in (
support b);
now
let o be
object;
assume o
in X;
per cases ;
suppose
D: o
= a;
hence ((b
\ a)
. o)
=
0 by
bb1
.= (b
. o) by
B,
D,
PRE_POLY:def 7;
end;
suppose o
<> a;
hence ((b
\ a)
. o)
= (b
. o) by
FUNCT_7: 32;
end;
end;
hence (b
\ a)
= b by
PBOOLE: 3;
end;
now
assume (b
\ a)
= b;
then (b
. a)
=
0 by
bb1;
hence not a
in (
support b) by
PRE_POLY:def 7;
end;
hence thesis by
A;
end;
theorem ::
RING_5:29
bb3a: for X be non
empty
set, b be
bag of X, a be
Element of X holds (
support (b
\ a))
= ((
support b)
\
{a})
proof
let X be non
empty
set, b be
bag of X, a be
Element of X;
A:
now
let o be
object;
assume
X: o
in (
support (b
\ a));
then
reconsider c = o as
Element of X;
B: ((b
\ a)
. o)
<>
0 by
X,
PRE_POLY:def 7;
then
D: a
<> o by
bb1;
then (b
. c)
= ((b
\ a)
. c) by
FUNCT_7: 32;
then
C: o
in (
support b) by
B,
PRE_POLY:def 7;
not o
in
{a} by
D,
TARSKI:def 1;
hence o
in ((
support b)
\
{a}) by
C,
XBOOLE_0:def 5;
end;
now
let o be
object;
assume
X: o
in ((
support b)
\
{a});
then
reconsider c = o as
Element of X;
B: o
in (
support b) & not o
in
{a} by
X,
XBOOLE_0:def 5;
then o
<> a by
TARSKI:def 1;
then ((b
\ a)
. c)
= (b
. c) by
FUNCT_7: 32;
then ((b
\ a)
. o)
<>
0 by
B,
PRE_POLY:def 7;
hence o
in (
support (b
\ a)) by
PRE_POLY:def 7;
end;
hence thesis by
A,
TARSKI: 2;
end;
theorem ::
RING_5:30
bb3: for X be non
empty
set, b be
bag of X, a be
Element of X holds ((b
\ a)
+ ((
{a},(b
. a))
-bag ))
= b
proof
let X be non
empty
set, b be
bag of X, a be
Element of X;
set c = ((b
\ a)
+ ((
{a},(b
. a))
-bag ));
now
let o be
object;
assume o
in X;
X: (c
. o)
= (((b
\ a)
. o)
+ (((
{a},(b
. a))
-bag )
. o)) by
PRE_POLY:def 5;
per cases ;
suppose
A: o
= a;
then
B: o
in
{a} by
TARSKI:def 1;
thus (c
. o)
= (
0
+ (((
{a},(b
. a))
-bag )
. o)) by
A,
X,
bb1
.= (b
. o) by
A,
B,
UPROOTS: 7;
end;
suppose
A: o
<> a;
then not o
in
{a} by
TARSKI:def 1;
hence (c
. o)
= (((b
\ a)
. o)
+
0 ) by
X,
UPROOTS: 6
.= (b
. o) by
A,
FUNCT_7: 32;
end;
end;
hence thesis by
PBOOLE: 3;
end;
theorem ::
RING_5:31
bb4: for X be non
empty
set, a be
Element of X, n be
Element of
NAT holds (
card ((
{a},n)
-bag ))
= n
proof
let X be non
empty
set, a be
Element of X, n be
Element of
NAT ;
reconsider b = ((
{a},n)
-bag ) as
bag of X;
consider F be
FinSequence of
NAT such that
H: (
degree b)
= (
Sum F) & F
= (b
* (
canFS (
support b))) by
UPROOTS:def 4;
I: a
in
{a} by
TARSKI:def 1;
per cases ;
suppose
X: n
=
0 ;
then b
= (
EmptyBag X) by
UPROOTS: 9;
then (
support b)
=
{} ;
hence thesis by
X,
bag1a;
end;
suppose n
<>
0 ;
then
A: (
support b)
=
{a} by
UPROOTS: 8;
then
C: a
in (
support b) by
TARSKI:def 1;
B: (
support b)
c= (
dom b) by
PRE_POLY: 37;
F
= (b
*
<*a*>) by
A,
H,
FINSEQ_1: 94
.=
<*(b
. a)*> by
C,
B,
FINSEQ_2: 34
.=
<*n*> by
I,
UPROOTS: 7;
hence thesis by
H,
RVSUM_1: 73;
end;
end;
begin
registration
let R be
domRing;
let p be non
zero
with_roots
Polynomial of R;
cluster (
BRoots p) -> non
zero;
coherence
proof
consider x be
Element of R such that
A: x
is_a_root_of p by
POLYNOM5:def 8;
(
multiplicity (p,x))
>= 1 by
A,
UPROOTS: 52;
then ((
BRoots p)
. x)
>= 1 by
UPROOTS:def 9;
hence thesis;
end;
end
theorem ::
RING_5:32
multipp0: for R be non
degenerated
comRing, p be non
zero
Polynomial of R holds for a be
Element of R holds (
multiplicity (p,a))
=
0 iff not (
rpoly (1,a))
divides p
proof
let R be non
degenerated
comRing, p be non
zero
Polynomial of R;
let a be
Element of R;
A:
now
assume (
multiplicity (p,a))
=
0 ;
then
C: not (a
is_a_root_of p) by
UPROOTS: 52;
now
assume (
rpoly (1,a))
divides p;
then
consider s be
Polynomial of R such that
B: p
= ((
rpoly (1,a))
*' s) by
RING_4: 1;
thus contradiction by
C,
B,
prl2,
HURWITZ: 30;
end;
hence not (
rpoly (1,a))
divides p;
end;
now
assume (
multiplicity (p,a))
<>
0 ;
then ((
multiplicity (p,a))
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (
multiplicity (p,a))
>= 1 by
NAT_1: 13;
then ex s be
Polynomial of R st p
= ((
rpoly (1,a))
*' s) by
UPROOTS: 52,
HURWITZ: 33;
hence (
rpoly (1,a))
divides p by
RING_4: 1;
end;
hence thesis by
A;
end;
theorem ::
RING_5:33
multip: for R be
domRing, p be non
zero
Polynomial of R holds for a be
Element of R holds (
multiplicity (p,a))
= n iff (((
rpoly (1,a))
`^ n)
divides p & not ((
rpoly (1,a))
`^ (n
+ 1))
divides p)
proof
let R be
domRing, p be non
zero
Polynomial of R;
let a be
Element of R;
A:
now
assume (
multiplicity (p,a))
= n;
then
consider F be
finite non
empty
Subset of
NAT such that
B: F
= { k where k be
Element of
NAT : ex q be
Polynomial of R st p
= ((
<%(
- a), (
1. R)%>
`^ k)
*' q) } & n
= (
max F) by
UPROOTS:def 8;
n
in F by
B,
XXREAL_2:def 6;
then
consider k be
Element of
NAT such that
C: k
= n & ex q be
Polynomial of R st p
= ((
<%(
- a), (
1. R)%>
`^ k)
*' q) by
B;
consider q be
Polynomial of R such that
D: p
= ((
<%(
- a), (
1. R)%>
`^ n)
*' q) by
C;
p
= (((
rpoly (1,a))
`^ n)
*' q) by
D,
repr;
hence ((
rpoly (1,a))
`^ n)
divides p by
RING_4: 1;
F: n is
UpperBound of F by
B,
XXREAL_2:def 3;
now
assume ((
rpoly (1,a))
`^ (n
+ 1))
divides p;
then
consider q be
Polynomial of R such that
E: p
= (((
rpoly (1,a))
`^ (n
+ 1))
*' q) by
RING_4: 1;
p
= ((
<%(
- a), (
1. R)%>
`^ (n
+ 1))
*' q) by
E,
repr;
then (n
+ 1)
in F by
B;
hence contradiction by
F,
XXREAL_2:def 1,
NAT_1: 16;
end;
hence not ((
rpoly (1,a))
`^ (n
+ 1))
divides p;
end;
now
assume
X: ((
rpoly (1,a))
`^ n)
divides p & not ((
rpoly (1,a))
`^ (n
+ 1))
divides p;
set n0 = (
multiplicity (p,a));
consider F be
finite non
empty
Subset of
NAT such that
B: F
= { k where k be
Element of
NAT : ex q be
Polynomial of R st p
= ((
<%(
- a), (
1. R)%>
`^ k)
*' q) } & n0
= (
max F) by
UPROOTS:def 8;
consider q be
Polynomial of R such that
E: p
= (((
rpoly (1,a))
`^ n)
*' q) by
X,
RING_4: 1;
K: n
in
NAT by
ORDINAL1:def 12;
p
= ((
<%(
- a), (
1. R)%>
`^ n)
*' q) by
E,
repr;
then
C: n
in F by
B,
K;
now
let k be
ExtReal;
assume k
in F;
then
consider k0 be
Element of
NAT such that
C: k0
= k & ex q be
Polynomial of R st p
= ((
<%(
- a), (
1. R)%>
`^ k0)
*' q) by
B;
consider q be
Polynomial of R such that
D: p
= ((
<%(
- a), (
1. R)%>
`^ k0)
*' q) by
C;
now
assume k0
>= (n
+ 1);
then
consider j be
Nat such that
E: k0
= ((n
+ 1)
+ j) by
NAT_1: 10;
reconsider j as
Element of
NAT by
ORDINAL1:def 12;
p
= (((
rpoly (1,a))
`^ k0)
*' q) by
D,
repr
.= ((((
rpoly (1,a))
`^ (n
+ 1))
*' ((
rpoly (1,a))
`^ j))
*' q) by
E,
UPROOTS: 30
.= (((
rpoly (1,a))
`^ (n
+ 1))
*' (((
rpoly (1,a))
`^ j)
*' q)) by
POLYNOM3: 33;
hence contradiction by
X,
RING_4: 1;
end;
hence k
<= n by
C,
NAT_1: 13;
end;
hence (
multiplicity (p,a))
= n by
B,
C,
XXREAL_2:def 8;
end;
hence thesis by
A;
end;
theorem ::
RING_5:34
BR5aa: for R be
domRing, a be
Element of R holds (
multiplicity ((
rpoly (1,a)),a))
= 1
proof
let R be
domRing, a be
Element of R;
set p = (
rpoly (1,a));
(p
*' (
1_. R))
= p;
then p
divides p by
RING_4: 1;
then
A: (p
`^ 1)
divides p by
POLYNOM5: 16;
p
<> (
0_. R);
then (
deg (p
*' p))
= ((
deg p)
+ (
deg p)) by
HURWITZ: 23
.= ((
deg p)
+ 1) by
HURWITZ: 27
.= (1
+ 1) by
HURWITZ: 27;
then (
deg (p
*' p))
> 1;
then
B: (
deg (p
*' p))
> (
deg p) by
HURWITZ: 27;
(p
*' p)
= (p
`^ 2) by
POLYNOM5: 17;
then not (p
`^ (1
+ 1))
divides p by
B,
prl25;
hence (
multiplicity (p,a))
= 1 by
A,
multip;
end;
theorem ::
RING_5:35
BR5aaa: for R be
domRing, a,b be
Element of R st b
<> a holds (
multiplicity ((
rpoly (1,a)),b))
=
0
proof
let R be
domRing, a,b be
Element of R;
set p = (
rpoly (1,a));
assume a
<> b;
then not (
rpoly (1,b))
divides (
rpoly (1,a)) by
div100;
hence (
multiplicity (p,b))
=
0 by
multipp0;
end;
theorem ::
RING_5:36
multip1d: for R be
domRing, p be non
zero
Polynomial of R holds for b be non
zero
Element of R, a be
Element of R holds (
multiplicity (p,a))
= (
multiplicity ((b
* p),a))
proof
let F be
domRing, p be non
zero
Polynomial of F;
let b be non
zero
Element of F, a be
Element of F;
set r = (
rpoly (1,a)), np = (
multiplicity (p,a));
(r
`^ np)
divides (b
* p) & not (r
`^ (np
+ 1))
divides p by
multip,
divi1;
then (r
`^ np)
divides (b
* p) & not (r
`^ (np
+ 1))
divides (b
* p) by
divi1ad;
hence thesis by
multip;
end;
BR3: for R be
domRing, a be non
zero
Element of R holds (
support (
BRoots (a
| R)))
=
{}
proof
let R be
domRing, a be non
zero
Element of R;
now
assume
A: (
support (
BRoots (a
| R)))
<>
{} ;
let b be
Element of (
support (
BRoots (a
| R)));
b
in (
Roots (a
| R)) by
A,
UPROOTS:def 9;
hence contradiction;
end;
hence thesis;
end;
theorem ::
RING_5:37
llll: for R be
domRing, p be non
zero
Polynomial of R holds for b be non
zero
Element of R holds (
BRoots (b
* p))
= (
BRoots p)
proof
let F be
domRing, p be non
zero
Polynomial of F;
let b be non
zero
Element of F;
now
let a be
Element of F;
(
multiplicity (p,a))
= (
multiplicity ((b
* p),a)) by
multip1d;
hence ((
BRoots (b
* p))
. a)
= (
multiplicity (p,a)) by
UPROOTS:def 9
.= ((
BRoots p)
. a) by
UPROOTS:def 9;
end;
then for o be
object holds o
in the
carrier of F implies ((
BRoots (b
* p))
. o)
= ((
BRoots p)
. o);
hence thesis by
PBOOLE: 3;
end;
theorem ::
RING_5:38
lemacf1: for R be
domRing, p be non
zero non
with_roots
Polynomial of R holds (
BRoots p)
= (
EmptyBag the
carrier of R)
proof
let R be
domRing, p be non
zero non
with_roots
Polynomial of R;
(
Roots p) is
empty;
then (
support (
BRoots p))
=
{} by
UPROOTS:def 9;
hence thesis by
PRE_POLY: 81;
end;
theorem ::
RING_5:39
bag1: for R be
domRing, a be non
zero
Element of R holds (
card (
BRoots (a
| R)))
=
0
proof
let R be
domRing, a be non
zero
Element of R;
(
support (
BRoots (a
| R)))
=
{} by
BR3;
hence thesis by
bag1a;
end;
theorem ::
RING_5:40
bag2: for R be
domRing, a be
Element of R holds (
card (
BRoots (
rpoly (1,a))))
= 1
proof
let R be
domRing, a be
Element of R;
(
BRoots (
rpoly (1,a)))
= (
BRoots
<%(
- a), (
1. R)%>) by
repr
.= ((
{a},1)
-bag ) by
UPROOTS: 54;
then (
card (
BRoots (
rpoly (1,a))))
= (
card
{a}) by
UPROOTS: 13;
hence thesis by
CARD_1: 30;
end;
theorem ::
RING_5:41
for R be
domRing, p,q be non
zero
Polynomial of R holds (
card (
BRoots (p
*' q)))
= ((
card (
BRoots p))
+ (
card (
BRoots q)))
proof
let R be
domRing, p,q be non
zero
Polynomial of R;
thus (
card (
BRoots (p
*' q)))
= (
card ((
BRoots p)
+ (
BRoots q))) by
UPROOTS: 56
.= ((
card (
BRoots p))
+ (
card (
BRoots q))) by
UPROOTS: 15;
end;
theorem ::
RING_5:42
for R be
domRing, p be non
zero
Polynomial of R holds (
card (
BRoots p))
<= (
deg p)
proof
let R be
domRing, p be non
zero
Polynomial of R;
defpred
P[
Nat] means for p be non
zero
Polynomial of R st (
deg p)
= $1 holds (
card (
BRoots p))
<= (
deg p);
IA:
P[
0 ]
proof
let p be non
zero
Polynomial of R;
assume
A1: (
deg p)
=
0 ;
reconsider q = p as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
consider a be
Element of R such that
A2: q
= (a
| R) by
A1,
RING_4:def 4,
RING_4: 20;
a
<> (
0. R) by
A2;
then
reconsider a as non
zero
Element of R by
STRUCT_0:def 12;
q
= (a
| R) by
A2;
hence (
card (
BRoots p))
<= (
deg p) by
bag1;
end;
IS:
now
let k be
Nat;
assume
IV:
P[k];
now
let p be non
zero
Polynomial of R;
assume
A1: (
deg p)
= (k
+ 1);
per cases ;
suppose ex x be
Element of R st x
is_a_root_of p;
then
consider x be
Element of R such that
A2: x
is_a_root_of p;
consider q be
Polynomial of R such that
A3: p
= ((
rpoly (1,x))
*' q) by
A2,
HURWITZ: 33;
A4: q
<> (
0_. R) by
A3;
reconsider q as non
zero
Polynomial of R by
A3;
(
BRoots p)
= ((
BRoots (
rpoly (1,x)))
+ (
BRoots q)) by
A3,
UPROOTS: 56;
then
A6: (
card (
BRoots p))
= ((
card (
BRoots (
rpoly (1,x))))
+ (
card (
BRoots q))) by
UPROOTS: 15
.= (1
+ (
card (
BRoots q))) by
bag2;
(
deg p)
= ((
deg q)
+ (
deg (
rpoly (1,x)))) by
HURWITZ: 23,
A3,
A4
.= ((
deg q)
+ 1) by
HURWITZ: 27;
hence (
card (
BRoots p))
<= (
deg p) by
IV,
A1,
A6,
XREAL_1: 6;
end;
suppose
A2: not ex x be
Element of R st x
is_a_root_of p;
now
assume
A3: (
Roots p)
<>
{} ;
let x be
Element of (
Roots p);
x
in (
Roots p) by
A3;
then
reconsider x as
Element of R;
x
is_a_root_of p by
A3,
POLYNOM5:def 10;
hence contradiction by
A2;
end;
then (
support (
BRoots p))
=
{} by
UPROOTS:def 9;
hence (
card (
BRoots p))
<= (
deg p) by
bag1a;
end;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
p
<> (
0_. R);
then (
deg p) is
Element of
NAT by
T8;
hence thesis by
I;
end;
begin
Lm10: for L be
unital non
empty
doubleLoopStr holds (((
0_. L)
+* ((
0 ,n)
--> ((
1. L),(
1. L))))
.
0 )
= (
1. L) & (((
0_. L)
+* ((
0 ,n)
--> ((
1. L),(
1. L))))
. n)
= (
1. L)
proof
let L be
unital non
empty
doubleLoopStr;
set t = ((
0_. L)
+* ((
0 ,n)
--> ((
1. L),(
1. L)))), f = ((
0 ,n)
--> ((
1. L),(
1. L)));
A3: (
dom (
0_. L))
=
NAT by
FUNCT_2:def 1;
A4: for u be
object holds u
in
{
0 , n} implies u
in
NAT by
ORDINAL1:def 12;
A7: (
dom f)
=
{
0 , n} by
FUNCT_4: 62;
then
A5: ((
dom (
0_. L))
\/ (
dom f))
=
NAT by
A3,
A4,
TARSKI:def 3,
XBOOLE_1: 12;
n
in (
dom f) & n
in ((
dom (
0_. L))
\/ (
dom f)) by
A5,
A7,
TARSKI:def 2,
ORDINAL1:def 12;
then
A10: (t
. n)
= (f
. n) by
FUNCT_4:def 1
.= (
1. L) by
FUNCT_4: 63;
per cases ;
suppose n
=
0 ;
hence thesis by
A10;
end;
suppose
A6: n
<>
0 ;
0
in (
dom f) by
A7,
TARSKI:def 2;
hence (t
.
0 )
= (f
.
0 ) by
A5,
FUNCT_4:def 1
.= (
1. L) by
A6,
FUNCT_4: 63;
thus thesis by
A10;
end;
end;
Lm11: for L be
unital non
empty
doubleLoopStr, i,n be
Nat st i
<>
0 & i
<> n holds (((
0_. L)
+* ((
0 ,n)
--> ((
1. L),(
1. L))))
. i)
= (
0. L)
proof
let L be
unital non
empty
doubleLoopStr;
let i,n be
Nat;
assume that
A1: i
<>
0 and
A2: i
<> n;
set t = ((
0_. L)
+* ((
0 ,n)
--> ((
1. L),(
1. L)))), f = ((
0 ,n)
--> ((
1. L),(
1. L)));
A3: (
dom (
0_. L))
=
NAT by
FUNCT_2:def 1;
A4: for u be
object holds u
in
{
0 , n} implies u
in
NAT by
ORDINAL1:def 12;
(
dom f)
=
{
0 , n} by
FUNCT_4: 62;
then
A5: ((
dom (
0_. L))
\/ (
dom f))
=
NAT by
A3,
A4,
TARSKI:def 3,
XBOOLE_1: 12;
A6: i
in
NAT by
ORDINAL1:def 12;
not i
in (
dom f) by
A1,
A2,
TARSKI:def 2;
hence (t
. i)
= ((
0_. L)
. i) by
A5,
A6,
FUNCT_4:def 1
.= (
0. L) by
ORDINAL1:def 12,
FUNCOP_1: 7;
end;
definition
let R be
unital non
empty
doubleLoopStr;
let n be
Nat;
::
RING_5:def3
func
npoly (R,n) ->
sequence of R equals ((
0_. R)
+* ((
0 ,n)
--> ((
1. R),(
1. R))));
coherence
proof
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
set f = ((
0 ,n)
--> ((
1. R),(
1. R)));
set q = ((
0_. R)
+* f);
A2: (
dom f)
=
{
0 , n} by
FUNCT_4: 62;
A5:
now
let xx be
object;
assume xx
in
NAT ;
then
reconsider x = xx as
Element of
NAT ;
per cases ;
suppose x
=
0 ;
then (q
. x)
= (
1. R) by
Lm10;
hence (q
. xx)
in the
carrier of R;
end;
suppose x
= n;
then (q
. x)
= (
1. R) by
Lm10;
hence (q
. xx)
in the
carrier of R;
end;
suppose x
<>
0 & x
<> n;
then (q
. x)
= (
0. R) by
Lm11;
hence (q
. xx)
in the
carrier of R;
end;
end;
(
dom (
0_. R))
=
NAT by
FUNCT_2:def 1;
then ((
dom (
0_. R))
\/ (
dom f))
=
NAT by
A2,
XBOOLE_1: 12;
then (
dom q)
=
NAT by
FUNCT_4:def 1;
hence thesis by
A5,
FUNCT_2: 3;
end;
end
registration
let R be
unital non
empty
doubleLoopStr;
let n be
Nat;
cluster (
npoly (R,n)) ->
finite-Support;
coherence
proof
take (n
+ 1);
let i be
Nat;
assume i
>= (n
+ 1);
then i
> n by
NAT_1: 13;
hence thesis by
Lm11;
end;
end
lem6: for R be
unital non
degenerated
doubleLoopStr holds (
deg (
npoly (R,n)))
= n
proof
let R be
unital non
degenerated
doubleLoopStr;
set q = (
npoly (R,n));
A9:
now
let i be
Nat;
assume i
>= (n
+ 1);
then i
<> n & i
<>
0 by
NAT_1: 13;
hence (q
. i)
= (
0. R) by
Lm11;
end;
now
let m be
Nat;
assume
X: m
is_at_least_length_of q;
now
assume
Y: (n
+ 1)
> m;
(q
. n)
= (
1. R) by
Lm10;
hence contradiction by
X,
Y,
NAT_1: 13;
end;
hence (n
+ 1)
<= m;
end;
then (
len q)
= (n
+ 1) by
A9,
ALGSEQ_1:def 3,
ALGSEQ_1:def 2;
then (
deg q)
= ((n
+ 1)
- 1) by
HURWITZ:def 2;
hence thesis;
end;
registration
let R be
unital non
degenerated
doubleLoopStr, n be
Nat;
cluster (
npoly (R,n)) -> non
zero;
coherence
proof
(
deg (
npoly (R,n)))
= n by
lem6;
hence thesis by
HURWITZ: 20;
end;
end
theorem ::
RING_5:43
for R be
unital non
degenerated
doubleLoopStr holds (
deg (
npoly (R,n)))
= n by
lem6;
theorem ::
RING_5:44
for R be
unital non
degenerated
doubleLoopStr holds (
LC (
npoly (R,n)))
= (
1. R)
proof
let R be
unital non
degenerated
doubleLoopStr;
set q = (
npoly (R,n));
A: n
= (
deg q) by
lem6
.= ((
len q)
- 1) by
HURWITZ:def 2;
then (n
+ 1)
= (
len q);
then ((
len q)
-' 1)
= n by
A,
XREAL_1: 233,
NAT_1: 11;
hence thesis by
Lm10;
end;
theorem ::
RING_5:45
lem1e: for R be non
degenerated
Ring, x be
Element of R holds (
eval ((
npoly (R,
0 )),x))
= (
1. R)
proof
let L be non
degenerated
Ring, x be
Element of L;
set q = (
npoly (L,
0 ));
consider F be
FinSequence of L such that
A3: (
eval (q,x))
= (
Sum F) and
A4: (
len F)
= (
len q) and
A5: for n be
Element of
NAT st n
in (
dom F) holds (F
. n)
= ((q
. (n
-' 1))
* ((
power L)
. (x,(n
-' 1)))) by
POLYNOM4:def 2;
0
= (
deg q) by
lem6
.= ((
len q)
- 1) by
HURWITZ:def 2;
then
C: F
=
<*(F
. 1)*> by
A4,
FINSEQ_1: 40;
then (
Seg 1)
= (
dom F) by
FINSEQ_1: 38;
then (F
. 1)
= ((q
. (1
-' 1))
* ((
power L)
. (x,(1
-' 1)))) by
A5,
FINSEQ_1: 3
.= ((q
.
0 )
* ((
power L)
. (x,(1
-' 1)))) by
NAT_2: 8
.= ((q
.
0 )
* ((
power L)
. (x,
0 ))) by
NAT_2: 8
.= ((
1. L)
* ((
power L)
. (x,
0 ))) by
Lm10
.= ((
1. L)
* (
1_ L)) by
GROUP_1:def 7
.= (
1. L);
hence thesis by
A3,
C,
RLVECT_1: 44;
end;
theorem ::
RING_5:46
lem1a: for R be non
degenerated
Ring, n be non
zero
Nat, x be
Element of R holds (
eval ((
npoly (R,n)),x))
= ((x
|^ n)
+ (
1. R))
proof
let R be non
degenerated
Ring, n be non
zero
Nat, x be
Element of R;
set q = (
npoly (R,n));
consider F be
FinSequence of R such that
A3: (
eval (q,x))
= (
Sum F) and
A4: (
len F)
= (
len q) and
A5: for j be
Element of
NAT st j
in (
dom F) holds (F
. j)
= ((q
. (j
-' 1))
* ((
power R)
. (x,(j
-' 1)))) by
POLYNOM4:def 2;
A: n
= (
deg q) by
lem6
.= ((
len q)
- 1) by
HURWITZ:def 2;
then
B: (
len q)
= (n
+ 1);
C: (
dom F)
= (
Seg (n
+ 1)) by
A,
A4,
FINSEQ_1:def 3;
D: 1
<= (n
+ 1) by
NAT_1: 11;
E: ((n
+ 1)
-' 1)
= ((n
+ 1)
- 1) by
NAT_1: 11,
XREAL_1: 233;
B1: (F
. (n
+ 1))
= ((q
. n)
* ((
power R)
. (x,((n
+ 1)
-' 1)))) by
E,
A5,
D,
C,
FINSEQ_1: 1
.= ((
1. R)
* ((
power R)
. (x,((n
+ 1)
-' 1)))) by
Lm10
.= (x
|^ n) by
E;
B2:
now
let j be
Element of
NAT ;
assume
H0: 1
< j & j
<= n;
reconsider j1 = (j
-' 1) as
Element of
NAT ;
reconsider n1 = (n
- 1) as
Element of
NAT by
INT_1: 3;
n
<= (n
+ 1) by
NAT_1: 11;
then
H1: j
<= (n
+ 1) by
H0,
XXREAL_0: 2;
H4: j1
= (j
- 1) by
H0,
XREAL_1: 233;
then
H2: j1
<>
0 by
H0;
(j1
+ 1)
<= (n1
+ 1) by
H4,
H0;
then
H3: j1
<> n by
NAT_1: 13;
thus (F
. j)
= ((q
. j1)
* ((
power R)
. (x,(j
-' 1)))) by
A5,
H1,
C,
H0,
FINSEQ_1: 1
.= ((
0. R)
* ((
power R)
. (x,(j
-' 1)))) by
H2,
H3,
Lm11
.= (
0. R);
end;
B3: (F
. 1)
= ((q
. (1
-' 1))
* ((
power R)
. (x,(1
-' 1)))) by
A5,
C,
D,
FINSEQ_1: 1
.= ((q
.
0 )
* ((
power R)
. (x,(1
-' 1)))) by
NAT_2: 8
.= ((q
.
0 )
* ((
power R)
. (x,
0 ))) by
NAT_2: 8
.= ((
1. R)
* ((
power R)
. (x,
0 ))) by
Lm10
.= ((
1. R)
* (
1_ R)) by
GROUP_1:def 7
.= (
1. R);
B4: (
len F)
<>
0 by
A,
A4;
consider fp be
sequence of the
carrier of R such that
A6: (
Sum F)
= (fp
. (
len F)) and
A7: (fp
.
0 )
= (
0. R) and
A8: for j be
Nat, v be
Element of R st j
< (
len F) & v
= (F
. (j
+ 1)) holds (fp
. (j
+ 1))
= ((fp
. j)
+ v) by
RLVECT_1:def 12;
defpred
P[
Element of
NAT ] means ($1
=
0 & (fp
. $1)
= (
0. R)) or (
0
< $1 & $1
< (
len F) & (fp
. $1)
= (
1. R)) or ($1
= (
len F) & (fp
. $1)
= ((x
|^ n)
+ (
1. R)));
IA:
P[
0 ] by
A7;
IS:
now
let j be
Element of
NAT ;
assume
C1:
0
<= j & j
< (
len F);
assume
C2:
P[j];
per cases ;
suppose
D1: j
=
0 & j
< ((
len F)
- 1);
then
D2: (fp
. (j
+ 1))
= ((fp
.
0 )
+ (
1. R)) by
B3,
A8,
C1
.= (
1. R) by
A7;
(j
+ 1)
< (((
len F)
- 1)
+ 1) by
D1,
XREAL_1: 6;
hence
P[(j
+ 1)] by
D2;
end;
suppose j
=
0 & j
>= ((
len F)
- 1);
hence
P[(j
+ 1)] by
A,
A4;
end;
suppose
D1:
0
< j & j
< ((
len F)
- 1);
then
D3: (j
+ 1)
<= n by
A,
A4,
INT_1: 7;
(j
+ 1)
> (
0
+ 1) by
D1,
XREAL_1: 8;
then (F
. (j
+ 1))
= (
0. R) by
D3,
B2;
then (fp
. (j
+ 1))
= ((
1. R)
+ (
0. R)) by
C2,
D1,
C1,
A8;
hence
P[(j
+ 1)] by
D3,
B,
A4,
XXREAL_0: 2,
NAT_1: 16;
end;
suppose
D1:
0
< j & j
>= ((
len F)
- 1);
(j
+ 1)
<= (
len F) by
INT_1: 7,
C1;
then ((j
+ 1)
- 1)
<= ((
len F)
- 1) by
XREAL_1: 9;
then
D3: j
= n by
A4,
A,
D1,
XXREAL_0: 1;
then (fp
. (j
+ 1))
= ((
1. R)
+ (x
|^ n)) by
B1,
C1,
C2,
A8
.= ((x
|^ n)
+ (
1. R)) by
RLVECT_1:def 2;
hence
P[(j
+ 1)] by
D3,
A4,
A;
end;
end;
I: for j be
Element of
NAT st
0
<= j & j
<= (
len F) holds
P[j] from
INT_1:sch 7(
IA,
IS);
thus (
eval (q,x))
= ((x
|^ n)
+ (
1. R)) by
I,
A6,
A3,
B4;
end;
theorem ::
RING_5:47
lem1: for n be
even
Nat, x be
Element of
F_Real holds (
eval ((
npoly (
F_Real ,n)),x))
> (
0.
F_Real )
proof
let n be
even
Nat, x be
Element of
F_Real ;
per cases ;
suppose n
=
0 ;
hence thesis by
lem1e;
end;
suppose
S: n is non
zero;
((x
|^ n)
+ 1)
>= ((
0.
F_Real )
+ 1) by
XX,
XREAL_1: 6;
then ((x
|^ n)
+ (
1.
F_Real ))
>= 1;
hence thesis by
lem1a,
S;
end;
end;
theorem ::
RING_5:48
lem1c: for n be
odd
Nat holds (
eval ((
npoly (
F_Real ,n)),(
- (
1.
F_Real ))))
= (
0.
F_Real )
proof
let n be
odd
Nat;
consider k be
Nat such that
H: (n
- 1)
= (2
* k) by
ABIAN:def 2;
A: k is
Element of
NAT by
ORDINAL1:def 12;
((
- (
1.
F_Real ))
|^ n)
= ((
power
F_Real )
. ((
- (
1.
F_Real )),((2
* k)
+ 1))) by
H
.= (
- (
1_
F_Real )) by
A,
HURWITZ: 4
.= (
- (
1.
F_Real ));
hence (
eval ((
npoly (
F_Real ,n)),(
- (
1.
F_Real ))))
= ((
- (
1.
F_Real ))
+ (
1.
F_Real )) by
lem1a
.= (
0.
F_Real );
end;
theorem ::
RING_5:49
lem1b: (
eval ((
npoly ((
Z/ 2),2)),(
1. (
Z/ 2))))
= (
0. (
Z/ 2))
proof
(
Char (
Z/ 2))
= 2 by
RING_3:def 6;
then
A: (2
'*' (
1. (
Z/ 2)))
= (
0. (
Z/ 2)) by
RING_3:def 5;
thus (
eval ((
npoly ((
Z/ 2),2)),(
1. (
Z/ 2))))
= (((
1. (
Z/ 2))
|^ 2)
+ (
1. (
Z/ 2))) by
lem1a
.= (((
1. (
Z/ 2))
* (
1. (
Z/ 2)))
+ (
1. (
Z/ 2))) by
prl4
.= (
0. (
Z/ 2)) by
A,
prl3;
end;
registration
let n be
even
Nat;
cluster (
npoly (
F_Real ,n)) -> non
with_roots;
coherence
proof
set q = (
npoly (
F_Real ,n));
now
assume q is
with_roots;
then
consider r be
Element of
F_Real such that
H: r
is_a_root_of q by
POLYNOM5:def 8;
(
eval (q,r))
= (
0.
F_Real ) by
H,
POLYNOM5:def 7;
hence contradiction by
lem1;
end;
hence thesis;
end;
end
registration
let n be
odd
Nat;
cluster (
npoly (
F_Real ,n)) ->
with_roots;
coherence
proof
(
eval ((
npoly (
F_Real ,n)),(
- (
1.
F_Real ))))
= (
0.
F_Real ) by
lem1c;
hence thesis by
POLYNOM5:def 8,
POLYNOM5:def 7;
end;
end
registration
cluster (
npoly ((
Z/ 2),2)) ->
with_roots;
coherence by
POLYNOM5:def 7,
POLYNOM5:def 8,
lem1b;
end
begin
definition
let R be
Ring;
::
RING_5:def4
mode
Ppoly of R ->
Polynomial of R means
:
dpp1: ex F be non
empty
FinSequence of (
Polynom-Ring R) st it
= (
Product F) & for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a));
existence
proof
reconsider p = (
rpoly (1,(
1. R))) as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
set F =
<*p*>;
reconsider q = (
Product F) as
Polynomial of R by
POLYNOM3:def 10;
A:
now
let i be
Nat;
assume
AS: i
in (
dom F);
(
dom F)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1: 38;
then i
= 1 by
AS,
TARSKI:def 1;
hence ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
FINSEQ_1: 40;
end;
take q, F;
thus thesis by
A;
end;
end
lemppoly: for R be
domRing, F be non
empty
FinSequence of (
Polynom-Ring R), p be
Polynomial of R st p
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a))) holds (
deg p)
= (
len F)
proof
let R be
domRing, F be non
empty
FinSequence of (
Polynom-Ring R), p be
Polynomial of R;
assume
AS: p
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)));
defpred
P[
Nat] means for F be non
empty
FinSequence of (
Polynom-Ring R) holds for p be
Polynomial of R st (
len F)
= $1 & p
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a))) holds (
deg p)
= (
len F);
IA:
P[
0 ];
IS:
now
let k be
Nat;
assume
IV:
P[k];
per cases ;
suppose
S: k
=
0 ;
now
let F be non
empty
FinSequence of (
Polynom-Ring R), p be
Polynomial of R;
assume
A: (
len F)
= 1 & p
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)));
then 1
in (
Seg (
len F)) by
FINSEQ_1: 1;
then 1
in (
dom F) by
FINSEQ_1:def 3;
then
consider a be
Element of R such that
A0: (F
. 1)
= (
rpoly (1,a)) by
A;
reconsider q = (
rpoly (1,a)) as
Element of (
Polynom-Ring R) by
POLYNOM3:def 10;
F
=
<*q*> by
A0,
A,
FINSEQ_1: 40;
then q
= p by
A,
GROUP_4: 9;
hence (
deg p)
= 1 by
HURWITZ: 27;
end;
hence
P[(k
+ 1)] by
S;
end;
suppose
S: k
>
0 ;
now
let F be non
empty
FinSequence of (
Polynom-Ring R), p be
Polynomial of R;
assume
A: (
len F)
= (k
+ 1) & p
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)));
consider G be
FinSequence, y be
object such that
B2: F
= (G
^
<*y*>) by
FINSEQ_1: 46;
B2a: (
rng G)
c= (
rng F) by
B2,
FINSEQ_1: 29;
B2b: (
rng F)
c= the
carrier of (
Polynom-Ring R) by
FINSEQ_1:def 4;
then
reconsider G as
FinSequence of (
Polynom-Ring R) by
B2a,
XBOOLE_1: 1,
FINSEQ_1:def 4;
reconsider q = (
Product G) as
Polynomial of R by
POLYNOM3:def 10;
B3: (
len F)
= ((
len G)
+ (
len
<*y*>)) by
B2,
FINSEQ_1: 22
.= ((
len G)
+ 1) by
FINSEQ_1: 39;
then
reconsider G as non
empty
FinSequence of (
Polynom-Ring R) by
S,
A;
C: (
dom G)
c= (
dom F) by
B2,
FINSEQ_1: 26;
now
let i be
Nat;
assume
C0: i
in (
dom G);
then (G
. i)
= (F
. i) by
B2,
FINSEQ_1:def 7;
hence ex a be
Element of R st (G
. i)
= (
rpoly (1,a)) by
C,
C0,
A;
end;
then
F: (
deg q)
= k by
IV,
B3,
A;
(
rng
<*y*>)
=
{y} by
FINSEQ_1: 39;
then
G5: y
in (
rng
<*y*>) by
TARSKI:def 1;
(
rng
<*y*>)
c= (
rng F) by
B2,
FINSEQ_1: 30;
then y
in (
rng F) by
G5;
then
reconsider y as
Element of (
Polynom-Ring R) by
B2b;
(
dom
<*y*>)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1:def 8;
then 1
in (
dom
<*y*>) by
TARSKI:def 1;
then
B6: (F
. (k
+ 1))
= (
<*y*>
. 1) by
B2,
B3,
A,
FINSEQ_1:def 7
.= y by
FINSEQ_1:def 8;
(
dom F)
= (
Seg (k
+ 1)) by
A,
FINSEQ_1:def 3;
then
consider a be
Element of R such that
B9: y
= (
rpoly (1,a)) by
A,
B6,
FINSEQ_1: 4;
B10: p
= ((
Product G)
* y) by
A,
B2,
GROUP_4: 6
.= (q
*' (
rpoly (1,a))) by
B9,
POLYNOM3:def 10;
q
<> (
0_. R) & (
rpoly (1,a))
<> (
0_. R) by
F,
HURWITZ: 20;
hence (
deg p)
= ((
deg q)
+ (
deg (
rpoly (1,a)))) by
B10,
HURWITZ: 23
.= (k
+ 1) by
F,
HURWITZ: 27;
end;
hence
P[(k
+ 1)];
end;
end;
I: for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
thus thesis by
I,
AS;
end;
cc2: for R be
domRing, p be
Ppoly of R holds (
LC p)
= (
1. R)
proof
let R be
domRing, p be
Ppoly of R;
defpred
P[
Nat] means for q be
Polynomial of R holds for F be non
empty
FinSequence of (
Polynom-Ring R) st (
len F)
= $1 & q
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a))) holds (
LC q)
= (
1. R);
IA:
P[
0 ];
IS:
now
let k be
Nat;
assume
IV:
P[k];
now
let q be
Polynomial of R;
let F be non
empty
FinSequence of (
Polynom-Ring R);
assume
AS: (
len F)
= (k
+ 1) & q
= (
Product F) & (for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)));
then
consider G be
FinSequence of (
Polynom-Ring R), x be
Element of (
Polynom-Ring R) such that
A1: F
= (G
^
<*x*>) by
FINSEQ_2: 19;
reconsider p = (
Product G) as
Polynomial of R by
POLYNOM3:def 10;
A4: (
len F)
= ((
len G)
+ 1) by
A1,
FINSEQ_2: 16;
A5: x
= (F
. (
len F)) by
A1,
A4,
FINSEQ_1: 42;
(
len F)
in (
Seg (
len F)) by
FINSEQ_1: 3;
then (
len F)
in (
dom F) by
FINSEQ_1:def 3;
then
consider a be
Element of R such that
A2: x
= (
rpoly (1,a)) by
AS,
A5;
per cases ;
suppose G
=
{} ;
then F
=
<*x*> by
A1,
FINSEQ_1: 34;
then (
Product F)
= (
rpoly (1,a)) by
A2,
GROUP_4: 9;
hence (
LC q)
= (
1. R) by
AS,
lcrpol;
end;
suppose
B1: G is non
empty;
B2:
now
let i be
Nat;
assume
C1: i
in (
dom G);
C2: (
dom G)
c= (
dom F) by
A1,
FINSEQ_1: 26;
(G
. i)
= (F
. i) by
A1,
C1,
FINSEQ_1:def 7;
hence ex a be
Element of R st (G
. i)
= (
rpoly (1,a)) by
C1,
C2,
AS;
end;
(
deg p)
= (
len G) by
B1,
B2,
lemppoly;
then p
<> (
0_. R) by
HURWITZ: 20;
then
reconsider p as non
zero
Polynomial of R by
UPROOTS:def 5;
(
Product F)
= ((
Product G)
* (
Product
<*x*>)) by
A1,
GROUP_4: 5
.= ((
Product G)
* x) by
GROUP_4: 9
.= (p
*' (
rpoly (1,a))) by
A2,
POLYNOM3:def 10;
hence (
LC q)
= ((
LC p)
* (
LC (
rpoly (1,a)))) by
AS,
NIVEN: 46
.= ((
LC p)
* (
1. R)) by
lcrpol
.= (
1. R) by
AS,
A4,
B1,
B2,
IV;
end;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat holds
P[k] from
NAT_1:sch 2(
IA,
IS);
consider F be non
empty
FinSequence of (
Polynom-Ring R) such that
H: p
= (
Product F) & for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
dpp1;
consider k be
Nat such that
J: (
len F)
= k;
thus thesis by
H,
I,
J;
end;
registration
let R be
domRing;
cluster -> non
constant
monic
with_roots for
Ppoly of R;
coherence
proof
let p be
Ppoly of R;
consider F be non
empty
FinSequence of (
Polynom-Ring R) such that
H: p
= (
Product F) & for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
dpp1;
A0: (
len F)
>= (1
+
0 ) by
NAT_1: 13;
hence p is non
constant by
H,
lemppoly;
thus p is
monic by
cc2;
consider G be
FinSequence of (
Polynom-Ring R), x be
Element of (
Polynom-Ring R) such that
A1: F
= (G
^
<*x*>) by
A0,
FINSEQ_2: 19;
A3: (F
. ((
len G)
+ 1))
= x by
A1,
FINSEQ_1: 42;
A4: (
len F)
= ((
len G)
+ (
len
<*x*>)) by
A1,
FINSEQ_1: 22
.= ((
len G)
+ 1) by
FINSEQ_1: 40;
(
len F)
in (
Seg (
len F)) by
FINSEQ_1: 3;
then (
len F)
in (
dom F) by
FINSEQ_1:def 3;
then
consider a be
Element of R such that
A2: x
= (
rpoly (1,a)) by
H,
A3,
A4;
reconsider q = (
Product G) as
Polynomial of R by
POLYNOM3:def 10;
p
= ((
Product G)
* x) by
H,
A1,
GROUP_4: 6
.= (q
*' (
rpoly (1,a))) by
A2,
POLYNOM3:def 10;
hence p is
with_roots;
end;
end
theorem ::
RING_5:50
for R be
domRing, p be
Ppoly of R holds (
LC p)
= (
1. R) by
cc2;
theorem ::
RING_5:51
lemppoly1: for R be
domRing, a be
Element of R holds (
rpoly (1,a)) is
Ppoly of R
proof
let R be
domRing, a be
Element of R;
reconsider p = (
rpoly (1,a)) as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
set F =
<*p*>;
A:
now
let i be
Nat;
assume
AS: i
in (
dom F);
(
dom F)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1: 38;
then i
= 1 by
AS,
TARSKI:def 1;
hence ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
FINSEQ_1: 40;
end;
(
Product F)
= p by
GROUP_4: 9;
hence thesis by
A,
dpp1;
end;
theorem ::
RING_5:52
lemppoly3: for R be
domRing, p,q be
Ppoly of R holds (p
*' q) is
Ppoly of R
proof
let R be
domRing, p,q be
Ppoly of R;
consider Fp be non
empty
FinSequence of (
Polynom-Ring R) such that
B0: p
= (
Product Fp) & for i be
Nat st i
in (
dom Fp) holds ex a be
Element of R st (Fp
. i)
= (
rpoly (1,a)) by
dpp1;
consider Fq be non
empty
FinSequence of (
Polynom-Ring R) such that
B1: q
= (
Product Fq) & for i be
Nat st i
in (
dom Fq) holds ex a be
Element of R st (Fq
. i)
= (
rpoly (1,a)) by
dpp1;
set G = (Fp
^ Fq);
A:
now
let i be
Nat;
assume
AS: i
in (
dom G);
per cases by
AS,
FINSEQ_1: 25;
suppose
B2: i
in (
dom Fp);
then (Fp
. i)
= (G
. i) by
FINSEQ_1:def 7;
hence ex a be
Element of R st (G
. i)
= (
rpoly (1,a)) by
B0,
B2;
end;
suppose ex n be
Nat st n
in (
dom Fq) & i
= ((
len Fp)
+ n);
then
consider n be
Nat such that
B2: n
in (
dom Fq) & i
= ((
len Fp)
+ n);
(G
. i)
= (Fq
. n) by
B2,
FINSEQ_1:def 7;
hence ex a be
Element of R st (G
. i)
= (
rpoly (1,a)) by
B1,
B2;
end;
end;
(
Product G)
= ((
Product Fp)
* (
Product Fq)) by
GROUP_4: 5
.= (p
*' q) by
B0,
B1,
POLYNOM3:def 10;
hence thesis by
A,
dpp1;
end;
lempolybag1: for R be
domRing, a be
Element of R holds for F be non
empty
FinSequence of (
Polynom-Ring R) st (for k be
Nat st k
in (
dom F) holds (F
. k)
= (
rpoly (1,a))) holds for p be
Polynomial of R st p
= (
Product F) holds p
= ((
rpoly (1,a))
`^ (
len F)) & (
Roots p)
=
{a}
proof
let R be
domRing, a be
Element of R, F be non
empty
FinSequence of (
Polynom-Ring R);
assume
AS1: for k be
Nat st k
in (
dom F) holds (F
. k)
= (
rpoly (1,a));
let p be
Polynomial of R;
assume
AS2: p
= (
Product F);
defpred
P[
Nat] means for F be
FinSequence of (
Polynom-Ring R) st (
len F)
= $1 & for k be
Nat st k
in (
dom F) holds (F
. k)
= (
rpoly (1,a)) holds for p be
Polynomial of R st p
= (
Product F) holds p
= ((
rpoly (1,a))
`^ (
len F)) & (
Roots p)
=
{a};
IA:
P[1]
proof
now
let F be
FinSequence of (
Polynom-Ring R);
assume
AS1: (
len F)
= 1 & for k be
Nat st k
in (
dom F) holds (F
. k)
= (
rpoly (1,a));
let p be
Polynomial of R;
assume
AS2: p
= (
Product F);
B: F
=
<*(F
. 1)*> by
AS1,
FINSEQ_1: 40;
then
A: (
dom F)
= (
Seg 1) by
FINSEQ_1: 38;
then
C: (F
. 1)
in (
rng F) by
FUNCT_1: 3,
FINSEQ_1: 3;
(
rng F)
c= the
carrier of (
Polynom-Ring R) by
FINSEQ_1:def 4;
then
reconsider x = (F
. 1) as
Element of the
carrier of (
Polynom-Ring R) by
C;
thus p
= x by
AS2,
B,
GROUP_4: 9
.= (
rpoly (1,a)) by
A,
AS1,
FINSEQ_1: 3
.= ((
rpoly (1,a))
`^ (
len F)) by
AS1,
POLYNOM5: 16;
then p
= (
rpoly (1,a)) by
AS1,
POLYNOM5: 16;
hence (
Roots p)
=
{a} by
ro4;
end;
hence thesis;
end;
IS:
now
let k be
Nat;
assume 1
<= k;
assume
IV:
P[k];
now
let F be
FinSequence of (
Polynom-Ring R);
assume
AS1: (
len F)
= (k
+ 1) & for i be
Nat st i
in (
dom F) holds (F
. i)
= (
rpoly (1,a));
let p be
Polynomial of R;
assume
AS2: p
= (
Product F);
consider G be
FinSequence of (
Polynom-Ring R), x be
Element of (
Polynom-Ring R) such that
A1: F
= (G
^
<*x*>) by
AS1,
FINSEQ_2: 19;
A3: (F
. ((
len G)
+ 1))
= x by
A1,
FINSEQ_1: 42;
A4: (
len F)
= ((
len G)
+ (
len
<*x*>)) by
A1,
FINSEQ_1: 22
.= ((
len G)
+ 1) by
FINSEQ_1: 40;
(
len F)
in (
Seg (
len F)) by
AS1,
FINSEQ_1: 3;
then (
len F)
in (
dom F) by
FINSEQ_1:def 3;
then
A2: x
= (
rpoly (1,a)) by
AS1,
A3,
A4;
reconsider q = (
Product G) as
Polynomial of R by
POLYNOM3:def 10;
now
let i be
Nat;
assume
A6: i
in (
dom G);
A7: (
dom G)
c= (
dom F) by
A1,
FINSEQ_1: 26;
thus (G
. i)
= (F
. i) by
A1,
A6,
FINSEQ_1:def 7
.= (
rpoly (1,a)) by
AS1,
A7,
A6;
end;
then
A6: q
= ((
rpoly (1,a))
`^ (
len G)) & (
Roots q)
=
{a} by
AS1,
A4,
IV;
A7: p
= ((
Product G)
* x) by
AS2,
A1,
GROUP_4: 6
.= (q
*' (
rpoly (1,a))) by
A2,
POLYNOM3:def 10;
hence p
= ((
rpoly (1,a))
`^ (
len F)) by
A4,
A6,
POLYNOM5: 19;
thus (
Roots p)
= ((
Roots q)
\/ (
Roots (
rpoly (1,a)))) by
A7,
UPROOTS: 23
.= (
{a}
\/
{a}) by
A6,
ro4
.=
{a};
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat st k
>= 1 holds
P[k] from
NAT_1:sch 8(
IA,
IS);
(
len F)
>= 1 by
FINSEQ_1: 20;
hence thesis by
I,
AS1,
AS2;
end;
lempolybag: for R be
domRing, B be
bag of the
carrier of R st (
card (
support B))
= 1 holds ex p be
Ppoly of R st (
deg p)
= (
card B) & for a be
Element of R holds (
multiplicity (p,a))
= (B
. a)
proof
let R be
domRing, B be
bag of the
carrier of R;
assume (
card (
support B))
= 1;
then
consider x be
object such that
A1: (
support B)
=
{x} by
CARD_2: 42;
x
in (
support B) by
A1,
TARSKI:def 1;
then
reconsider a = x as
Element of the
carrier of R;
reconsider q = (
rpoly (1,a)) as
Element of (
Polynom-Ring R) by
POLYNOM3:def 10;
deffunc
f(
set) = q;
consider F be
FinSequence of (
Polynom-Ring R) such that
A2: (
len F)
= (B
. a) & for k be
Nat st k
in (
dom F) holds (F
. k)
=
f(k) from
FINSEQ_2:sch 1;
reconsider F as non
empty
FinSequence of (
Polynom-Ring R) by
A1,
A2,
bb7;
reconsider p = (
Product F) as
Polynomial of R by
POLYNOM3:def 10;
AS: B
= ((
{a},(B
. a))
-bag ) by
A1,
bb7;
A3: for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
A2;
then
reconsider p as
Ppoly of R by
dpp1;
take p;
thus (
deg p)
= (B
. a) by
A2,
A3,
lemppoly
.= (
card B) by
AS,
bb4;
A5: ((
rpoly (1,a))
`^ (B
. a))
= p by
lempolybag1,
A2;
now
let o be
Element of R;
per cases ;
suppose
C: o
= a;
((
rpoly (1,a))
`^ (B
. a))
= (((
rpoly (1,a))
`^ (B
. a))
*' (
1_. R));
then
B: ((
rpoly (1,a))
`^ (B
. a))
divides p by
A5,
RING_4: 1;
E: ((
rpoly (1,a))
`^ (B
. a))
<> (
0_. R);
((
rpoly (1,a))
`^ ((B
. a)
+ 1))
= (((
rpoly (1,a))
`^ (B
. a))
*' (
rpoly (1,a))) by
POLYNOM5: 19;
then (
deg ((
rpoly (1,a))
`^ ((B
. a)
+ 1)))
= ((
deg ((
rpoly (1,a))
`^ (B
. a)))
+ (
deg (
rpoly (1,a)))) by
E,
HURWITZ: 23
.= ((
deg ((
rpoly (1,a))
`^ (B
. a)))
+ 1) by
HURWITZ: 27;
then (
deg ((
rpoly (1,a))
`^ ((B
. a)
+ 1)))
> (
deg ((
rpoly (1,a))
`^ (B
. a))) by
XREAL_1: 29;
hence (
multiplicity (p,o))
= (B
. o) by
C,
B,
A5,
prl25,
multip;
end;
suppose
C: o
<> a;
then
C1: not o
in (
support B) by
A1,
TARSKI:def 1;
((
rpoly (1,o))
`^
0 )
= (
1_. R) by
POLYNOM5: 15;
then
B: (((
rpoly (1,o))
`^
0 )
*' p)
= p;
now
assume ((
rpoly (1,o))
`^ (
0
+ 1))
divides p;
then (
rpoly (1,o))
divides p by
POLYNOM5: 16;
then (
eval (p,o))
= (
0. R) by
Th9;
then o
is_a_root_of p by
POLYNOM5:def 7;
then o
in (
Roots p) by
POLYNOM5:def 10;
then o
in
{a} by
lempolybag1,
A2;
hence contradiction by
C,
TARSKI:def 1;
end;
hence (
multiplicity (p,o))
=
0 by
B,
multip,
RING_4: 1
.= (B
. o) by
C1,
PRE_POLY:def 7;
end;
end;
hence thesis;
end;
definition
let R be
domRing;
let B be non
zero
bag of the
carrier of R;
::
RING_5:def5
mode
Ppoly of R,B ->
Ppoly of R means
:
dpp: (
deg it )
= (
card B) & for a be
Element of R holds (
multiplicity (it ,a))
= (B
. a);
existence
proof
defpred
P[
Nat] means for B be non
zero
bag of the
carrier of R st (
card (
support B))
= $1 holds ex p be
Ppoly of R st (
deg p)
= (
card B) & for a be
Element of R holds (
multiplicity (p,a))
= (B
. a);
IA:
P[1] by
lempolybag;
IS:
now
let k be
Nat;
assume
AS: 1
<= k;
assume
IV:
P[k];
now
let B be non
zero
bag of the
carrier of R;
assume
X: (
card (
support B))
= (k
+ 1);
now
assume
A: not ex x be
Element of R st x
in (
support B);
let o be
Element of (
support B);
now
assume (
support B)
<>
{} ;
then o
in (
support B);
hence contradiction by
A;
end;
hence contradiction by
X;
end;
then
consider x be
Element of R such that
A: x
in (
support B);
H1: for o be
object holds o
in
{x} implies o
in (
support B) by
A,
TARSKI:def 1;
set b = ((
{x},(B
. x))
-bag ), b1 = (B
\ x);
(B
. x)
<>
0 by
A,
PRE_POLY:def 7;
then (
support b)
=
{x} by
UPROOTS: 8;
then (
card (
support b))
= 1 by
CARD_1: 30;
then
consider p1 be
Ppoly of R such that
A1: (
deg p1)
= (
card b) & for a be
Element of R holds (
multiplicity (p1,a))
= (b
. a) by
lempolybag;
A3: (
card (
support b1))
= (
card ((
support B)
\
{x})) by
bb3a
.= ((
card (
support B))
- (
card
{x})) by
TARSKI:def 3,
H1,
CARD_2: 44
.= ((
card (
support B))
- 1) by
CARD_1: 30;
then (
support b1)
<>
{} by
X,
AS;
then
reconsider b1 as non
zero
bag of the
carrier of R by
bbag;
consider p2 be
Ppoly of R such that
A5: (
deg p2)
= (
card b1) & for a be
Element of R holds (
multiplicity (p2,a))
= (b1
. a) by
A3,
X,
IV;
reconsider q = (p1
*' p2) as
Ppoly of R by
lemppoly3;
p1
<> (
0_. R) & p2
<> (
0_. R);
then
A2: (
deg q)
= ((
deg p1)
+ (
deg p2)) by
HURWITZ: 23
.= (
card (b
+ b1)) by
A1,
A5,
UPROOTS: 15
.= (
card B) by
bb3;
now
let a be
Element of R;
thus (
multiplicity (q,a))
= ((
multiplicity (p1,a))
+ (
multiplicity (p2,a))) by
UPROOTS: 55
.= ((b
. a)
+ (
multiplicity (p2,a))) by
A1
.= ((b
. a)
+ (b1
. a)) by
A5
.= ((b
+ b1)
. a) by
PRE_POLY:def 5
.= (B
. a) by
bb3;
end;
hence ex p be
Ppoly of R st (
deg p)
= (
card B) & for a be
Element of R holds (
multiplicity (p,a))
= (B
. a) by
A2;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat st 1
<= k holds
P[k] from
NAT_1:sch 8(
IA,
IS);
consider n be
Nat such that
H: (
card (
support B))
= n;
now
assume n
=
0 ;
then (
support B)
=
{} by
H;
hence contradiction by
bbag;
end;
then (n
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then 1
<= n by
NAT_1: 13;
hence thesis by
H,
I;
end;
end
theorem ::
RING_5:53
for R be
domRing, B be non
zero
bag of the
carrier of R, p be
Ppoly of R, B holds for a be
Element of R st a
in (
support B) holds (
eval (p,a))
= (
0. R)
proof
let R be
domRing, F be non
zero
bag of the
carrier of R, p be
Ppoly of R, F;
let a be
Element of R;
assume a
in (
support F);
then (F
. a)
<>
0 by
PRE_POLY:def 7;
then ((F
. a)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
then (F
. a)
>= 1 by
NAT_1: 13;
then (
multiplicity (p,a))
>= 1 by
dpp;
then
consider s be
Polynomial of R such that
A: p
= ((
rpoly (1,a))
*' s) by
HURWITZ: 33,
UPROOTS: 52;
thus thesis by
A,
RING_4: 1,
Th9;
end;
theorem ::
RING_5:54
pf1: for R be
domRing, B be non
zero
bag of the
carrier of R, p be
Ppoly of R, B holds for a be
Element of R holds ((
rpoly (1,a))
`^ (B
. a))
divides p & not ((
rpoly (1,a))
`^ ((B
. a)
+ 1))
divides p
proof
let R be
domRing, F be non
zero
bag of the
carrier of R, p be
Ppoly of R, F;
let a be
Element of R;
(
multiplicity (p,a))
= (F
. a) by
dpp;
hence thesis by
multip;
end;
theorem ::
RING_5:55
pf2: for R be
domRing, B be non
zero
bag of the
carrier of R, p be
Ppoly of R, B holds (
BRoots p)
= B
proof
let R be
domRing, B be non
zero
bag of the
carrier of R, p be
Ppoly of R, B;
set b = (
BRoots p);
now
let o be
object;
assume o
in the
carrier of R;
then
reconsider a = o as
Element of the
carrier of R;
(B
. a)
= (
multiplicity (p,a)) by
dpp
.= (b
. a) by
UPROOTS:def 9;
hence (b
. o)
= (B
. o);
end;
hence thesis by
PBOOLE: 3;
end;
theorem ::
RING_5:56
lemacf5: for R be
domRing, B be non
zero
bag of the
carrier of R holds for p be
Ppoly of R, B holds (
deg p)
= (
card (
BRoots p))
proof
let R be
domRing, B be non
zero
bag of the
carrier of R;
let p be
Ppoly of R, B;
thus (
card (
BRoots p))
= (
card B) by
pf2
.= (
deg p) by
dpp;
end;
theorem ::
RING_5:57
lemacf: for R be
domRing, a be
Element of R holds (
rpoly (1,a)) is
Ppoly of R, (
Bag
{a})
proof
let R be
domRing, a be
Element of R;
reconsider p = (
rpoly (1,a)) as
Ppoly of R by
lemppoly1;
A: (
deg p)
= 1 by
HURWITZ: 27
.= (
card
{a}) by
CARD_1: 30
.= (
card ((
{a},1)
-bag )) by
UPROOTS: 13;
now
let c be
Element of R;
per cases ;
suppose
B: c
= a;
then
C: c
in
{a} by
TARSKI:def 1;
thus (
multiplicity (p,c))
= 1 by
B,
BR5aa
.= ((
Bag
{a})
. c) by
C,
UPROOTS: 7;
end;
suppose
B: c
<> a;
then
C: not c
in
{a} by
TARSKI:def 1;
thus (
multiplicity (p,c))
=
0 by
B,
BR5aaa
.= ((
Bag
{a})
. c) by
C,
UPROOTS: 6;
end;
end;
hence thesis by
A,
dpp;
end;
theorem ::
RING_5:58
lemacf2: for R be
domRing, B1,B2 be non
zero
bag of the
carrier of R holds for p be
Ppoly of R, B1, q be
Ppoly of R, B2 holds (p
*' q) is
Ppoly of R, (B1
+ B2)
proof
let R be
domRing, B1,B2 be non
zero
bag of the
carrier of R;
set B = (B1
+ B2);
let p be
Ppoly of R, B1, q be
Ppoly of R, B2;
reconsider r = (p
*' q) as
Ppoly of R by
lemppoly3;
p
<> (
0_. R) & q
<> (
0_. R);
then
A: (
deg r)
= ((
deg p)
+ (
deg q)) by
HURWITZ: 23
.= ((
card (
BRoots p))
+ (
deg q)) by
lemacf5
.= ((
card B1)
+ (
deg q)) by
pf2
.= ((
card B1)
+ (
card (
BRoots q))) by
lemacf5
.= ((
card B1)
+ (
card B2)) by
pf2
.= (
card B) by
UPROOTS: 15;
now
let c be
Element of R;
thus (
multiplicity (r,c))
= ((
multiplicity (p,c))
+ (
multiplicity (q,c))) by
UPROOTS: 55
.= (((
BRoots p)
. c)
+ (
multiplicity (q,c))) by
UPROOTS:def 9
.= ((B1
. c)
+ (
multiplicity (q,c))) by
pf2
.= ((B1
. c)
+ ((
BRoots q)
. c)) by
UPROOTS:def 9
.= ((B1
. c)
+ (B2
. c)) by
pf2
.= (B
. c) by
PRE_POLY:def 5;
end;
hence thesis by
A,
dpp;
end;
theorem ::
RING_5:59
lll: for R be
domRing, p be
Ppoly of R holds p is
Ppoly of R, (
BRoots p)
proof
let R be
domRing, p be
Ppoly of R;
defpred
P[
Nat] means for p be
Ppoly of R st (
deg p)
= $1 holds p is
Ppoly of R, (
BRoots p);
IA:
P[1]
proof
now
let p be
Ppoly of R;
assume
A0: (
deg p)
= 1;
consider F be non
empty
FinSequence of (
Polynom-Ring R) such that
A1: p
= (
Product F) & for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
dpp1;
(
len F)
= 1 by
A0,
A1,
lemppoly;
then
A2: F
=
<*(F
. 1)*> by
FINSEQ_1: 40;
then
A3: (
dom F)
= (
Seg 1) by
FINSEQ_1: 38;
then
consider a be
Element of R such that
A4: (F
. 1)
= (
rpoly (1,a)) by
A1,
FINSEQ_1: 1;
reconsider e = 1 as
Element of (
dom F) by
A3,
FINSEQ_1: 1;
A5: (
Product F)
= (F
. e) by
A2,
GROUP_4: 9;
(
rpoly (1,a))
=
<%(
- a), (
1. R)%> by
repr;
then (
BRoots (
rpoly (1,a)))
= (
Bag
{a}) by
UPROOTS: 54;
hence p is
Ppoly of R, (
BRoots p) by
A1,
A4,
A5,
lemacf;
end;
hence thesis;
end;
IS:
now
let k be
Nat;
assume
AS: k
>= 1;
assume
IV:
P[k];
now
let p be
Ppoly of R;
assume
B0: (
deg p)
= (k
+ 1);
consider F be non
empty
FinSequence of (
Polynom-Ring R) such that
B1: p
= (
Product F) & for i be
Nat st i
in (
dom F) holds ex a be
Element of R st (F
. i)
= (
rpoly (1,a)) by
dpp1;
B1a: (
len F)
= (k
+ 1) by
B0,
B1,
lemppoly;
consider G be
FinSequence, y be
object such that
B2: F
= (G
^
<*y*>) by
FINSEQ_1: 46;
B2a: (
rng G)
c= (
rng F) by
B2,
FINSEQ_1: 29;
B2b: (
rng F)
c= the
carrier of (
Polynom-Ring R) by
FINSEQ_1:def 4;
then
reconsider G as
FinSequence of (
Polynom-Ring R) by
B2a,
XBOOLE_1: 1,
FINSEQ_1:def 4;
B3: (
len F)
= ((
len G)
+ (
len
<*y*>)) by
B2,
FINSEQ_1: 22
.= ((
len G)
+ 1) by
FINSEQ_1: 39;
then
reconsider G as non
empty
FinSequence of (
Polynom-Ring R) by
B1a,
AS;
reconsider q = (
Product G) as
Polynomial of R by
POLYNOM3:def 10;
C: (
dom G)
c= (
dom F) by
B2,
FINSEQ_1: 26;
D:
now
let i be
Nat;
assume
C0: i
in (
dom G);
then (G
. i)
= (F
. i) by
B2,
FINSEQ_1:def 7;
hence ex a be
Element of R st (G
. i)
= (
rpoly (1,a)) by
C,
C0,
B1;
end;
then
reconsider q as
Ppoly of R by
dpp1;
set B = (
BRoots q);
(
deg q)
= k by
B1a,
B3,
D,
lemppoly;
then
reconsider q as
Ppoly of R, B by
IV;
(
rng
<*y*>)
=
{y} by
FINSEQ_1: 39;
then
G5: y
in (
rng
<*y*>) by
TARSKI:def 1;
(
rng
<*y*>)
c= (
rng F) by
B2,
FINSEQ_1: 30;
then y
in (
rng F) by
G5;
then
reconsider y as
Element of (
Polynom-Ring R) by
B2b;
(
dom
<*y*>)
=
{1} by
FINSEQ_1: 2,
FINSEQ_1:def 8;
then 1
in (
dom
<*y*>) by
TARSKI:def 1;
then
B6: (F
. (k
+ 1))
= (
<*y*>
. 1) by
B2,
B3,
B1a,
FINSEQ_1:def 7
.= y by
FINSEQ_1:def 8;
(
dom F)
= (
Seg (k
+ 1)) by
B1a,
FINSEQ_1:def 3;
then
consider a be
Element of R such that
B9: y
= (
rpoly (1,a)) by
B1,
B6,
FINSEQ_1: 4;
reconsider r = y as
Ppoly of R, (
Bag
{a}) by
lemacf,
B9;
B10: p
= ((
Product G)
* y) by
B1,
B2,
GROUP_4: 6
.= (q
*' r) by
POLYNOM3:def 10;
reconsider B1 = (B
+ (
Bag
{a})) as non
zero
bag of the
carrier of R;
(
rpoly (1,a))
=
<%(
- a), (
1. R)%> by
repr;
then (
BRoots (
rpoly (1,a)))
= (
Bag
{a}) by
UPROOTS: 54;
then (
BRoots p)
= (B
+ (
Bag
{a})) by
B9,
B10,
UPROOTS: 56;
hence p is
Ppoly of R, (
BRoots p) by
B10,
lemacf2;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat st k
>= 1 holds
P[k] from
NAT_1:sch 8(
IA,
IS);
reconsider n = (
deg p) as
Element of
NAT by
INT_1: 3;
(n
+ 1)
> (
0
+ 1) by
RATFUNC1:def 2,
XREAL_1: 6;
then n
>= 1 by
NAT_1: 13;
hence thesis by
I;
end;
definition
let R be
domRing;
let S be non
empty
finite
Subset of R;
mode
Ppoly of R,S is
Ppoly of R, (
Bag S);
end
theorem ::
RING_5:60
m00: for R be
domRing, S be non
empty
finite
Subset of R holds for p be
Ppoly of R, S holds (
deg p)
= (
card S)
proof
let R be
domRing, S be non
empty
finite
Subset of R;
let p be
Ppoly of R, S;
thus (
deg p)
= (
card (
Bag S)) by
dpp
.= (
card S) by
UPROOTS: 13;
end;
theorem ::
RING_5:61
m0: for R be
domRing, S be non
empty
finite
Subset of R holds for p be
Ppoly of R, S holds for a be
Element of R st a
in S holds (
rpoly (1,a))
divides p & not ((
rpoly (1,a))
`^ 2)
divides p
proof
let R be
domRing, S be non
empty
finite
Subset of R;
let p be
Ppoly of R, S;
let a be
Element of R;
assume a
in S;
then
A: ((
Bag S)
. a)
= 1 by
UPROOTS: 7;
X: ((
rpoly (1,a))
`^ ((
Bag S)
. a))
divides p & not ((
rpoly (1,a))
`^ (((
Bag S)
. a)
+ 1))
divides p by
pf1;
hence (
rpoly (1,a))
divides p by
A,
POLYNOM5: 16;
thus thesis by
A,
X;
end;
theorem ::
RING_5:62
m1: for R be
domRing, S be non
empty
finite
Subset of R, p be
Ppoly of R, S holds for a be
Element of R st a
in S holds (
eval (p,a))
= (
0. R)
proof
let R be
domRing, S be non
empty
finite
Subset of R, p be
Ppoly of R, S;
let a be
Element of R;
assume a
in S;
then
consider q be
Polynomial of R such that
H: ((
rpoly (1,a))
*' q)
= p by
m0,
RING_4: 1;
a
is_a_root_of p by
H,
prl2,
HURWITZ: 30;
hence (
eval (p,a))
= (
0. R) by
POLYNOM5:def 7;
end;
theorem ::
RING_5:63
for R be
domRing, S be non
empty
finite
Subset of R, p be
Ppoly of R, S holds (
Roots p)
= S
proof
let R be
domRing, S be non
empty
finite
Subset of R, p be
Ppoly of R, S;
A0:
now
let o be
object;
assume
AS: o
in S;
then
reconsider x = o as
Element of R;
(
eval (p,x))
= (
0. R) by
AS,
m1;
then x
is_a_root_of p by
POLYNOM5:def 7;
hence o
in (
Roots p) by
POLYNOM5:def 10;
end;
then (
card ((
Roots p)
\ S))
= ((
card (
Roots p))
- (
card S)) by
TARSKI:def 3,
CARD_2: 44;
then
B: (((
card (
Roots p))
- (
card S))
+ (
card S))
>= (
0
+ (
card S)) by
XREAL_1: 6;
(
card (
Roots p))
<= (
deg p) by
degpoly;
then (
card (
Roots p))
<= (
card S) by
m00;
then (
card S)
= (
card (
Roots p)) by
B,
XXREAL_0: 1;
hence thesis by
A0,
CARD_2: 102,
TARSKI:def 3;
end;
begin
theorem ::
RING_5:64
acf: for R be
domRing, p be non
zero
with_roots
Polynomial of R holds ex q be
Ppoly of R, (
BRoots p), r be non
with_roots
Polynomial of R st p
= (q
*' r) & (
Roots q)
= (
Roots p)
proof
let R be
domRing, p be non
zero
with_roots
Polynomial of R;
defpred
P[
Nat] means for p be non
zero
with_roots
Polynomial of R st (
deg p)
= $1 holds ex q be
Ppoly of R, (
BRoots p), r be non
with_roots
Polynomial of R st p
= (q
*' r) & (
Roots q)
= (
Roots p);
IA:
P[1]
proof
let p be non
zero
with_roots
Polynomial of R;
assume
AS: (
deg p)
= 1;
consider a be
Element of R such that
A1: a
is_a_root_of p by
POLYNOM5:def 8;
(
eval (p,a))
= (
0. R) by
A1,
POLYNOM5:def 7;
then
consider p1 be
Polynomial of R such that
A2: p
= ((
rpoly (1,a))
*' p1) by
Th9,
RING_4: 1;
reconsider q = (
rpoly (1,a)) as
Ppoly of R by
lemppoly1;
reconsider B = (
BRoots p) as non
zero
bag of the
carrier of R;
p1
<> (
0_. R) & (
rpoly (1,a))
<> (
0_. R) by
A2;
then (
deg p)
= ((
deg (
rpoly (1,a)))
+ (
deg p1)) by
A2,
HURWITZ: 23
.= (1
+ (
deg p1)) by
HURWITZ: 27;
then
reconsider p1 as non
with_roots
Polynomial of R by
AS,
HURWITZ: 24;
reconsider p1 as non
zero non
with_roots
Polynomial of R;
A7: (
rpoly (1,a))
=
<%(
- a), (
1. R)%> by
repr;
(
BRoots p)
= ((
BRoots (
rpoly (1,a)))
+ (
BRoots p1)) by
A2,
UPROOTS: 56
.= (((
{a},1)
-bag )
+ (
BRoots p1)) by
A7,
UPROOTS: 54
.= (((
{a},1)
-bag )
+ (
EmptyBag the
carrier of R)) by
lemacf1
.= (
Bag
{a}) by
PRE_POLY: 53;
then
reconsider q = (
rpoly (1,a)) as
Ppoly of R, (
BRoots p) by
lemacf;
take q, p1;
thus (q
*' p1)
= p by
A2;
thus (
Roots p)
= ((
Roots q)
\/ (
Roots p1)) by
A2,
UPROOTS: 23
.= (
Roots q);
end;
IS:
now
let k be
Nat;
assume 1
<= k;
assume
IV:
P[k];
now
let p be non
zero
with_roots
Polynomial of R;
assume
AS1: (
deg p)
= (k
+ 1);
consider a be
Element of R such that
A1: a
is_a_root_of p by
POLYNOM5:def 8;
consider s be
Polynomial of R such that
A2: p
= ((
rpoly (1,a))
*' s) by
A1,
HURWITZ: 33;
reconsider s as non
zero
Polynomial of R by
A2;
per cases ;
suppose
A4: s is non
with_roots;
then
A5: (
Roots s)
=
{} ;
reconsider q = (
rpoly (1,a)) as
Ppoly of R, (
Bag
{a}) by
lemacf;
A7: (
rpoly (1,a))
=
<%(
- a), (
1. R)%> by
repr;
A6: (
BRoots p)
= ((
BRoots (
rpoly (1,a)))
+ (
BRoots s)) by
A2,
UPROOTS: 56
.= ((
BRoots (
rpoly (1,a)))
+ (
EmptyBag the
carrier of R)) by
A4,
lemacf1
.= (
BRoots (
rpoly (1,a))) by
PRE_POLY: 53
.= (
Bag
{a}) by
A7,
UPROOTS: 54;
(
Roots p)
= ((
Roots q)
\/ (
Roots s)) by
A2,
UPROOTS: 23
.= (
Roots q) by
A5;
hence ex q be
Ppoly of R, (
BRoots p), r be non
with_roots
Polynomial of R st p
= (q
*' r) & (
Roots q)
= (
Roots p) by
A2,
A4,
A6;
end;
suppose s is
with_roots;
then
reconsider s as non
zero
with_roots
Polynomial of R;
s
<> (
0_. R) & (
rpoly (1,a))
<> (
0_. R);
then (
deg p)
= ((
deg (
rpoly (1,a)))
+ (
deg s)) by
A2,
HURWITZ: 23
.= (1
+ (
deg s)) by
HURWITZ: 27;
then
consider qs be
Ppoly of R, (
BRoots s), rs be non
with_roots
Polynomial of R such that
B1: s
= (qs
*' rs) & (
Roots qs)
= (
Roots s) by
AS1,
IV;
reconsider rs as non
zero non
with_roots
Polynomial of R;
set q = ((
rpoly (1,a))
*' qs);
B2: p
= (q
*' rs) by
A2,
B1,
POLYNOM3: 33;
reconsider B = ((
Bag
{a})
+ (
BRoots s)) as non
zero
bag of the
carrier of R;
(
rpoly (1,a)) is
Ppoly of R, (
Bag
{a}) by
lemacf;
then
reconsider q as
Ppoly of R, B by
lemacf2;
B7: (
rpoly (1,a))
=
<%(
- a), (
1. R)%> by
repr;
B4: (
BRoots p)
= ((
BRoots q)
+ (
BRoots rs)) by
B2,
UPROOTS: 56
.= ((
BRoots q)
+ (
EmptyBag the
carrier of R)) by
lemacf1
.= (
BRoots q) by
PRE_POLY: 53
.= ((
BRoots (
rpoly (1,a)))
+ (
BRoots qs)) by
UPROOTS: 56
.= ((
Bag
{a})
+ (
BRoots qs)) by
B7,
UPROOTS: 54
.= B by
pf2;
B3: (
Roots p)
= ((
Roots q)
\/ (
Roots rs)) by
B2,
UPROOTS: 23
.= (
Roots q);
thus ex q be
Ppoly of R, (
BRoots p), r be non
with_roots
Polynomial of R st p
= (q
*' r) & (
Roots q)
= (
Roots p) by
B2,
B3,
B4;
end;
end;
hence
P[(k
+ 1)];
end;
I: for k be
Nat st 1
<= k holds
P[k] from
NAT_1:sch 8(
IA,
IS);
K: (
deg p)
>= (
0
+ 1) by
INT_1: 7,
RATFUNC1:def 2;
p
<> (
0_. R);
then (
deg p) is
Element of
NAT by
T8;
then
consider d be
Nat such that
H: (
deg p)
= d;
thus thesis by
K,
H,
I;
end;
theorem ::
RING_5:65
for R be
domRing, p be non
zero
Polynomial of R holds (
card (
Roots p))
<= (
card (
BRoots p))
proof
let R be
domRing, p be non
zero
Polynomial of R;
per cases ;
suppose p is
with_roots;
then
reconsider p1 = p as non
zero
with_roots
Polynomial of R;
consider q be
Ppoly of R, (
BRoots p1), r be non
with_roots
Polynomial of R such that
A: p1
= (q
*' r) & (
Roots q)
= (
Roots p1) by
acf;
(
deg q)
= (
card (
BRoots q)) by
lemacf5
.= (
card (
BRoots p1)) by
pf2;
hence thesis by
A,
degpoly;
end;
suppose
A: p is non
with_roots;
then (
card (
Roots p))
=
0
.= (
card (
EmptyBag the
carrier of R)) by
UPROOTS: 11
.= (
card (
BRoots p)) by
A,
lemacf1;
hence thesis;
end;
end;
theorem ::
RING_5:66
for R be
domRing, p be non
constant
Polynomial of R holds (
card (
BRoots p))
= (
deg p) iff ex a be
Element of R, q be
Ppoly of R st p
= (a
* q)
proof
let R be
domRing, p be non
constant
Polynomial of R;
per cases ;
suppose p is
with_roots;
then
reconsider p1 = p as non
zero
with_roots
Polynomial of R;
consider q be
Ppoly of R, (
BRoots p1), r be non
with_roots
Polynomial of R such that
H: p1
= (q
*' r) & (
Roots q)
= (
Roots p1) by
acf;
reconsider r1 = r as
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
A:
now
assume
A1: (
card (
BRoots p))
= (
deg p);
r
<> (
0_. R) & q
<> (
0_. R);
then (
deg p)
= ((
deg q)
+ (
deg r)) by
H,
HURWITZ: 23
.= ((
card (
BRoots q))
+ (
deg r)) by
lemacf5
.= ((
deg p)
+ (
deg r)) by
A1,
pf2;
then r1 is
constant;
then
consider a be
Element of R such that
B: r1
= (a
| R) by
RING_4: 20;
p
= (q
*' (a
* (
1_. R))) by
H,
B,
RING_4: 16
.= (a
* (q
*' (
1_. R))) by
RATFUNC1: 6
.= (a
* q);
hence ex a be
Element of R, q be
Ppoly of R st p
= (a
* q);
end;
now
assume ex a be
Element of R, q be
Ppoly of R st p
= (a
* q);
then
consider a be
Element of R, q be
Ppoly of R such that
A1: p
= (a
* q);
set B = (
BRoots q);
reconsider q as
Ppoly of R, B by
lll;
p
<> (
0_. R);
then
A3: a is non
zero by
A1,
POLYNOM5: 26;
hence (
deg p)
= (
deg q) by
A1,
Th25
.= (
card B) by
lemacf5
.= (
card (
BRoots p)) by
A1,
A3,
llll;
end;
hence thesis by
A;
end;
suppose
A: p is non
with_roots;
then
reconsider p1 = p as non
zero non
with_roots
Polynomial of R;
(
card (
BRoots p))
= (
card (
EmptyBag the
carrier of R)) by
A,
lemacf1
.=
0 by
UPROOTS: 11;
hence thesis by
A,
RATFUNC1:def 2;
end;
end;
theorem ::
RING_5:67
for R be
domRing, p,q be
Polynomial of R st (ex S be
Subset of R st (
card S)
= ((
max ((
deg p),(
deg q)))
+ 1) & for a be
Element of R st a
in S holds (
eval (p,a))
= (
eval (q,a))) holds p
= q
proof
let R be
domRing, p,q be
Polynomial of R;
assume ex S be
Subset of R st (
card S)
= ((
max ((
deg p),(
deg q)))
+ 1) & for a be
Element of R st a
in S holds (
eval (p,a))
= (
eval (q,a));
then
consider S be
Subset of R such that
A0: (
card S)
= ((
max ((
deg p),(
deg q)))
+ 1) & for a be
Element of R st a
in S holds (
eval (p,a))
= (
eval (q,a));
now
assume
HH: p
<> q;
((
max ((
deg p),(
deg q)))
+ 1) is
Element of
NAT
proof
D: (
max ((
deg p),(
deg q)))
>= (
deg p) by
XXREAL_0: 25;
(
deg p)
>= (
- 1)
proof
per cases ;
suppose p
= (
0_. R);
hence thesis by
HURWITZ: 20;
end;
suppose p
<> (
0_. R);
hence thesis by
T8;
end;
end;
then (
max ((
deg p),(
deg q)))
>= (
- 1) by
D,
XXREAL_0: 2;
then ((
max ((
deg p),(
deg q)))
+ 1)
>= ((
- 1)
+ 1) by
XREAL_1: 6;
hence thesis by
INT_1: 3;
end;
then
reconsider S as
finite
Subset of the
carrier of R by
A0;
per cases ;
suppose
AS: p is
zero;
then q is non
zero by
HH;
then
reconsider q as non
zero
Element of the
carrier of (
Polynom-Ring R) by
POLYNOM3:def 10;
reconsider n = (
deg q) as
Element of
NAT by
AS,
T8;
(
deg p)
= (
- 1) by
AS,
HURWITZ: 20;
then
C0: ((
max ((
deg p),(
deg q)))
+ 1)
= (n
+ 1) by
XXREAL_0:def 10;
now
let x be
object;
assume
C: x
in S;
then
reconsider a = x as
Element of R;
(
eval (q,a))
= (
eval (p,a)) by
A0,
C
.= (
0. R) by
AS,
POLYNOM4: 17;
then a
is_a_root_of q by
POLYNOM5:def 7;
hence x
in (
Roots q) by
POLYNOM5:def 10;
end;
then
C2: (n
+ 1)
<= (
card (
Roots q)) by
A0,
C0,
NAT_1: 43,
TARSKI:def 3;
(
card (
Roots q))
<= (
deg q) by
degpoly;
then
C4: (n
+ 1)
<= n by
C2,
XXREAL_0: 2;
n
<= (n
+ 1) by
NAT_1: 11;
then (n
+ 1)
= n by
C4,
XXREAL_0: 1;
hence contradiction;
end;
suppose p is non
zero;
then
reconsider n = (
deg p) as
Element of
NAT by
T8;
H2: n
= ((
len p)
- 1) by
HURWITZ:def 2;
then
H2a: (
len p)
= (n
+ 1);
per cases by
XXREAL_0: 1;
suppose
D: (
len q)
< (
len p);
then ((
len q)
+ 1)
<= (
len p) by
INT_1: 7;
then (((
len q)
+ 1)
- 1)
<= ((
len p)
- 1) by
XREAL_1: 9;
then (q
. n)
= (
0. R) by
H2,
ALGSEQ_1: 8;
then
H3: (q
. n)
<> (p
. n) by
H2a,
ALGSEQ_1: 10;
(
deg q)
= ((
len q)
- 1) & (
deg p)
= ((
len p)
- 1) by
HURWITZ:def 2;
then
H4: (
max ((
deg p),(
deg q)))
= n by
D,
XREAL_1: 9,
XXREAL_0:def 10;
defpred
P[
Nat] means (p
. $1)
<> (q
. $1);
A2: for k be
Nat st
P[k] holds k
<= n
proof
let k be
Nat;
assume
B0:
P[k];
now
let i be
Nat;
assume i
> n;
then
B1: i
>= (
len p) by
H2a,
NAT_1: 13;
hence (p
. i)
= (
0. R) by
ALGSEQ_1: 8
.= (q
. i) by
B1,
D,
XXREAL_0: 2,
ALGSEQ_1: 8;
end;
hence thesis by
B0;
end;
A3: ex k be
Nat st
P[k] by
H3;
consider m be
Nat such that
A4:
P[m] & for i be
Nat st
P[i] holds i
<= m from
NAT_1:sch 6(
A2,
A3);
A5: (p
. m)
<> (q
. m) & m
<= n by
A2,
A4;
A6:
now
assume
A7: ((p
- q)
. m)
= (
0. R);
((p
. m)
+ (
0. R))
= ((p
. m)
+ ((
- (q
. m))
+ (q
. m))) by
RLVECT_1: 5
.= (((p
. m)
+ (
- (q
. m)))
+ (q
. m)) by
RLVECT_1:def 3
.= (((p
. m)
- (q
. m))
+ (q
. m)) by
RLVECT_1:def 11
.= ((
0. R)
+ (q
. m)) by
A7,
NORMSP_1:def 3;
hence contradiction by
A4;
end;
then (p
- q)
<> (
0_. R) by
FUNCOP_1: 7,
ORDINAL1:def 12;
then
reconsider r = (p
- q) as non
zero
Polynomial of R by
UPROOTS:def 5;
now
let x be
object;
assume
C2: x
in S;
then
reconsider a = x as
Element of R;
(
eval (r,a))
= ((
eval (p,a))
- (
eval (q,a))) by
POLYNOM4: 21
.= ((
eval (p,a))
- (
eval (p,a))) by
C2,
A0
.= (
0. R) by
RLVECT_1: 15;
then a
is_a_root_of r by
POLYNOM5:def 7;
hence x
in (
Roots r) by
POLYNOM5:def 10;
end;
then
C2: (n
+ 1)
<= (
card (
Roots r)) by
A0,
H4,
NAT_1: 43,
TARSKI:def 3;
(
len r)
= (m
+ 1)
proof
E1:
now
let i be
Nat;
assume i
>= (m
+ 1);
then not (i
<= m) by
NAT_1: 13;
then
X: (p
. i)
= (q
. i) by
A4;
thus (r
. i)
= ((p
. i)
- (q
. i)) by
NORMSP_1:def 3
.= (
0. R) by
X,
RLVECT_1: 15;
end;
for k be
Nat st k
is_at_least_length_of r holds (m
+ 1)
<= k by
A6,
NAT_1: 13;
hence thesis by
E1,
ALGSEQ_1:def 2,
ALGSEQ_1:def 3;
end;
then ((
len r)
- 1)
= m;
then
C3: (
deg r)
= m by
HURWITZ:def 2;
(
card (
Roots r))
<= (
deg r) by
degpoly;
then (n
+ 1)
<= m by
C2,
C3,
XXREAL_0: 2;
then
C4: (n
+ 1)
<= n by
A5,
XXREAL_0: 2;
n
<= (n
+ 1) by
NAT_1: 11;
then (n
+ 1)
= n by
C4,
XXREAL_0: 1;
hence contradiction;
end;
suppose
D: (
len p)
< (
len q);
then ((
len p)
+ 1)
<= (
len q) by
INT_1: 7;
then
D1: (((
len p)
+ 1)
- 1)
<= ((
len q)
- 1) by
XREAL_1: 9;
((
len p)
- 1)
< ((
len q)
- 1) by
D,
XREAL_1: 9;
then (
deg p)
< ((
len q)
- 1) by
HURWITZ:def 2;
then (
deg p)
< (
deg q) &
0
<= n by
HURWITZ:def 2;
then
reconsider l = (
deg q) as
Element of
NAT by
INT_1: 3;
H2b: l
= ((
len q)
- 1) by
HURWITZ:def 2;
then
H2c: (
len q)
= (l
+ 1);
(p
. l)
= (
0. R) by
D1,
H2b,
ALGSEQ_1: 8;
then
H3: (q
. l)
<> (p
. l) by
H2c,
ALGSEQ_1: 10;
(
deg q)
= ((
len q)
- 1) & (
deg p)
= ((
len p)
- 1) by
HURWITZ:def 2;
then
H4: (
max ((
deg p),(
deg q)))
= l by
D,
XREAL_1: 9,
XXREAL_0:def 10;
defpred
P[
Nat] means (p
. $1)
<> (q
. $1);
A2: for k be
Nat st
P[k] holds k
<= l
proof
let k be
Nat;
assume
B0:
P[k];
now
let i be
Nat;
assume i
> l;
then
B1: i
>= (
len q) by
H2c,
NAT_1: 13;
hence (q
. i)
= (
0. R) by
ALGSEQ_1: 8
.= (p
. i) by
B1,
D,
XXREAL_0: 2,
ALGSEQ_1: 8;
end;
hence thesis by
B0;
end;
A3: ex k be
Nat st
P[k] by
H3;
consider m be
Nat such that
A4:
P[m] & for i be
Nat st
P[i] holds i
<= m from
NAT_1:sch 6(
A2,
A3);
A5: (p
. m)
<> (q
. m) & m
<= l by
A2,
A4;
A6:
now
assume
A7: ((p
- q)
. m)
= (
0. R);
((p
. m)
+ (
0. R))
= ((p
. m)
+ ((
- (q
. m))
+ (q
. m))) by
RLVECT_1: 5
.= (((p
. m)
+ (
- (q
. m)))
+ (q
. m)) by
RLVECT_1:def 3
.= (((p
. m)
- (q
. m))
+ (q
. m)) by
RLVECT_1:def 11
.= ((
0. R)
+ (q
. m)) by
A7,
NORMSP_1:def 3;
hence contradiction by
A4;
end;
then (p
- q)
<> (
0_. R) by
FUNCOP_1: 7,
ORDINAL1:def 12;
then
reconsider r = (p
- q) as non
zero
Polynomial of R by
UPROOTS:def 5;
now
let x be
object;
assume
C2: x
in S;
then
reconsider a = x as
Element of R;
(
eval (r,a))
= ((
eval (p,a))
- (
eval (q,a))) by
POLYNOM4: 21
.= ((
eval (p,a))
- (
eval (p,a))) by
C2,
A0
.= (
0. R) by
RLVECT_1: 15;
then a
is_a_root_of r by
POLYNOM5:def 7;
hence x
in (
Roots r) by
POLYNOM5:def 10;
end;
then
C2: (l
+ 1)
<= (
card (
Roots r)) by
A0,
H4,
NAT_1: 43,
TARSKI:def 3;
(
len r)
= (m
+ 1)
proof
E1:
now
let i be
Nat;
assume i
>= (m
+ 1);
then not (i
<= m) by
NAT_1: 13;
then
X: (p
. i)
= (q
. i) by
A4;
thus (r
. i)
= ((p
. i)
- (q
. i)) by
NORMSP_1:def 3
.= (
0. R) by
X,
RLVECT_1: 15;
end;
for k be
Nat st k
is_at_least_length_of r holds (m
+ 1)
<= k by
A6,
NAT_1: 13;
hence thesis by
E1,
ALGSEQ_1:def 2,
ALGSEQ_1:def 3;
end;
then ((
len r)
- 1)
= m;
then
C3: (
deg r)
= m by
HURWITZ:def 2;
(
card (
Roots r))
<= (
deg r) by
degpoly;
then (l
+ 1)
<= m by
C2,
C3,
XXREAL_0: 2;
then
C4: (l
+ 1)
<= l by
A5,
XXREAL_0: 2;
l
<= (l
+ 1) by
NAT_1: 11;
then (l
+ 1)
= l by
C4,
XXREAL_0: 1;
hence contradiction;
end;
suppose
D: (
len p)
= (
len q);
n
= ((
len p)
- 1) by
HURWITZ:def 2;
then
H2: (
len p)
= (n
+ 1);
H4: (
deg q)
= ((
len q)
- 1) & (
deg p)
= ((
len p)
- 1) by
HURWITZ:def 2;
consider k be
Nat such that
A1: k
< (
len p) & (p
. k)
<> (q
. k) by
HH,
D,
ALGSEQ_1: 12;
defpred
P[
Nat] means (p
. $1)
<> (q
. $1);
A2: for k be
Nat st
P[k] holds k
<= n
proof
let k be
Nat;
assume
B0:
P[k];
now
let i be
Nat;
assume i
> n;
then
B1: i
>= (
len p) by
H2,
NAT_1: 13;
hence (p
. i)
= (
0. R) by
ALGSEQ_1: 8
.= (q
. i) by
D,
B1,
ALGSEQ_1: 8;
end;
hence thesis by
B0;
end;
A3: ex k be
Nat st
P[k] by
A1;
consider m be
Nat such that
A4:
P[m] & for i be
Nat st
P[i] holds i
<= m from
NAT_1:sch 6(
A2,
A3);
A5: (p
. m)
<> (q
. m) & m
<= n by
A2,
A4;
A6:
now
assume
A7: ((p
- q)
. m)
= (
0. R);
((p
. m)
+ (
0. R))
= ((p
. m)
+ ((
- (q
. m))
+ (q
. m))) by
RLVECT_1: 5
.= (((p
. m)
+ (
- (q
. m)))
+ (q
. m)) by
RLVECT_1:def 3
.= (((p
. m)
- (q
. m))
+ (q
. m)) by
RLVECT_1:def 11
.= ((
0. R)
+ (q
. m)) by
A7,
NORMSP_1:def 3;
hence contradiction by
A4;
end;
then (p
- q)
<> (
0_. R) by
FUNCOP_1: 7,
ORDINAL1:def 12;
then
reconsider r = (p
- q) as non
zero
Polynomial of R by
UPROOTS:def 5;
now
let x be
object;
assume
C2: x
in S;
then
reconsider a = x as
Element of R;
(
eval (r,a))
= ((
eval (p,a))
- (
eval (q,a))) by
POLYNOM4: 21
.= ((
eval (p,a))
- (
eval (p,a))) by
C2,
A0
.= (
0. R) by
RLVECT_1: 15;
then a
is_a_root_of r by
POLYNOM5:def 7;
hence x
in (
Roots r) by
POLYNOM5:def 10;
end;
then
C2: (n
+ 1)
<= (
card (
Roots r)) by
H4,
A0,
D,
NAT_1: 43,
TARSKI:def 3;
(
len r)
= (m
+ 1)
proof
E1:
now
let i be
Nat;
assume i
>= (m
+ 1);
then not (i
<= m) by
NAT_1: 13;
then
X: (p
. i)
= (q
. i) by
A4;
thus (r
. i)
= ((p
. i)
- (q
. i)) by
NORMSP_1:def 3
.= (
0. R) by
X,
RLVECT_1: 15;
end;
for k be
Nat st k
is_at_least_length_of r holds (m
+ 1)
<= k by
A6,
NAT_1: 13;
hence thesis by
E1,
ALGSEQ_1:def 2,
ALGSEQ_1:def 3;
end;
then ((
len r)
- 1)
= m;
then
C3: (
deg r)
= m by
HURWITZ:def 2;
(
card (
Roots r))
<= (
deg r) by
degpoly;
then (n
+ 1)
<= m by
C2,
C3,
XXREAL_0: 2;
then
C4: (n
+ 1)
<= n by
A5,
XXREAL_0: 2;
n
<= (n
+ 1) by
NAT_1: 11;
then (n
+ 1)
= n by
C4,
XXREAL_0: 1;
hence contradiction;
end;
end;
end;
hence thesis;
end;
registration
let F be
algebraic-closed
Field;
cluster ->
with_roots for non
constant
Polynomial of F;
coherence
proof
let p be non
constant
Polynomial of F;
(
deg p)
>
0 by
RATFUNC1:def 2;
then ((
len p)
- 1)
>
0 by
HURWITZ:def 2;
then (((
len p)
- 1)
+ 1)
> (
0
+ 1) by
XREAL_1: 6;
hence p is
with_roots by
POLYNOM5:def 9;
end;
end
registration
cluster
F_Real -> non
algebraic-closed;
coherence
proof
set q = (
npoly (
F_Real ,2));
A: (
0
+ 2) is
even;
now
assume
AS:
F_Real is
algebraic-closed;
((
len q)
- 1)
= (
deg q) by
HURWITZ:def 2
.= 2 by
lem6;
then (
len q)
= 3;
hence contradiction by
A,
AS,
POLYNOM5:def 9;
end;
hence thesis;
end;
end
registration
cluster -> non
algebraic-closed for
finite
domRing;
coherence
proof
let R be
finite
domRing;
ex q be
Polynomial of R st (
len q)
> 1 & not q is
with_roots
proof
set p = the
Ppoly of R, (
[#] the
carrier of R);
take q = (p
+ (
1_. R));
A: (
deg p)
>= (
card (
[#] the
carrier of R)) by
m00;
then
B: (
deg p)
>= 1 by
NAT_1: 14;
C: (
deg p)
> (
deg (
1_. R)) by
A,
RATFUNC1:def 2;
then (
deg q)
= (
max ((
deg p),(
deg (
1_. R)))) by
HURWITZ: 21
.= (
deg p) by
C,
XXREAL_0:def 10;
then ((
len q)
- 1)
>= 1 by
B,
HURWITZ:def 2;
then (((
len q)
- 1)
+ 1)
>= (1
+ 1) by
XREAL_1: 6;
hence (
len q)
> 1 by
NAT_1: 13;
D:
now
let a be
Element of R;
a
in the
carrier of R;
then
D1: a
in (
[#] the
carrier of R) by
SUBSET_1:def 3;
thus (
eval (q,a))
= ((
eval (p,a))
+ (
eval ((
1_. R),a))) by
POLYNOM4: 19
.= ((
0. R)
+ (
eval ((
1_. R),a))) by
D1,
m1
.= ((
0. R)
+ (
1. R)) by
POLYNOM4: 18;
end;
now
assume q is
with_roots;
then
consider a be
Element of R such that
H: a
is_a_root_of q by
POLYNOM5:def 8;
(
0. R)
= (
eval (q,a)) by
H,
POLYNOM5:def 7
.= (
1. R) by
D;
hence contradiction;
end;
hence thesis;
end;
hence thesis by
POLYNOM5:def 9;
end;
end
registration
cluster
algebraic-closed ->
almost_right_invertible for
Ring;
coherence
proof
let R be
Ring;
assume
AS: R is
algebraic-closed;
let a be
Element of R;
set p =
<%(
1. R), a%>;
assume a
<> (
0. R);
then (
len p)
= 2 by
POLYNOM5: 40;
then
consider b be
Element of R such that
A: b
is_a_root_of p by
AS,
POLYNOM5:def 8,
POLYNOM5:def 9;
(
0. R)
= (
eval (p,b)) by
A,
POLYNOM5:def 7
.= ((
1. R)
+ (a
* b)) by
POLYNOM5: 44;
then (
1. R)
= (
- (a
* b)) by
RLVECT_1: 6
.= (a
* (
- b)) by
VECTSP_1: 8;
hence a is
right_invertible by
ALGSTR_0:def 28;
end;
end
theorem ::
RING_5:68
cc4: for F be
algebraic-closed
Field, p be non
constant
Polynomial of F holds ex a be
Element of F, q be
Ppoly of F, (
BRoots p) st (a
* q)
= p
proof
let F be
algebraic-closed
Field, p be non
constant
Polynomial of F;
consider q be
Ppoly of F, (
BRoots p), r be non
with_roots
Polynomial of F such that
A: p
= (q
*' r) & (
Roots q)
= (
Roots p) by
acf;
reconsider r1 = r as
Element of the
carrier of (
Polynom-Ring F) by
POLYNOM3:def 10;
((
len r)
- 1)
<= (1
- 1) by
XREAL_1: 9,
POLYNOM5:def 9;
then r1 is
constant by
HURWITZ:def 2;
then
consider a be
Element of F such that
B: r1
= (a
| F) by
RING_4: 20;
take a, q;
thus p
= (q
*' (a
* (
1_. F))) by
A,
B,
RING_4: 16
.= (a
* (q
*' (
1_. F))) by
RATFUNC1: 6
.= (a
* q);
end;
theorem ::
RING_5:69
cc3: for F be
algebraic-closed
Field, p be non
constant
monic
Polynomial of F holds p is
Ppoly of F, (
BRoots p)
proof
let R be
algebraic-closed
Field, p be non
constant
monic
Polynomial of R;
consider a be
Element of R, q be
Ppoly of R, (
BRoots p) such that
A: p
= (a
* q) by
cc4;
(
1. R)
= (
LC p) by
RATFUNC1:def 7
.= (a
* (
LC q)) by
A,
RATFUNC1: 18
.= (a
* (
1. R)) by
cc2
.= a;
hence thesis by
A;
end;
theorem ::
RING_5:70
for F be
Field holds F is
algebraic-closed iff (for p be non
constant
monic
Polynomial of F holds p is
Ppoly of F)
proof
let F be
Field;
now
assume
AS: for p be non
constant
monic
Polynomial of F holds p is
Ppoly of F;
now
let p be
Polynomial of F;
assume
A: (
len p)
> 1;
then
B: p is non
zero by
POLYNOM4: 3;
set np = (
NormPolynomial p);
(((
len np)
- 1)
+ 1)
> 1 by
A,
POLYNOM5: 57;
then ((
len np)
- 1)
>= 1 by
NAT_1: 13;
then np is non
constant
monic by
B,
HURWITZ:def 2;
then
reconsider np as
Ppoly of F by
AS;
np is
with_roots;
hence p is
with_roots by
A,
POLYNOM5: 60;
end;
hence F is
algebraic-closed by
POLYNOM5:def 9;
end;
hence thesis by
cc3;
end;