:: {I}ntroduction to {A}lgebraic {G}eometry
:: by Yasushige Watase
::
:: Received June 30, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
FUNCT_1, XXREAL_0, TARSKI, NAT_1, ARYTM_3, ZFMISC_1, CARD_1, YELLOW_8,
ORDINAL1, ARYTM_1, PRE_POLY, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1,
POLYNOM1, POLYNOM2, FINSEQ_2, CARD_3, SQUARE_1, STRUCT_0, PARTFUN1,
FINSET_1, SUPINF_2, RATFUNC1, FUNCT_2, HILBASIS, VECTSP_2, CARD_FIL,
RSSPACE, IDEAL_1, MESFUNC1, INT_2, SETFAM_1, XCMPLX_0, POLYNOM5,
LATTICES, BSPACE, NEWTON, RING_1, RING_2, MATROID0, SGRAPH1, FUNCT_4,
UPROOTS, BINOP_1, ALGGEO_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, CARD_1,
NUMBERS, XXREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCT_7, WSIERP_1,
PRE_POLY, BSPACE, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1,
VECTSP_2, POLYNOM1, BINOM, POLYNOM2, UPROOTS, IDEAL_1, HILBASIS,
POLYNOM7, GROEB_1, RING_1, RING_2, HILB10_5, POLYNOM9;
constructors RELSET_1, RECDEF_1, FUNCT_7, WSIERP_1, BSPACE, GCD_1, BINOM,
POLYNOM2, UPROOTS, HILBASIS, TERMORD, GROEB_1, HILB10_5, IDEAL_2,
POLYNOM9;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1,
VALUED_0, RELSET_1, STRUCT_0, VECTSP_1, PRE_POLY, POLYNOM2, AFINSQ_1,
POLYNOM6, FINSEQ_1, FUNCOP_1, ALGSTR_1, ALGSTR_0, HILBASIS, POLYNOM7,
POLYNOM1, RLVECT_1, IDEAL_1, RING_1, RING_2, PBOOLE, FINSET_1, NEWTON04,
RVSUM_4;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0;
equalities FINSEQ_1, STRUCT_0, POLYNOM1, FINSEQ_2, SUBSET_1, IDEAL_1,
POLYNOM9;
expansions IDEAL_1, SUBSET_1, FUNCT_1, TARSKI, STRUCT_0, XBOOLE_0, FINSEQ_1,
RING_1;
theorems TARSKI, FUNCT_1, CARD_1, ZFMISC_1, FINSEQ_3, FINSEQ_1, FINSEQ_5,
FINSEQ_2, ORDINAL1, HILB10_3, XBOOLE_0, PRE_POLY, FUNCT_2, POLYNOM1,
POLYNOM2, PARTFUN1, XBOOLE_1, RLVECT_1, POLYNOM7, SUBSET_1, IDEAL_1,
SETFAM_1, BINOM, GROUP_1, FVSUM_1, VECTSP_2, TARSKI_0, HILBASIS,
XXREAL_0, TOPZARI1, RING_2, IDEAL_2, BOOLE, ORDINAL3, FUNCT_7, RVSUM_1,
UPROOTS, HILB10_5, FIELD_5, CARD_2, BSPACE, POLYNOM9;
schemes FINSEQ_2, NAT_1;
begin :: Preliminaries
reserve A for non degenerated comRing;
reserve R for non degenerated domRing;
reserve n for non empty Ordinal;
reserve o,o1,o2 for object;
reserve X,Y for Subset of Funcs(n,[#]R);
reserve S,T for Subset of Polynom-Ring(n,R);
reserve F,G for FinSequence of the carrier of Polynom-Ring(n,R);
reserve x for Function of n,R;
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p be Polynomial of n,L;
redefine func {p} -> Subset of Polynom-Ring(n,L); :: redefines { (TARSKI, definition)
coherence
proof
for u be object st u in {p} holds
u in the carrier of Polynom-Ring(n,L);
hence thesis;
end;
end;
::$INSERT Enhance eval function: evaluated function is Element of Polynom-Ring.
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr;
let f be Element of Polynom-Ring (n,L), x be Function of n,L;
func E_eval(f,x) -> Element of L means
:Def1:
ex p be Polynomial of n,L st p = f & it = eval(p,x);
existence
proof
f in [#]Polynom-Ring(n,L) by SUBSET_1:def 1; then
f is Polynomial of n,L by POLYNOM1:def 11; then
reconsider p = f as Polynomial of n,L;
consider y be Element of L such that
A1: y = eval(p,x);
thus thesis by A1;
end;
uniqueness;
end;
::$INSERT Enhance E_eval function to evaluate Finite Sequence of Polynomials.
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
F be FinSequence of the carrier of Polynom-Ring(n,L),
x be Function of n,L;
func E_eval(F,x) -> FinSequence of the carrier of L means :Def2:
dom it = dom F & for i be Nat st i in dom F holds it.i = E_eval(F/.i,x);
existence
proof
deffunc G(Nat) = E_eval(F/.$1,x);
ex z being FinSequence of the carrier of L
st len z = len F & for j being Nat st j in dom z holds
z.j = G(j) from FINSEQ_2:sch 1; then
consider z being FinSequence of the carrier of L such that
A1: len z = len F and
A2: for j being Nat st j in dom z holds z.j = G(j);
take z;
thus dom z = dom F by A1,FINSEQ_3:29;
hence thesis by A2;
end;
uniqueness
proof
let it1, it2 be FinSequence of the carrier of L such that
A3: dom it1 = dom F and
A4: for i being Nat st i in dom F holds it1.i = E_eval(F/.i,x) and
A5: dom it2 = dom F and
A6: for i being Nat st i in dom F holds it2.i = E_eval(F/.i,x);
for n being Nat st n in dom it1 holds it1.n = it2.n
proof
let n be Nat;
assume
A7: n in dom it1;
reconsider n as Element of NAT by ORDINAL1:def 12;
it1.n = E_eval(F/.n,x) by A3,A4,A7 .= it2.n by A3,A6,A7;
hence thesis;
end;
hence thesis by A3,A5;
end;
end;
theorem Th1:
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Ordinal holds
Support 0_(n,L) = {}
proof
let L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n be Ordinal;
assume Support 0_(n,L) <> {}; then
consider o such that
A2: o in Support 0_(n,L) by XBOOLE_0:def 1;
reconsider b = o as bag of n by A2;
b in dom 0_(n,L) & (0_(n,L)).b <> 0.L by A2,POLYNOM1:def 3;
hence contradiction by POLYNOM1:22;
end;
theorem Th2:
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, f,g being Element of Polynom-Ring(n,L),
x being Function of n, L holds
E_eval(f+g,x) = E_eval(f,x) + E_eval(g,x)
proof
let n be Ordinal, L be right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, f,g be Element of Polynom-Ring(n,L),
x be Function of n, L;
f in [#]Polynom-Ring(n,L) & g in [#]Polynom-Ring(n,L) by SUBSET_1:def 1;
then
f is Polynomial of n,L & g is Polynomial of n,L by POLYNOM1:def 11; then
consider p,q be Polynomial of n,L such that
A1: p = f & q = g;
A2: f+g = p+q by A1,POLYNOM1:def 11;
A3: E_eval(f,x) = eval(p,x) & E_eval(g,x) = eval(q,x) by A1,Def1;
E_eval(f+g,x) = eval(p+q,x) by A2,Def1
.= E_eval(f,x) + E_eval(g,x) by A3,POLYNOM2:23;
hence thesis;
end;
theorem Th3:
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
f,g being Element of Polynom-Ring(n,L),
x being Function of n, L holds
E_eval(f*g,x) = E_eval(f,x) * E_eval(g,x)
proof
let n be Ordinal, L be right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
f,g be Element of Polynom-Ring(n,L),
x be Function of n, L;
f in [#]Polynom-Ring(n,L) & g in [#]Polynom-Ring(n,L) by SUBSET_1:def 1;
then
f is Polynomial of n,L & g is Polynomial of n,L by POLYNOM1:def 11; then
consider p,q be Polynomial of n,L such that
A1: p = f & q = g;
A2: f*g = p*'q by A1,POLYNOM1:def 11;
A3: E_eval(f,x) = eval(p,x) & E_eval(g,x) = eval(q,x) by A1,Def1;
E_eval(f*g,x) = eval(p*'q,x) by A2,Def1
.= E_eval(f,x) * E_eval(g,x) by A3,POLYNOM2:25;
hence thesis;
end;
theorem Th4:
for N0 be Nat
for n be Ordinal,
L being right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
F be FinSequence of the carrier of Polynom-Ring(n,L),
x be Function of n,L
st len F = N0+1 holds
E_eval(F,x) = (E_eval(F|N0,x))^<*E_eval(F/.(len F),x)*>
proof
let N0 be Nat;
let n be Ordinal,
L be right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
F be FinSequence of the carrier of Polynom-Ring(n,L),
x be Function of n,L;
assume
A1: len F = N0+1; then
A2: dom F = Seg(N0+1) by FINSEQ_1:def 3; then
A3: Seg (N0+1) = dom E_eval(F,x) by Def2
.= Seg len E_eval(F,x) by FINSEQ_1:def 3;
A4: len(F|N0) = min(N0,len F) by FINSEQ_2:21 .= N0 by A1;
A5: Seg(len E_eval(F|N0,x)) = dom E_eval(F|N0,x) by FINSEQ_1:def 3
.= dom (F|N0) by Def2 .= Seg N0 by A4,FINSEQ_1:def 3; then
A6: len E_eval(F|N0,x) = N0 by FINSEQ_1:6;
len <*E_eval(F/.(N0+1),x)*> = 1 by FINSEQ_1:39; then
A8: len (E_eval(F|N0,x)^<*E_eval(F/.(N0+1),x)*>) = N0+1 by A6,FINSEQ_1:22;
for k be Nat st 1 <= k & k <= len E_eval(F,x) holds
E_eval(F,x).k = (E_eval(F|N0,x)^<*E_eval(F/.(len F),x)*>).k
proof
let k be Nat;
assume 1 <= k & k <= len E_eval(F,x); then
k in Seg (N0+1) by A3; then
A11: k in Seg N0 \/ {N0+1} by FINSEQ_1:9;
A13: Seg N0 c= Seg(N0 + 1) by FINSEQ_3:18;
per cases by A11,XBOOLE_0:def 3;
suppose
A12: k in Seg N0; then
A14: k in dom (F|N0) by A4,FINSEQ_1:def 3; then
A15: k in dom E_eval(F|N0,x) by Def2;
A16: k in dom (F|Seg N0) by A12,A4,FINSEQ_1:def 3;
A17: (F|N0)/.k = (F|Seg N0).k by A14,PARTFUN1:def 6
.= F.k by A16,FUNCT_1:47 .= F/.k by A2,A12,A13,PARTFUN1:def 6;
((E_eval(F|N0,x))^<* E_eval(F/.(N0+1),x) *>).k
= (E_eval(F|N0,x)).k by A15,FINSEQ_1:def 7
.= E_eval(F/.k,x) by A17,A14,Def2
.= E_eval(F,x).k by Def2,A2,A12,A13;
hence thesis by A1;
end;
suppose k in {N0+1}; then
A19: k = N0+1 by TARSKI:def 1;
N0+1 = len E_eval(F|N0,x) + 1 by A5,FINSEQ_1:6;
hence thesis by A1,Def2,A2,FINSEQ_1:4,A19;
end;
end;
hence thesis by A1,A3,A8,FINSEQ_1:6;
end;
theorem Th5:
for n be Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
F be FinSequence of the carrier of Polynom-Ring(n,L),
x be Function of n,L
holds E_eval(Sum F,x) = Sum E_eval(F,x)
proof
let n be Ordinal, L be right_zeroed add-associative
right_complementable Abelian well-unital distributive
non trivial commutative associative non empty doubleLoopStr,
F be FinSequence of the carrier of Polynom-Ring(n,L),
x be Function of n,L;
per cases;
suppose
A1: len F = 0; then
A2: F = <*>(the carrier of Polynom-Ring(n,L));
A3: 0.Polynom-Ring(n,L) = 0_(n,L) by POLYNOM1:def 11;
A4: E_eval(Sum F,x) = E_eval(0.Polynom-Ring(n,L),x) by A2,RLVECT_1:43
.= eval(0_(n,L),x) by A3,Def1 .= 0.L by POLYNOM2:20;
Seg len F = dom F by FINSEQ_1:def 3
.= dom E_eval(F,x) by Def2
.= Seg(len E_eval(F,x)) by FINSEQ_1:def 3; then
E_eval(F,x) = <*>(the carrier of L) by A1;
hence thesis by A4,RLVECT_1:43;
end;
suppose
A5: len F <> 0;
for k be non zero Nat holds
len F = k implies E_eval(Sum F,x) = Sum E_eval(F,x)
proof
let k be non zero Nat;
defpred P[Nat] means
for F be FinSequence of the carrier of Polynom-Ring(n,L) st
len F = $1 holds E_eval(Sum F,x) = Sum E_eval(F,x);
A6: P[1]
proof
for F be FinSequence of the carrier of Polynom-Ring(n,L) st
len F = 1 holds E_eval(Sum F,x) = Sum E_eval(F,x)
proof
let F be FinSequence of the carrier of Polynom-Ring(n,L);
assume
A7: len F = 1; then
dom F = Seg 1 by FINSEQ_1:def 3; then
A9: 1 in dom F; then
F.1 in rng F by FUNCT_1:3; then
reconsider o = F.1 as Element of Polynom-Ring(n,L);
F = <*o*> by A7,FINSEQ_1:40; then
A11: Sum F = F.1 by BINOM:3 .= F/.1 by A9,PARTFUN1:def 6;
A12: dom E_eval(F,x) = dom F by Def2 .= Seg 1
by A7,FINSEQ_1:def 3;
set o1 = E_eval(F,x).1;
set o = E_eval(F,x)/.1;
A13: 1 in dom E_eval(F,x) by A12;
A14: dom E_eval(F,x) = dom F by Def2;
E_eval(F,x) = <* o1 *> by A12,FINSEQ_1:def 8 .= <* o *>
by A13,PARTFUN1:def 6; then
Sum E_eval(F,x) = E_eval(F,x).1 by BINOM:3
.= E_eval(Sum F,x) by A11,A13,A14,Def2;
hence thesis;
end;
hence thesis;
end;
A15: for k be non zero Nat holds P[k] implies P[k+1]
proof
let k be non zero Nat;
assume
A16: P[k];
for F be FinSequence of the carrier of Polynom-Ring(n,L)
st len F = k+1 holds E_eval(Sum F,x) = Sum E_eval(F,x)
proof
let F be FinSequence of the carrier of Polynom-Ring(n,L);
assume
A17: len F = k+1; then
consider G be FinSequence of Polynom-Ring(n,L),
d be Element of Polynom-Ring(n,L) such that
A18: F = G^<*d*> by FINSEQ_2:19;
(F|k)^<* F/.len F *> = G^<*d*> by A18,A17,FINSEQ_5:21; then
A20: G = (F|k) & d = F/.len F by FINSEQ_2:17;
A21: k+ 1 = len G + 1 by FINSEQ_2:16,A18,A17;
Sum F = Sum G + d by A18,FVSUM_1:71; then
E_eval(Sum F,x) = E_eval(Sum G,x) + E_eval(d,x) by Th2
.= Sum(E_eval(F|k,x)) + E_eval(F/.len F,x) by A21,A16,A20
.= Sum(E_eval(F|k,x)^<* E_eval(F/.(len F),x) *>) by FVSUM_1:71
.= Sum(E_eval(F,x)) by A17,Th4;
hence thesis;
end;
hence P[k + 1];
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A6,A15);
hence thesis;
end;
hence thesis by A5;
end;
end;
Lm1:
for G be FinSequence of the carrier of R holds
G = (len G)|-> 0.R iff (for i be Nat st i in dom G holds G.i = 0.R)
proof
let G be FinSequence of the carrier of R;
(for i be Nat st i in dom G holds G.i = 0.R) implies G = (len G)|-> 0.R
proof
assume
A2: for i be Nat st i in dom G holds G.i = 0.R;
for k be Nat st 1 <= k & k <= len G holds G.k = ((len G) |-> 0.R).k
proof
let k be Nat;
assume
A4: 1 <= k & k <= len G; then
A6: k in dom ((len G) |-> 0.R);
G.k = 0.R by A2,A4,FINSEQ_3:25
.= ((len G) |-> 0.R).k by A6,FINSEQ_2:57;
hence thesis;
end;
hence thesis;
end;
hence thesis by FINSEQ_2:57;
end;
Lm2: ::: see MATRIX_3 and EUCLID_7, for Element of NAT
for n be Nat holds Sum (n|->0.R) = 0.R
proof
let n be Nat;
defpred P[Nat] means Sum ($1|->0.R) = 0.R;
A1: for n be Nat st P[n] holds P[(n+1)]
proof
let n be Nat;
assume
A2: P[n];
Sum((n+1) |-> 0.R) = Sum ((n |-> 0.R) ^ <*0.R*>) by FINSEQ_2:60
.= 0.R + 0.R by A2,FVSUM_1:71 .= 0.R;
hence thesis;
end;
A3: P[0]
proof
Sum(0|->0.R) = Sum(<*>(the carrier of R)) .=0.R by RLVECT_1:43;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
::$INSERT monic multivariate Polynomials with degree 1.
definition
let n,R;
let a be Function of n,R, i be Element of n;
func deg1Poly(a,i) -> Polynomial of n,R equals
1_1(i,R) - (a.i)|(n,R);
coherence;
end;
theorem Th6:
for a be Element of R,i be Element of n holds
(1_1(i,R)).(UnitBag i) = 1.R & (a|(n,R)).(EmptyBag n) = a &
(1_1(i,R)).(EmptyBag n) = 0.R & (a|(n,R)).(UnitBag i) = 0.R
proof
let a be Element of R, i be Element of n;
set UBi = UnitBag i;
A1: UBi in dom (0_(n,R)) & EmptyBag n in dom (0_(n,R)) by PRE_POLY:def 12;
A2: (1_1(i,R)).(UBi) = (0_(n,R)+*(UBi,1_R)).(UBi) by HILBASIS:def 3
.= 1.R by A1,FUNCT_7:31;
A3: (a|(n,R)).(EmptyBag n)
= (0_(n,R)+*(EmptyBag n,a)).(EmptyBag n) by POLYNOM7:def 8
.= a by A1,FUNCT_7:31;
A4: UBi <> EmptyBag n
proof
(UBi).i <> (EmptyBag n).i by HILBASIS:9;
hence thesis;
end;
A5: (1_1(i,R)).(EmptyBag n)
= (0_(n,R)+*(UBi,1_R)).(EmptyBag n) by HILBASIS:def 3
.= (0_(n,R)).(EmptyBag n) by A4,FUNCT_7:32 .= 0.R;
(a|(n,R)).(UBi) = (0_(n,R)+*(EmptyBag n,a)).(UBi) by POLYNOM7:def 8
.=(0_(n,R)).(UBi) by A4,FUNCT_7:32 .= 0.R;
hence thesis by A2,A3,A5;
end;
theorem
for a be Element of R,i be Element of n holds
1_1(i,R) is Polynomial of n,R & a|(n,R) is Polynomial of n,R;
theorem
for a be non zero Element of R, b be Element of R,i be Element of n holds
(a|(n,R))*'(1_1(i,R)) + b|(n,R) is Polynomial of n,R;
theorem Th9:
for a be Element of R,i be Element of n holds
Support((1_1(i,R)) + a|(n,R)) c= {UnitBag i} \/ {EmptyBag n}
proof
let a be Element of R,i be Element of n;
set p = 1_1(i,R), q = a|(n,R);
set UBi = UnitBag i;
A1: Support p = {UBi} by HILBASIS:13;
A2: Support q = {} or Support q = {EmptyBag n} by POLYNOM7:22;
A5: Support(p+q) c= Support p \/ Support q by POLYNOM1:20;
Support q c= {EmptyBag n} by A2,XBOOLE_0:def 1; then
Support p \/ Support q c= Support p \/ {EmptyBag n} by XBOOLE_1:9;
hence thesis by A1,A5;
end;
theorem Th10:
for n holds degree (EmptyBag n) = 0
proof
let n;
set b = EmptyBag n;
A1: b*canFS(support b) = <*>NAT;
b*canFS(support b) = <*>REAL; then
reconsider f = b*canFS(support b) as FinSequence of REAL;
consider f being FinSequence of NAT such that
A2: 0 = Sum f & f = b*canFS(support b) by RVSUM_1:72,A1;
thus thesis by A2,UPROOTS:def 4;
end;
theorem Th11:
for x be Element of n holds degree(UnitBag x) = 1
proof
let x be Element of n;
set b = UnitBag x;
dom b = n by PARTFUN1:def 2; then
A1: x in dom b by SUBSET_1:def 1;
dom (EmptyBag n) = n by PARTFUN1:def 2; then
A2: x in dom(EmptyBag n) by SUBSET_1:def 1;
A3: b*canFS(support b) = b*canFS({x}) by HILBASIS:8
.= b*<*x*> by FINSEQ_1:94
.= <*b.x*> by A1,FINSEQ_2:34;
b.x in rng b by A1,FUNCT_1:3; then
reconsider f = b*canFS(support b) as FinSequence of NAT by A3,FINSEQ_1:74;
degree b = Sum f by UPROOTS:def 4
.= ((EmptyBag n)+*(x,1)).x by A3,HILBASIS:def 2
.= 1 by A2,FUNCT_7:31;
hence thesis;
end;
theorem
for a be Element of R,i be Element of n holds
degree((1_1(i,R)) + a|(n,R)) = 1
proof
let a be Element of R,i be Element of n;
set p = 1_1(i,R), q = a|(n,R);
set UBi = UnitBag i;
reconsider p0 = p + q as Polynomial of n,R;
A1: Support p0 c= {UBi} \/ {EmptyBag n} by Th9;
dom p0 = Bags n by FUNCT_2:def 1; then
A2: UBi in dom p0 by PRE_POLY:def 12;
p.UBi = 1.R & q.UBi = 0.R by Th6; then
p0.UBi = 1.R + 0.R by POLYNOM1:15 .= 1.R; then
p0.UBi <> 0.R; then
A4: UBi in Support p0 by A2,POLYNOM1:def 3; then
Support p0 <> {} by XBOOLE_0:def 1; then
A5: p0 <> 0_(n,R) by Th1;
A6: for o holds o in Support p0 implies o = UBi or o= EmptyBag n
proof
let o;
assume o in Support p0; then
o in {UBi} or o in {EmptyBag n} by A1,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
A8: for s1 be bag of n st s1 in Support p0 holds
degree s1 <= degree UBi
proof
let s1 be bag of n;
assume s1 in Support p0; then
per cases by A6;
suppose s1 = UBi;
hence thesis;
end;
suppose s1 = EmptyBag n;
hence thesis by Th10;
end;
end;
consider s be bag of n such that
A12: s = UBi;
degree p0 = degree s by A8,A5,A12,A4,HILB10_5:def 3;
hence thesis by A12,Th11;
end;
::$INSERT Enhance function Roots for multivariate Polynomials.
definition ::Zero set of f
let R,n;
let f be Polynomial of n,R;
func Zero_(f) -> Subset of Funcs(n,[#]R) equals
{x where x is Function of n,R : eval(f,x) = 0.R};
coherence
proof
set M = {x where x is Function of n,R : eval(f,x) = 0.R};
M c= Funcs(n,[#]R)
proof
let o be object;
assume o in M; then
consider x being Function of n,R such that
A2: o = x & eval(f,x) = 0.R;
thus thesis by A2,FUNCT_2:8;
end;
hence thesis;
end;
end;
::NdR Fulton69: p.9 (5): V(0) = A^n(k)
theorem Th13:
Zero_(0_(n,R)) = Funcs(n,[#]R)
proof
o in Funcs(n,[#]R) implies o in Zero_(0_(n,R))
proof
assume o in Funcs(n,[#]R); then
consider x be Function such that
A2: o = x & dom x = n & rng x c= [#]R by FUNCT_2:def 2;
reconsider x as Function of n,R by A2,FUNCT_2:2;
eval(0_(n,R),x) = 0.R by POLYNOM2:20;
hence thesis by A2;
end; then
Funcs(n,[#]R) c= Zero_(0_(n,R));
hence thesis;
end;
::NdR Fulton69: p.9 (5): V(1) = {}.
theorem Th14:
Zero_(1_(n,R)) = {}Funcs(n,[#]R)
proof
assume Zero_(1_(n,R)) <> {}Funcs(n,[#]R); then
consider o such that
A2: o in Zero_(1_(n,R)) by XBOOLE_0:def 1;
consider x be Function of n,R such that
A3: o=x & eval(1_(n,R),x) = 0.R by A2;
thus contradiction by A3,POLYNOM2:21;
end;
::1.2 Affine Space and Algebraic Sets
::$INSERT Enhance function Zero_ for set of Polynomials.
definition
let R,n,S;
func Zero_(S) -> Subset of Funcs(n,[#]R) equals
:Def6:
{x where x is Function of n,R : for p be Polynomial of n,R
st p in S holds eval(p,x) = 0.R} if S <> {}
otherwise {};
coherence
proof
set Z = {x where x is Function of n,R : for p be Polynomial of n,R st p in S
holds eval(p,x) = 0.R};
Z c= Funcs(n,[#]R)
proof
let z be object;
assume z in Z; then
consider x be Function of n,R such that
A2: z = x &
for p be Polynomial of n,R st p in S holds eval(p,x) = 0.R;
thus thesis by A2,FUNCT_2:8;
end;
hence thesis by XBOOLE_1:2;
end;
consistency;
end;
theorem Th15:
for p be Polynomial of n,R holds Zero_{p} = Zero_(p)
proof
let p be Polynomial of n,R;
set S = {p};
thus for o holds o in Zero_S implies o in Zero_(p)
proof
let o;
assume o in Zero_S; then
o in {x where x is Function of n,R : for f be Polynomial of n,R
st f in S holds eval(f,x) = 0.R} by Def6; then
consider x be Function of n,R such that
A3: x = o &
for f be Polynomial of n,R st f in S holds eval(f,x) = 0.R;
assume not o in Zero_(p); then
A5: eval(p,x) <> 0.R by A3;
p in S by TARSKI:def 1;
hence contradiction by A5,A3;
end;
thus for o holds o in Zero_(p) implies o in Zero_S
proof
let o;
assume
o in Zero_(p); then
consider x1 be Function of n,R such that
A6: x1 = o & eval(p,x1) = 0.R;
for f be Polynomial of n,R st f in S holds eval(f,x1) = 0.R
by A6,TARSKI:def 1; then
x1 in {x where x is Function of n,R : for f be Polynomial of n,R
st f in S holds eval(f,x) = 0.R};
hence thesis by A6,Def6;
end;
end;
definition
let R,n;
let IT be Subset of Funcs(n,[#]R);
attr IT is algebraic_set_from_ideal means :Def7:
ex I be Ideal of Polynom-Ring(n,R) st IT = Zero_(I);
end;
registration
let R,n;
cluster algebraic_set_from_ideal for non empty Subset of Funcs(n,[#]R);
existence
proof
set M = [#]Funcs(n,[#]R);
Zero_({0.Polynom-Ring(n,R)}) = Zero_({0_(n,R)}) by POLYNOM1:def 11
.= Zero_(0_(n,R)) by Th15 .= M by Th13; then
M is algebraic_set_from_ideal;
hence thesis;
end;
end;
::$INSERT Definition of Algebraic Set.
definition
let n,R;
mode Algebraic_Set of n,R is
algebraic_set_from_ideal Subset of Funcs(n,[#]R);
end;
::NdR Fulton69: p.9 (3): If I c= J then V(J) c= V(I).
theorem Th16:
for S,T be non empty Subset of Polynom-Ring(n,R) holds
S c= T implies Zero_(T) c= Zero_(S)
proof
let S,T be non empty Subset of Polynom-Ring(n,R);
assume
A1: S c= T;
for o holds o in Zero_(T) implies o in Zero_(S)
proof
let o;
assume o in Zero_(T); then
o in {x where x is Function of n,R : for f be Polynomial of n,R
st f in T holds eval(f,x) = 0.R} by Def6; then
consider x being Function of n,R such that
A3: o = x & for f be Polynomial of n,R st f in T holds
eval(f,x) = 0.R;
for f be Polynomial of n,R holds f in S implies eval(f,x) = 0.R
by A1,A3; then
x in {x where x is Function of n,R :
for f be Polynomial of n,R st f in S holds eval(f,x) = 0.R};
hence thesis by A3,Def6;
end;
hence thesis;
end;
::NdR Fulton69: p.9 (1): If I is the ideal in k[x1,...,xn] generated by S....
theorem Th17:
for S be non empty Subset of Polynom-Ring(n,R) holds
Zero_(S) = Zero_(S-Ideal)
proof
let S be non empty Subset of Polynom-Ring(n,R);
A1: S c= S-Ideal by IDEAL_1:def 14;
Zero_(S) c= Zero_(S-Ideal)
proof
set MS = {x where x is Function of n,R : for f be Polynomial of n,R
st f in S holds eval(f,x) = 0.R};
set MI = {x where x is Function of n,R : for f be Polynomial of n,R
st f in S-Ideal holds eval(f,x) = 0.R};
for o holds o in Zero_(S) implies o in Zero_(S-Ideal)
proof
let o;
assume o in Zero_(S); then
o in MS by Def6; then
consider x be Function of n,R such that
A3: o = x & for f be Polynomial of n,R
st f in S holds eval(f,x) = 0.R;
for p be Polynomial of n,R st p in S-Ideal holds eval(p,x) = 0.R
proof
let p be Polynomial of n,R;
assume p in S-Ideal; then
consider F be LinearCombination of S such that
A5: p = Sum F by IDEAL_1:60;
A6: for i being Nat st i in dom E_eval(F,x) holds E_eval(F,x).i = 0.R
proof
let i be Nat;
assume i in dom E_eval(F,x); then
A8: i in dom F by Def2;
consider u,v being Element of Polynom-Ring(n,R),
a being Element of S such that
A9: F/.i = u*a*v by A8,IDEAL_1:def 8;
A10: a in S by SUBSET_1:def 1;
a in Polynom-Ring(n,R) by SUBSET_1:def 1; then
reconsider a1 = a as Polynomial of n,R by POLYNOM1:def 11;
A11: E_eval(a,x) = eval(a1,x) by Def1 .= 0.R by A10,A3;
F/.i = (u*v)*a by A9,GROUP_1:def 3; then
E_eval(F,x).i = E_eval((u*v)*a,x) by A8,Def2
.= E_eval(u*v,x) * 0.R by A11,Th3 .= 0.R;
hence thesis;
end;
A13: Sum E_eval(F,x) = Sum (len(E_eval(F,x))|-> 0.R) by A6,Lm1
.= 0.R by Lm2;
eval(p,x) = E_eval(Sum F,x) by A5,Def1
.= 0.R by A13,Th5;
hence thesis;
end; then
x in MI;
hence thesis by A3,Def6;
end;
hence Zero_(S) c= Zero_(S-Ideal);
end;
hence Zero_(S) = Zero_(S-Ideal) by A1,Th16;
end;
theorem Th18:
for I,J be Ideal of Polynom-Ring(n,R) holds
Zero_(I \/ J) = Zero_(I) /\ Zero_(J)
proof
let I,J be Ideal of Polynom-Ring(n,R);
A1: Zero_(I\/J) c= Zero_(I)/\Zero_(J)
proof
Zero_(I\/J) c= Zero_(J) & Zero_(I\/J) c= Zero_(I) by XBOOLE_1:7,Th16;
hence thesis by XBOOLE_1:19;
end;
Zero_(I) /\ Zero_(J) c= Zero_(I \/ J)
proof
for o holds o in Zero_(I) /\ Zero_(J) implies o in Zero_(I \/ J)
proof
let o;
assume o in Zero_(I) /\ Zero_(J); then
A3: o in Zero_(I) & o in Zero_(J) by XBOOLE_0:def 4; then
o in {x where x is Function of n,R : for f be Polynomial of n,R
st f in J holds eval(f,x) = 0.R} by Def6; then
consider x being Function of n,R such that
A4: o = x & for f be Polynomial of n,R holds
f in J implies eval(f,x) = 0.R;
o in {x where x is Function of n,R : for f be Polynomial of n,R
st f in I holds eval(f,x) = 0.R} by A3, Def6; then
consider y being Function of n,R such that
A5: o = y &
for g be Polynomial of n,R holds
g in I implies eval(g,y) = 0.R;
o in Zero_(I \/ J)
proof
assume not o in Zero_(I \/ J); then
A7: not o in {x where x is Function of n,R :
for f be Polynomial of n,R
st f in I\/J holds eval(f,x) = 0.R} by Def6;
consider f be Polynomial of n,R such that
A8: f in I \/ J & eval(f,x) <> 0.R by A4,A7;
per cases by A8,XBOOLE_0:def 3;
suppose f in J;
hence contradiction by A8,A4;
end;
suppose f in I;
hence contradiction by A8,A4,A5;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th19:
for S,T be Algebraic_Set of n,R holds S /\ T is Algebraic_Set of n,R
proof
let S,T be Algebraic_Set of n,R;
consider I be Ideal of Polynom-Ring(n,R) such that
A1: S = Zero_(I) by Def7;
consider J be Ideal of Polynom-Ring(n,R) such that
A2: T = Zero_(J) by Def7;
reconsider Z = I \/ J as non empty Subset of Polynom-Ring(n,R);
reconsider M = Z-Ideal as Ideal of Polynom-Ring(n,R);
S /\ T = Zero_(I \/ J) by A1,A2,Th18
.= Zero_(Z-Ideal) by Th17; then
S /\ T is algebraic_set_from_ideal;
hence thesis;
end;
Lm3:
for F be non empty Subset of Ideals(A) holds
union F is non empty Subset of A
proof
let F be non empty Subset of Ideals(A);
consider I be object such that
A1: I in F by XBOOLE_0:def 1;
I in Ideals(A) by A1; then
I in the set of all J where J is Ideal of A by RING_2:def 3; then
consider I1 be Ideal of A such that
A2: I = I1;
0.A in I1 by IDEAL_1:2; then
A3: 0.A in union F by A1,A2,TARSKI:def 4;
for I be set st I in F holds I c= [#]A
proof
let I be set;
assume I in F; then
I in Ideals(A); then
I in the set of all J where J is Ideal of A by RING_2:def 3; then
consider I1 be Ideal of A such that
A5: I = I1;
thus thesis by A5;
end;
hence thesis by A3,XBOOLE_0:def 1,ZFMISC_1:76;
end;
definition
let A;
let F be non empty Subset of Ideals(A);
redefine func union F -> non empty Subset of A; :: redefines union (TARSKI, definition)
coherence by Lm3;
end;
::NdR Fulton69: p.9(2):If {Ij} is any collection of ideals then V(\/Ij)=/\V(Ij)
theorem
for F be non empty Subset of Ideals(Polynom-Ring(n,R)) holds
Zero_(union F) = meet{Zero_I where I is Ideal of Polynom-Ring(n,R): I in F}
proof
let F be non empty Subset of Ideals(Polynom-Ring(n,R));
set PR = Polynom-Ring(n,R);
set M = {Zero_I where I is Ideal of PR: I in F};
consider I be object such that
A1: I in F by XBOOLE_0:def 1;
I in Ideals(PR) by A1; then
I in the set of all J where J is Ideal of PR by RING_2:def 3; then
consider I1 be Ideal of PR such that
A2: I = I1;
Zero_I1 in M by A1,A2; then
A3: M <> {} by XBOOLE_0:def 1;
A4: for o holds o in Zero_(union F) implies o in meet M
proof
let o;
assume o in Zero_(union F); then
o in {x where x is Function of n,R : for p be Polynomial of n,R
st p in union F holds eval(p,x) = 0.R} by Def6; then
consider x be Function of n,R such that
A6: x = o &
for p be Polynomial of n,R st p in union F holds eval(p,x) = 0.R;
for Z being set holds Z in M implies o in Z
proof
let Z be set;
assume Z in M; then
consider I be Ideal of PR such that
A8: Z = Zero_I & I in F;
A9: I c= union F by A8,ZFMISC_1:74;
for p1 be Polynomial of n,R st p1 in I holds eval(p1,x) = 0.R
by A6,A9; then
x in {x where x is Function of n,R : for p be Polynomial of n,R
st p in I holds eval(p,x) = 0.R};
hence thesis by A8, A6,Def6;
end;
hence thesis by A3,SETFAM_1:def 1;
end;
for o holds o in meet M implies o in Zero_(union F)
proof
let o;
assume
A10: o in meet M;
Zero_I1 in M by A1,A2; then
A11: meet M c= Zero_I1 by SETFAM_1:3;
A12: meet M c= Funcs(n,[#]R) by A11,XBOOLE_1:1;
consider x be Function such that
A13: o = x & dom x = n & rng x c= [#]R by A10,A12,FUNCT_2:def 2;
reconsider x as Function of n,R by A13,FUNCT_2:2;
for p be Polynomial of n,R st p in union F holds eval(p,x) = 0.R
proof
let p be Polynomial of n,R;
assume p in union F; then
consider Ip be set such that
A15: p in Ip & Ip in F by TARSKI:def 4;
Ip in Ideals(PR) by A15; then
Ip in the set of all J where J is Ideal of PR by RING_2:def 3; then
consider I be Ideal of PR such that
A16: I = Ip;
Zero_I in M by A15,A16; then
o in Zero_I by A3,A10,SETFAM_1:def 1;then
o in {x where x is Function of n,R : for p be Polynomial of n,R
st p in I holds eval(p,x) = 0.R} by Def6; then
consider y be Function of n,R such that
A17: y = o & for f be Polynomial of n,R st f in I holds eval(f,y)=0.R;
thus thesis by A17,A15,A16,A13;
end; then
x in {x where x is Function of n,R : for p be Polynomial of n,R
st p in union F holds eval(p,x) = 0.R};
hence thesis by A13,Def6;
end;
hence thesis by TARSKI:2,A4;
end;
::NdR Fulton69:p.9 (4): V(FG) = V(F) \/ V(G)
theorem Th21:
for f,g be Polynomial of n,R holds Zero_({f*'g}) = Zero_({f}) \/ Zero_({g})
proof
let f,g be Polynomial of n,R;
A1: o in Zero_({f*'g}) implies o in Zero_({f}) \/ Zero_({g})
proof
assume o in Zero_({f*'g}); then
o in Zero_(f*'g) by Th15; then
consider x be Function of n,R such that
A4: x = o & eval(f*'g,x) = 0.R;
reconsider x1 = eval(f,x) as Element of R;
reconsider x2 = eval(g,x) as Element of R;
A5: 0.R = x1 * x2 by A4,POLYNOM2:25;
:::Integral Domain requires
eval(f,x) = 0.R or eval(g,x) = 0.R by A5,VECTSP_2:def 1; then
o in Zero_(f) or o in Zero_(g) by A4; then
o in Zero_({f}) or o in Zero_({g}) by Th15;
hence thesis by XBOOLE_0:def 3;
end;
o in Zero_({f}) \/ Zero_({g}) implies o in Zero_({f*'g})
proof
assume o in Zero_({f}) \/ Zero_({g}); then
o in Zero_({f}) or o in Zero_({g}) by XBOOLE_0:def 3; then
per cases by Th15;
suppose o in Zero_(f); then
consider x be Function of n,R such that
A10: o = x & eval(f,x) = 0.R;
reconsider x1 = eval(g,x) as Element of R;
eval(f*'g,x) = 0.R * x1 by A10,POLYNOM2:25 .= 0.R; then
o in Zero_(f*'g) by A10;
hence thesis by Th15;
end;
suppose o in Zero_(g); then
consider x be Function of n,R such that
A13: o = x & eval(g,x) = 0.R;
reconsider x1 = eval(f,x) as Element of R;
eval(f*'g,x) = x1 * 0.R by A13,POLYNOM2:25 .= 0.R; then
o in Zero_(f*'g) by A13;
hence thesis by Th15;
end;
end;
hence thesis by A1,TARSKI_0:2;
end;
theorem Th22:
for I,J be Ideal of Polynom-Ring(n,R) holds
Zero_(I /\ J) = Zero_(I) \/ Zero_(J)
proof
let I,J be Ideal of Polynom-Ring(n,R);
A1: Zero_I c= Zero_(I /\ J) & Zero_J c= Zero_(I /\ J) by Th16,XBOOLE_1:17;
for o holds o in Zero_(I /\ J) implies o in (Zero_(I) \/ Zero_(J))
proof
let o;
assume o in Zero_(I /\ J); then
o in {x where x is Function of n,R : for p be Polynomial of n,R
st p in I /\ J holds eval(p,x) = 0.R} by Def6; then
consider x1 be Function of n,R such that
A3: o = x1 &
for p be Polynomial of n,R st p in I /\ J holds eval(p,x1) = 0.R;
x1 in (Zero_(I) \/ Zero_(J))
proof
assume not x1 in (Zero_(I) \/ Zero_(J)); then
A5: not x1 in Zero_(I) & not x1 in Zero_(J) by XBOOLE_0:def 3;
not x1 in {z where z is Function of n,R: for f be Polynomial of n,R
st f in I holds eval(f,z) = 0.R} by A5,Def6; then
consider f1 be Polynomial of n,R such that
A6: f1 in I & eval(f1,x1) <> 0.R;
not x1 in {z where z is Function of n,R: for f be Polynomial of n,R
st f in J holds eval(f,z) = 0.R} by A5,Def6; then
consider f2 be Polynomial of n,R such that
A7: f2 in J & eval(f2,x1) <> 0.R;
A8: eval(f1*'f2,x1) = eval(f1,x1)*eval(f2,x1) by POLYNOM2:25;
reconsider F1 = f1, F2 = f2 as Element of Polynom-Ring(n,R)
by POLYNOM1:def 11;
A9: F1*F2 = f1*'f2 by POLYNOM1:def 11;
A10: F1*F2 in I & F1*F2 in J by A6,A7,IDEAL_1:def 2;
f1*'f2 in I/\J by A9,A10;
hence contradiction by A3,A8,A6,A7,VECTSP_2:def 1;
end;
hence thesis by A3;
end; then
Zero_(I /\ J) c= Zero_(I) \/ Zero_(J);
hence thesis by A1,XBOOLE_1:8;
end;
theorem
for I,J be Ideal of Polynom-Ring(n,R) holds
Zero_(I*'J) = Zero_(I) \/ Zero_(J)
proof
let I,J be Ideal of Polynom-Ring(n,R);
set PR = Polynom-Ring(n,R);
A1: Zero_(I/\J) c= Zero_(I*'J) by Th16,IDEAL_1:79;
for o holds o in Zero_(I*'J) implies o in (Zero_(I) \/ Zero_(J))
proof
let o;
assume o in Zero_(I*'J); then
o in {x where x is Function of n,R : for p be Polynomial of n,R
st p in I*'J holds eval(p,x) = 0.R} by Def6; then
consider x1 be Function of n,R such that
A3: o = x1 &
for p be Polynomial of n,R st p in I*'J holds eval(p,x1) = 0.R;
x1 in (Zero_(I) \/ Zero_(J))
proof
assume not x1 in (Zero_(I) \/ Zero_(J)); then
A5: not x1 in Zero_(I) & not x1 in Zero_(J) by XBOOLE_0:def 3; then
not x1 in {z where z is Function of n,R: for f be Polynomial of n,R
st f in I holds eval(f,z) = 0.R} by Def6; then
consider f1 be Polynomial of n,R such that
A6: f1 in I & eval(f1,x1) <> 0.R;
not x1 in {z where z is Function of n,R: for f be Polynomial of n,R
st f in J holds eval(f,z) = 0.R} by A5,Def6; then
consider f2 be Polynomial of n,R such that
A7: f2 in J & eval(f2,x1) <> 0.R;
reconsider F1=f1,F2=f2 as Element of Polynom-Ring(n,R) by POLYNOM1:def 11;
A8: F1*F2 =f1*'f2 by POLYNOM1:def 11;
reconsider s1 = <* F1*F2 *> as FinSequence of the carrier of PR;
dom s1 = Seg 1 by FINSEQ_1:def 8; then
A10: len s1 = 1 by FINSEQ_1:def 3;
A11: Sum s1 = F1*F2 by BINOM:3;
set M = { Sum s where s is FinSequence of the carrier of PR :
for i being Element of NAT st 1 <= i & i <= len s ex a,b being
Element of PR st s.i = a*b & a in I & b in J};
for i being Element of NAT st 1 <= i & i <= len s1 ex a,b being
Element of PR st s1.i = a*b & a in I & b in J
proof
let i be Element of NAT;
assume 1 <= i & i <= len s1; then
A13: i = 1 by A10,XXREAL_0:1;
consider a,b be Element of PR such that
A14: a = F1 & b = F2 & s1.i = a*b & a in I & b in J by A6,A7,A13;
thus thesis by A14;
end; then
f1*'f2 in I*'J by A8,A11; then
0.R = eval(f1*'f2,x1) by A3.= eval(f1,x1)*eval(f2,x1) by POLYNOM2:25;
hence contradiction by A6,A7,VECTSP_2:def 1;
end;
hence thesis by A3;
end; then
Zero_(I*'J) c= Zero_(I) \/ Zero_(J);
hence thesis by A1,Th22;
end;
definition let n,R;
func Alg_Sets(n,R) -> set equals
{S where S is Subset of Funcs(n,[#]R): S is Algebraic_Set of n,R };
coherence;
end;
::NdR Fulton69: p.9 (4)-any finite union of algebraic sets is an algebraic set.
theorem Th24:
for m be non zero Nat, F be Subset of Alg_Sets(n,R) holds
card F = m implies union F is Algebraic_Set of n,R
proof
let m be non zero Nat, F be Subset of Alg_Sets(n,R);
defpred P[Nat] means
for G be Subset of Alg_Sets(n,R) holds
card G = $1 implies union G is Algebraic_Set of n,R;
A1: for m be non zero Nat st P[m] holds P[(m+1)]
proof
let m be non zero Nat;
assume
A2: P[m];
for G be Subset of Alg_Sets(n,R) holds
card G = m+1 implies union G is Algebraic_Set of n,R
proof
let G be Subset of Alg_Sets(n,R);
assume
A3: card G = m+1; then
G <> {}; then
consider o such that
A4: o in G by XBOOLE_0:def 1;
o in {S where S is Subset of [#]Funcs(n,[#]R):
S is Algebraic_Set of n,R } by A4; then
consider S be Subset of [#]Funcs(n,[#]R) such that
A5: o = S & S is Algebraic_Set of n,R;
A6: G is finite by A3;
reconsider G1 = G \ {S} as finite Subset of Alg_Sets(n,R) by A6;
A7: not S in G1 by ZFMISC_1:56;
A8: m+1 = card (G1 \/ {S}) by A3,A4,A5,ZFMISC_1:31,FIELD_5:1
.= card G1 + 1 by A7,CARD_2:41;
union G1 is Algebraic_Set of n,R by A2,A8; then
consider I be Ideal of Polynom-Ring(n,R) such that
A9: union G1 = Zero_(I) by Def7;
consider J be Ideal of Polynom-Ring(n,R) such that
A10: S = Zero_(J) by A5,Def7;
A11: Zero_(I /\ J) = union G1 \/ S by A9,A10,Th22
.= union G1 \/ union {S} by ZFMISC_1:25
.= union (G1 \/ {S}) by ZFMISC_1:78;
consider I1 be Ideal of Polynom-Ring(n,R) such that
A12: I1 = I /\ J;
Zero_I1 = union G by A11,A4,A5,ZFMISC_1:31,FIELD_5:1,A12;
hence thesis by Def7;
end;
hence thesis;
end;
A14: P[1]
proof
for G be Subset of Alg_Sets(n,R) holds
card G = 1 implies union G is Algebraic_Set of n,R
proof
let G be Subset of Alg_Sets(n,R);
assume card G = 1; then
consider o being object such that
A16: G = {o} by CARD_2:42;
o in G by A16,TARSKI:def 1; then
o in {S where S is Subset of Funcs(n,[#]R):
S is Algebraic_Set of n,R }; then
consider S be Subset of Funcs(n,[#]R) such that
A20: o = S & S is Algebraic_Set of n,R;
thus thesis by A16,A20,ZFMISC_1:25;
end;
hence thesis;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A14,A1);
hence thesis;
end;
Lm4:
Zero_([#]Polynom-Ring(n,R)) = {}Funcs(n,[#]R)
proof
Zero_([#]Polynom-Ring(n,R))
= Zero_({1.Polynom-Ring(n,R)}-Ideal) by RING_2:20
.= Zero_({1.Polynom-Ring(n,R)}) by Th17
.= Zero_({1_(n,R)}) by POLYNOM1:31
.= Zero_(1_(n,R)) by Th15
.= {}Funcs(n,[#]R) by Th14;
hence thesis;
end;
definition
let n,R;
let a be Function of n,R;
func polyset(a) -> non empty Subset of Polynom-Ring(n,R) equals
{f where f is Polynomial of n,R:
ex i be Element of n st f = deg1Poly(a,i)};
coherence
proof
set M = {f where f is Polynomial of n,R:
ex i be Element of n st f = deg1Poly(a,i)};
now
let u be object;
assume u in M; then
consider f be Polynomial of n,R such that
A2: u = f & ex i being Element of n st f = deg1Poly(a,i);
thus u in [#]Polynom-Ring(n,R) by A2,POLYNOM1:def 11;
end; then
reconsider M as Subset of Polynom-Ring(n,R) by TARSKI:def 3;
M is non empty
proof
reconsider k=0 as Element of n by ORDINAL3:8;
deg1Poly(a,k) in M;
hence thesis;
end;
hence thesis;
end;
end;
::NdR Fulton69: p.9 (5): V(x_1-a_1,x_2-a_2,...x_n-a_n) = {(a_1,...a_n)}.
theorem Th25:
for a be Function of n,R holds Zero_(polyset(a)) = {a}
proof
let a be Function of n,R;
thus o in Zero_(polyset(a)) implies o in {a}
proof
assume
A2: o in Zero_(polyset(a)); then
consider x be Function such that
A4: o = x & dom x = n & rng x c= [#]R by FUNCT_2:def 2;
assume
A3: not o in {a};
reconsider x as Function of n,R by A4,FUNCT_2:2;
A5: dom a = n by FUNCT_2:def 1 .= dom x by FUNCT_2:def 1;
x <> a by A4,A3,TARSKI:def 1; then
consider i be object such that
A6: i in dom a & x.i <> a.i by A5;
reconsider i0 = i as Element of n by A6;
reconsider f0 = deg1Poly(a,i0) as Polynomial of n,R;
A7: f0 in polyset(a);
A8: eval(f0,x) = eval(1_1(i0,R),x) - eval((a.i0)|(n,R),x) by POLYNOM2:24
.= x.i0 - eval((a.i0)|(n,R),x) by HILB10_3:1
.= x.i0 - (a.i0) by POLYNOM7:25;
not x in Zero_(polyset(a))
proof
assume x in Zero_(polyset(a)); then
x in {x where x is Function of n,R : for p be Polynomial of n,R
st p in polyset(a) holds eval(p,x) = 0.R} by Def6; then
consider x0 be Function of n,R such that
A10: x0 = x & for f be Polynomial of n,R
st f in polyset(a) holds eval(f,x0) = 0.R;
thus contradiction by RLVECT_1:21,A6,A8,A7,A10;
end;
hence contradiction by A2,A4;
end;
thus o in {a} implies o in Zero_(polyset(a))
proof
assume o in {a}; then
A12: o = a by TARSKI:def 1;
for f be Polynomial of n,R st f in polyset(a) holds eval(f,a) = 0.R
proof
let f be Polynomial of n,R;
assume f in polyset(a); then
consider f0 be Polynomial of n,R such that
A14: f0 = f & ex i be Element of n st f0 = deg1Poly(a,i);
consider i0 be Element of n such that
A15: f0 = deg1Poly(a,i0) by A14;
eval(f0,a)
= eval(1_1(i0,R),a) - eval((a.i0)|(n,R),a) by A15,POLYNOM2:24
.= a.i0 - eval((a.i0)|(n,R),a) by HILB10_3:1
.= a.i0 - a.i0 by POLYNOM7:25
.= 0.R by RLVECT_1:15;
hence thesis by A14;
end; then
a in {x where x is Function of n,R :
for f be Polynomial of n,R st f in polyset(a) holds eval(f,x)=0.R};
hence thesis by A12, Def6;
end;
end;
theorem Th26:
for x be Element of Funcs(n,[#]R) holds {x} is Algebraic_Set of n,R
proof
let x be Element of Funcs(n,[#]R);
x in Funcs(n,[#]R) by SUBSET_1:def 1; then
consider x1 be Function such that
A1: x1 = x & dom x1 = n & rng x1 c= [#]R by FUNCT_2:def 2;
reconsider x1 as Function of n,R by A1;
A2: {x1} = Zero_(polyset(x1)) by Th25 .= Zero_((polyset(x1))-Ideal) by Th17;
reconsider Q = {x} as non empty Subset of Funcs(n,[#]R);
Q is algebraic_set_from_ideal by A2,A1;
hence thesis;
end;
::NdR Fulton69: p.9 (5): any finite subset A^n(k) is an algebaic set.
theorem
for m be non zero Nat, P be Subset of singletons(Funcs(n,[#]R)) holds
card P = m implies union P is Algebraic_Set of n,R
proof
let m be non zero Nat, P be Subset of singletons(Funcs(n,[#]R));
assume
A1: card P = m;
A2: singletons(Funcs(n,[#]R)) c= Alg_Sets(n,R)
proof
for o holds o in singletons(Funcs(n,[#]R)) implies o in Alg_Sets(n,R)
proof
let o;
assume o in singletons(Funcs(n,[#]R)); then
o in { S where S is Subset of Funcs(n,[#]R) : S is 1-element }
by BSPACE:def 8; then
consider S be Subset of Funcs(n,[#]R) such that
A4: o = S & S is 1-element;
consider p be Element of Funcs(n,[#]R) such that
A5: S = {p} by A4,CARD_1:65;
S is Algebraic_Set of n,R by A5,Th26;
hence thesis by A4;
end;
hence thesis;
end;
P c= Alg_Sets(n,R) by A2;
hence thesis by A1,Th24;
end;
::$INSERT The Ideal of a Set of Points.
definition
let R, n, X;
func Ideal_X -> non empty Subset of Polynom-Ring(n,R) equals
{f where f is Polynomial of n,R : X c= Zero_(f)};
coherence
proof
set M = {f where f is Polynomial of n,R : X c= Zero_(f)};
A1: M c= [#]Polynom-Ring(n,R)
proof
let o be object;
assume o in M; then
consider x being Polynomial of n,R such that
A3: o = x & X c= Zero_(x);
thus thesis by A3,POLYNOM1:def 11;
end;
M <> {}
proof
A4: Zero_(0_(n,R)) = Funcs(n,[#]R) by Th13;
0_(n,R) in {f where f is Polynomial of n,R : X c= Zero_(f)} by A4;
hence thesis by XBOOLE_0:def 1;
end;
hence thesis by A1;
end;
end;
Lm5:
for p, q being Element of Polynom-Ring(n,R) holds
p in Ideal_X & q in Ideal_X implies p + q in Ideal_X
proof
set M = {f where f is Polynomial of n,R : X c= Zero_(f)};
let p,q be Element of Polynom-Ring(n,R);
assume
A1: p in Ideal_X & q in Ideal_X; then
consider f be Polynomial of n,R such that
A2: f = p & X c= Zero_(f);
consider g be Polynomial of n,R such that
A3: g = q & X c= Zero_(g) by A1;
for y be object st y in X holds y in Zero_(f+g)
proof
let y be object;
assume y in X; then
A5: y in {x where x is Function of n,R : eval(f,x) = 0.R} &
y in {x where x is Function of n,R : eval(g,x) = 0.R} by A2,A3; then
consider x1 be Function of n,R such that
A6: y = x1 & eval(f,x1) = 0.R;
consider x2 be Function of n,R such that
A7: y = x2 & eval(g,x2) = 0.R by A5;
eval(f+g,x1) = 0.R + 0.R by A7,A6,POLYNOM2:23 .= 0.R;
hence thesis by A6;
end; then
X c= Zero_(f + g); then
f + g in Ideal_X;
hence thesis by A2,A3,POLYNOM1:def 11;
end;
Lm6:
for a, p being Element of Polynom-Ring(n,R) st p in Ideal_X holds
a*p in Ideal_X
proof
let a,p be Element of Polynom-Ring(n,R);
assume
A1: p in Ideal_X;
p in [#]Polynom-Ring(n,R) by SUBSET_1:def 1; then
reconsider a1 = a as Polynomial of n,R by POLYNOM1:def 11;
consider f be Polynomial of n,R such that
A2: f = p & X c= Zero_(f) by A1;
for y be object st y in X holds y in Zero_(a1*'f)
proof
let y be object;
assume y in X; then
y in {x where x is Function of n,R : eval(f,x) = 0.R} by A2; then
consider x1 be Function of n,R such that
A4: y = x1 & eval(f,x1) = 0.R;
eval(a1*'f,x1) = eval(a1,x1)* 0.R by A4,POLYNOM2:25 .= 0.R;
hence thesis by A4;
end; then
X c= Zero_(a1*'f); then
a1*'f in Ideal_X;
hence thesis by A2,POLYNOM1:def 11;
end;
Lm7:
for a, p being Element of Polynom-Ring(n,R) st p in Ideal_X holds
p*a in Ideal_X by Lm6;
theorem
for X holds Ideal_X is Ideal of Polynom-Ring(n,R)
proof
let X;
A1: Ideal_X is add-closed by Lm5;
Ideal_X is right-ideal by Lm7;
hence thesis by A1;
end;
registration
let R, n, X;
cluster Ideal_X -> add-closed for Subset of Polynom-Ring(n,R);
coherence by Lm5;
cluster Ideal_X -> right-ideal for Subset of Polynom-Ring(n,R);
coherence by Lm7;
end;
::NdR Fulton69: p.11 (6): if X c= Y, then I(Y) c= I(X)
theorem Th29:
X c= Y implies Ideal_Y c= Ideal_X
proof
assume
A1: X c= Y;
o in Ideal_Y implies o in Ideal_X
proof
assume o in Ideal_Y; then
consider f be Polynomial of n,R such that
A3: f = o & Y c= Zero_(f);
X c= Zero_(f) by A3,A1;
hence thesis by A3;
end;
hence thesis;
end;
::NdR Fulton69: p.11 (7): I({}) = k[x_1,...,x_n]
theorem Th30:
X = {} iff Ideal_X = [#]Polynom-Ring(n,R)
proof
A1: X = {} implies Ideal_X = [#]Polynom-Ring(n,R)
proof
assume
A2: X = {};
o in [#]Polynom-Ring(n,R) implies o in Ideal_X
proof
assume o in [#]Polynom-Ring(n,R); then
reconsider f = o as Polynomial of n,R by POLYNOM1:def 11;
{} c= Zero_(f) by XBOOLE_1:2;
hence thesis by A2;
end; then
[#]Polynom-Ring(n,R) c= Ideal_X;
hence thesis;
end;
Ideal_X = [#]Polynom-Ring(n,R) implies X = {}Funcs(n,[#]R)
proof
assume
A4: Ideal_X = [#]Polynom-Ring(n,R);
assume X <> {}Funcs(n,[#]R); then
consider o such that
A6: o in X by XBOOLE_0:def 1;
reconsider x = o as Element of Funcs(n,[#]R) by A6;
A7: Ideal_{x} = [#]Polynom-Ring(n,R) by A4,Th29,A6,ZFMISC_1:31;
reconsider y = x as Function of n,R;
1.Polynom-Ring(n,R) in [#]Polynom-Ring(n,R) by SUBSET_1:def 1;
then
1_(n,R) in {f where f is Polynomial of n,R : {x} c= Zero_(f)}
by A7, POLYNOM1:31; then
consider g be Polynomial of n,R such that
A9: g = 1_(n,R) & {x} c= Zero_(g);
{x} c= {}Funcs(n,[#]R) by A9,Th14;
hence contradiction;
end;
hence thesis by A1;
end;
::NdR Fulton69: p 11 (7): I(A^n(k)) = (0) (only (0) c= I(A^n(k)))
theorem
{0.Polynom-Ring(n,R)} c= Ideal_([#]Funcs(n,[#]R))
proof
o in {0.Polynom-Ring(n,R)} implies o in Ideal_([#]Funcs(n,[#]R))
proof
assume o in {0.Polynom-Ring(n,R)}; then
A2: o = 0.Polynom-Ring(n,R) by TARSKI:def 1
.= 0_(n,R) by POLYNOM1:def 11;
Zero_(0_(n,R)) = Funcs(n,[#]R) by Th13;
hence thesis by A2;
end;
hence thesis;
end;
::NdR Fulton69: p.11 (8): S c= I(V(S))
theorem Th32:
S c= Ideal_(Zero_(S))
proof
for o holds o in S implies o in Ideal_(Zero_(S))
proof
let o;
assume
A1: o in S; then
A2: S <> {} by XBOOLE_0:def 1;
reconsider p = o as Polynomial of n,R by A1,POLYNOM1:def 11;
assume not o in Ideal_(Zero_(S)); then
not Zero_(S) c= Zero_(p); then
consider z be object such that
A4: z in Zero_(S) and
A5: not z in Zero_(p);
z in {x where x is Function of n,R :
for f be Polynomial of n,R st f in S holds eval(f,x) = 0.R}
by A2,A4,Def6; then
consider x be Function of n,R such that
A6: x = z and
A7: for f be Polynomial of n,R st f in S holds eval(f,x) = 0.R;
eval(p,x) = 0.R by A1,A7;
hence contradiction by A5, A6;
end;
hence thesis;
end;
::NdR Fulton69: p.11 (8): X c= V(I(X))
theorem Th33:
X c= Zero_(Ideal_X)
proof
for o holds o in X implies o in Zero_(Ideal_X)
proof
let o;
assume
A1: o in X; then
reconsider X as non empty Subset of Funcs(n,[#]R) by XBOOLE_0:def 1;
consider x be Function such that
A2: o = x & dom x = n & rng x c= [#]R by A1,FUNCT_2:def 2;
reconsider x as Function of n,R by A2,FUNCT_2:2;
o in Zero_(Ideal_X)
proof
assume not o in Zero_(Ideal_X); then
not o in {z where z is Function of n,R :for f be Polynomial of n,R
st f in Ideal_X holds eval(f,z) = 0.R} by Def6; then
consider f1 be Polynomial of n,R such that
A4: f1 in Ideal_X & eval(f1,x) <> 0.R by A2;
consider f2 be Polynomial of n,R such that
A5: f1 = f2 & X c= Zero_(f2) by A4;
o in Zero_(f1) by A1,A5; then
consider x1 be Function of n,R such that
A6: x1 = o & eval(f1,x1) = 0.R;
thus contradiction by A2,A4,A6;
end;
hence thesis;
end;
hence thesis;
end;
::NdR Fulton69: p.11 (9): V(I(V(S))) = V(S)
theorem Th34:
Zero_(Ideal_(Zero_S)) = Zero_S
proof
per cases;
suppose S <> {}; then
reconsider S as non empty Subset of Polynom-Ring(n,R);
Zero_S c= Zero_(Ideal_(Zero_S)) by Th33;
hence thesis by Th16,Th32;
end;
suppose
A3: S = {}; then
Zero_(Ideal_(Zero_S)) = Zero_([#]Polynom-Ring(n,R)) by Def6, Th30
.= {}Funcs(n,[#]R) by Lm4 .= Zero_S by Def6,A3;
hence thesis;
end;
end;
::NdR Fulton69: p.11 (9): I(V(I(X))) = I(X)
theorem
Ideal_(Zero_(Ideal_X)) = Ideal_X by Th32,Th29,Th33;
::NdR Fulton69: p.11 (9): V=V(I(V)) if V is an algebraic set.
theorem Th36:
for X be Algebraic_Set of n,R holds X = Zero_(Ideal_X)
proof
let X be Algebraic_Set of n,R;
consider I be Ideal of Polynom-Ring(n,R) such that
A1: X = Zero_(I) by Def7;
thus thesis by A1,Th34;
end;
theorem
for V,W be Algebraic_Set of n,R holds V = W iff Ideal_V = Ideal_W
proof
let V,W be Algebraic_Set of n,R;
Ideal_V = Ideal_W implies V = W
proof
assume Ideal_V = Ideal_W; then
V = Zero_(Ideal_W) by Th36 .= W by Th36;
hence thesis;
end;
hence thesis;
end;
::NdR Fulton69: p.11 (6): case of strict subset.
theorem Th38:
for X,Y be Algebraic_Set of n,R holds X c< Y implies Ideal_Y c< Ideal_X
proof
let X,Y be Algebraic_Set of n,R;
assume
A1: X c< Y;
Ideal_X <> Ideal_Y
proof
assume Ideal_X = Ideal_Y; then
X = Zero_(Ideal_Y) by Th36 .= Y by Th36;
hence contradiction by A1;
end;
hence thesis by A1,Th29;
end;
Lm8:
for p be Polynomial of n,R
for i be non zero Nat holds Zero_({p`^i}) = Zero_({p})
proof
let p be Polynomial of n,R;
defpred P[Nat] means Zero_({p`^$1}) = Zero_({p});
A1: now
let i be non zero Nat;
assume
A2: P[i];
reconsider p1 = p`^i as Polynomial of n,R;
Zero_({p`^(i+1)}) = Zero_({p1*'p}) by POLYNOM9:29
.= Zero_({p}) \/ Zero_({p}) by A2,Th21
.= Zero_({p});
hence P[i+1];
end;
reconsider p1=p as Element of Polynom-Ring(n,R) by POLYNOM1:def 11;
p`^1 = p1|^1 by BINOM:def 2 .= p by BINOM:8; then
A4: P[1];
thus for i be non zero Nat holds P[i] from NAT_1:sch 10(A4,A1);
end;
::NdR Fulton69: p.11 (10): I(X) is a radical ideal for any set X c= A^n(k).
theorem
sqrt(Ideal_X) = Ideal_X
proof
per cases;
suppose X <> {}; then
Ideal_X <> [#]Polynom-Ring(n,R) by Th30; then
reconsider IX = Ideal_X as proper Ideal of Polynom-Ring(n,R)
by SUBSET_1:def 6;
A4: not 1.Polynom-Ring(n,R) in IX by IDEAL_1:19;
sqrt(Ideal_X) c= Ideal_X
proof
now let o;
assume o in sqrt(Ideal_X); then
consider f be Element of Polynom-Ring(n,R) such that
A5: f = o & ex m be Element of NAT st f|^m in Ideal_X;
consider m be Element of NAT such that
A6: f|^m in Ideal_X by A5;
m <> 0
proof
assume
A7: m = 0;
f|^m = (power Polynom-Ring(n,R)).(f,m) by BINOM:def 2
.= 1_Polynom-Ring(n,R) by A7,GROUP_1:def 7
.= 1.Polynom-Ring(n,R);
hence contradiction by A4,A6;
end; then
reconsider m as non zero Nat;
f in [#]Polynom-Ring(n,R) by SUBSET_1:def 1; then
reconsider p = f as Polynomial of n,R by POLYNOM1:def 11;
consider fm be Polynomial of n,R such that
A9: fm = f|^m & X c= Zero_(fm) by A6;
f|^m = p`^m by BINOM:def 2; then
Zero_(fm) = Zero_({p`^m}) by A9,Th15 .= Zero_({p}) by Lm8
.= Zero_(p) by Th15;
hence o in Ideal_X by A5,A9;
end;
hence thesis;
end;
hence thesis by TOPZARI1:20;
end;
suppose X = {}; then
Ideal_X = [#]Polynom-Ring(n,R) by Th30;
hence thesis by IDEAL_2:10;
end;
end;
::$INSERT Reducible Algebraic Set.
definition
let R,n;
let IT be Algebraic_Set of n,R;
attr IT is reducible means
ex V1,V2 be Algebraic_Set of n,R st IT = V1 \/ V2 & V1 c< IT & V2 c< IT;
end;
notation
let R,n;
let V be Algebraic_Set of n,R;
antonym V is irreducible for V is reducible;
end;
::NdR Fulton69:p.15 Prop1. An algebraic set V is irreducible iff I(V) is prime.
theorem
for V be non empty Algebraic_Set of n,R holds
V is irreducible iff Ideal_V is prime Ideal of Polynom-Ring(n,R)
proof
let V be non empty Algebraic_Set of n,R;
A1: Ideal_V is prime Ideal of Polynom-Ring(n,R) implies V is irreducible
proof
assume
A2: Ideal_V is prime Ideal of Polynom-Ring(n,R);
assume not V is irreducible; then
consider V1,V2 be Algebraic_Set of n,R such that
A4: V = V1 \/ V2 & V1 c< V & V2 c< V;
consider o1 such that
A5: o1 in Ideal_V1 & not o1 in Ideal_V by A4,Th38, XBOOLE_0:6;
consider o2 such that
A6: o2 in Ideal_V2 & not o2 in Ideal_V by A4,Th38,XBOOLE_0:6;
reconsider f1 = o1, f2 = o2 as Element of Polynom-Ring(n,R) by A6, A5;
reconsider p1 = o1, p2 = o2 as Polynomial of n,R by A6, A5,POLYNOM1:def 11;
A7: Zero_(p1*'p2) = Zero_({p1*'p2}) by Th15
.= Zero_({p1}) \/ Zero_({p2}) by Th21;
Zero_(Ideal_V1) c= Zero_{p1} & Zero_Ideal_V2 c= Zero_{p2}
by A5, A6, ZFMISC_1:31, Th16; then
A8: V1 c= Zero_{p1} & V2 c= Zero_{p2} by Th36;
V c= Zero_(p1*'p2) by A7, A8, A4, XBOOLE_1:13; then
p1*'p2 in Ideal_V; then
A9: f1*f2 in Ideal_V by POLYNOM1:def 11;
Ideal_V is quasi-prime by A2;
hence contradiction by A9, A5, A6;
end;
V is irreducible implies Ideal_V is prime Ideal of Polynom-Ring(n,R)
proof
assume
A10: V is irreducible;
A11: Ideal_V <> [#]Polynom-Ring(n,R) by Th30;
assume not Ideal_V is prime Ideal of Polynom-Ring(n,R); then
not(Ideal_V is proper & Ideal_V is quasi-prime); then
consider f1,f2 be Element of Polynom-Ring(n,R) such that
A14: f1*f2 in Ideal_V & not f1 in Ideal_V & not f2 in Ideal_V by A11;
f1 in Polynom-Ring(n,R) & f2 in Polynom-Ring(n,R) by SUBSET_1:def 1;
then
reconsider p1 = f1, p2 = f2 as Polynomial of n,R by POLYNOM1:def 11;
consider g be Polynomial of n,R such that
A15: f1*f2 = g & V c= Zero_ g by A14;
A16: g = p1*'p2 by A15,POLYNOM1:def 11;
A17: (Zero_{p1} \/ Zero_{p2}) = Zero_{p1*'p2} by Th21 .= Zero_(p1*'p2)
by Th15;
A18: V c/= Zero_{p1}
proof
assume V c= Zero_{p1}; then
A20: Ideal_Zero_{p1} c= Ideal_V by Th29;
{p1} c= Ideal_Zero_{p1} by Th32;
hence contradiction by A14,ZFMISC_1:31,A20;
end;
A21: V c/= Zero_{p2}
proof
assume V c= Zero_{p2}; then
A23: Ideal_Zero_{p2} c= Ideal_V by Th29;
{p2} c= Ideal_Zero_{p2} by Th32;
hence contradiction by A14,ZFMISC_1:31,A23;
end;
A24: V /\ Zero_{p1} c= V & V /\ Zero_{p2} c= V by XBOOLE_1:17;
A27: (V /\ Zero_{p1}) c< V & V /\ Zero_{p2} c< V
by A18,A21,XBOOLE_1:18;
V c= (V /\ Zero_{p1}) \/ (V /\ Zero_{p2})
proof
let x be object;
assume
A28: x in V;
assume not x in (V /\ Zero_{p1}) \/ (V /\ Zero_{p2}); then
not x in (V /\ Zero_{p1}) & not x in (V /\ Zero_{p2})
by XBOOLE_0:def 3; then
not x in Zero_{p1} & not x in Zero_{p2} by A28,XBOOLE_0:def 4;
hence contradiction by A28,A15, A16, A17,XBOOLE_0:def 3;
end; then
A30: V = (V /\ Zero_{f1}) \/ (V /\ Zero_{f2}) by A24,XBOOLE_1:8;
Zero_{f1} <> {} by A21,A15,A16,A17,BOOLE:1; then
reconsider Z = Zero_{f1} as non empty Subset of Funcs(n,[#]R);
Z = Zero_({f1}-Ideal) by Th17; then
A32: Z is algebraic_set_from_ideal;
Zero_{f2} <> {} by A15,A16,A17,BOOLE:1,A18; then
reconsider Z = Zero_{f2} as non empty Subset of Funcs(n,[#]R);
Z = Zero_({f2}-Ideal) by Th17; then
Z is algebraic_set_from_ideal; then
V /\ Zero_{f1} is Algebraic_Set of n,R &
V /\ Zero_{f2} is Algebraic_Set of n,R by A32,Th19;
hence contradiction by A10,A30,A27;
end;
hence thesis by A1;
end;