let R be domRing; for n being non empty Ordinal
for m being non zero Nat
for F being Subset of (Alg_Sets (n,R)) st card F = m holds
union F is Algebraic_Set of n,R
let n be non empty Ordinal; for m being non zero Nat
for F being Subset of (Alg_Sets (n,R)) st card F = m holds
union F is Algebraic_Set of n,R
let m be non zero Nat; for F being Subset of (Alg_Sets (n,R)) st card F = m holds
union F is Algebraic_Set of n,R
let F be Subset of (Alg_Sets (n,R)); ( card F = m implies union F is Algebraic_Set of n,R )
defpred S1[ Nat] means for G being Subset of (Alg_Sets (n,R)) st card G = $1 holds
union G is Algebraic_Set of n,R;
A1:
for m being non zero Nat st S1[m] holds
S1[m + 1]
proof
let m be non
zero Nat;
( S1[m] implies S1[m + 1] )
assume A2:
S1[
m]
;
S1[m + 1]
for
G being
Subset of
(Alg_Sets (n,R)) st
card G = m + 1 holds
union G is
Algebraic_Set of
n,
R
proof
let G be
Subset of
(Alg_Sets (n,R));
( card G = m + 1 implies union G is Algebraic_Set of n,R )
assume A3:
card G = m + 1
;
union G is Algebraic_Set of n,R
then
G <> {}
;
then consider o being
object 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 being
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 being
Ideal of
(Polynom-Ring (n,R)) such that A9:
union G1 = Zero_ I
by Def7;
consider J being
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 being
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
union G is
Algebraic_Set of
n,
R
by Def7;
verum
end;
hence
S1[
m + 1]
;
verum
end;
A14:
S1[1]
proof
for
G being
Subset of
(Alg_Sets (n,R)) st
card G = 1 holds
union G is
Algebraic_Set of
n,
R
proof
let G be
Subset of
(Alg_Sets (n,R));
( card G = 1 implies union G is Algebraic_Set of n,R )
assume
card G = 1
;
union G is Algebraic_Set of n,R
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 being
Subset of
(Funcs (n,([#] R))) such that A20:
(
o = S &
S is
Algebraic_Set of
n,
R )
;
thus
union G is
Algebraic_Set of
n,
R
by A16, A20, ZFMISC_1:25;
verum
end;
hence
S1[1]
;
verum
end;
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A14, A1);
hence
( card F = m implies union F is Algebraic_Set of n,R )
; verum