let A be non degenerated commutative Ring; for p being prime Ideal of A
for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)
let p be prime Ideal of A; for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)
let F be non empty FinSequence of PRIMARY (A,p); meet (rng F) in PRIMARY (A,p)
set q = meet (rng F);
meet (rng F) in PRIMARY (A,p)
proof
A1:
len F <> 0
;
defpred S1[
Nat]
means for
F being non
empty FinSequence of
PRIMARY (
A,
p) st $1
= len F holds
meet (rng F) in PRIMARY (
A,
p);
A2:
for
n being
Nat st
n >= 1 &
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that A3:
n >= 1
and A4:
S1[
n]
;
S1[n + 1]
for
F being non
empty FinSequence of
PRIMARY (
A,
p) st
n + 1
= len F holds
meet (rng F) in PRIMARY (
A,
p)
proof
let F be non
empty FinSequence of
PRIMARY (
A,
p);
( n + 1 = len F implies meet (rng F) in PRIMARY (A,p) )
assume A5:
n + 1
= len F
;
meet (rng F) in PRIMARY (A,p)
len F <> 0
;
then consider G being
FinSequence of
PRIMARY (
A,
p),
q being
Element of
PRIMARY (
A,
p)
such that A6:
F = G ^ <*q*>
by FINSEQ_2:19;
A7:
Seg (len <*q*>) =
dom <*q*>
by FINSEQ_1:def 3
.=
Seg 1
by FINSEQ_1:def 8
;
A8:
len F =
(len G) + (len <*q*>)
by A6, FINSEQ_1:22
.=
(len G) + 1
by A7, FINSEQ_1:6
;
reconsider G =
G as non
empty FinSequence of
PRIMARY (
A,
p)
by A3, A5, A8;
A9:
meet (rng G) in PRIMARY (
A,
p)
by A4, A5, A8;
dom G = Seg n
by A5, A8, FINSEQ_1:def 3;
then A10:
1
in dom G
by A3;
dom <*q*> = Seg 1
by FINSEQ_1:def 8;
then A12:
(
rng G <> {} &
rng <*q*> <> {} )
by A10, RELAT_1:42;
q in { I where I is primary Ideal of A : I is p -primary }
;
then consider q1 being
primary Ideal of
A such that A13:
(
q1 = q &
q1 is
p -primary )
;
consider q2 being
primary Ideal of
A such that A14:
(
q2 = meet (rng G) &
q2 is
p -primary )
by A9;
q2 /\ q1 in { I where I is primary Ideal of A : I is p -primary }
by A13, A9, A14, Th41;
then consider q3 being
primary Ideal of
A such that A15:
q3 = q2 /\ q1
and A16:
q3 is
p -primary
;
A17:
meet (rng F) =
meet ((rng G) \/ (rng <*q*>))
by A6, FINSEQ_1:31
.=
(meet (rng G)) /\ (meet (rng <*q*>))
by A12, SETFAM_1:9
.=
(meet (rng G)) /\ (meet {q})
by FINSEQ_1:38
.=
q3
by A15, A14, A13, SETFAM_1:10
;
reconsider Q =
meet (rng F) as
primary Ideal of
A by A17;
thus
meet (rng F) in PRIMARY (
A,
p)
by A17, A16;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A18:
S1[1]
for
n being
Nat st
n >= 1 holds
S1[
n]
from NAT_1:sch 8(A18, A2);
hence
meet (rng F) in PRIMARY (
A,
p)
by A1, NAT_1:14;
verum
end;
hence
meet (rng F) in PRIMARY (A,p)
; verum