let A be non degenerated commutative Ring; for I being proper Ideal of A
for F being non empty FinSequence of Ideals A holds (% I) . (meet (rng F)) = meet (rng ((% I) * F))
let I be proper Ideal of A; for F being non empty FinSequence of Ideals A holds (% I) . (meet (rng F)) = meet (rng ((% I) * F))
let F be non empty FinSequence of Ideals A; (% I) . (meet (rng F)) = meet (rng ((% I) * F))
reconsider J = meet (rng F) as Ideal of A by Th3;
A1:
rng F c= bool the carrier of A
by XBOOLE_1:1;
then reconsider F1 = F as non empty FinSequence of bool the carrier of A by FINSEQ_1:def 4;
A2:
dom (% I) = bool the carrier of A
by FUNCT_2:def 1;
A3:
dom ((% I) * F) = dom F
by A1, A2, RELAT_1:27;
A4:
rng ((% I) * F) <> {}
by Th6;
A5:
rng F c= Ideals A
;
A6:
for x being object st x in (% I) . (meet (rng F)) holds
x in meet (rng ((% I) * F))
proof
let x be
object ;
( x in (% I) . (meet (rng F)) implies x in meet (rng ((% I) * F)) )
assume
x in (% I) . (meet (rng F))
;
x in meet (rng ((% I) * F))
then A8:
x in J % I
by Def1;
x in { a where a is Element of A : a * I c= J }
by A8, IDEAL_1:def 23;
then consider a being
Element of
A such that A9:
(
a = x &
a * I c= J )
;
x in meet (rng ((% I) * F))
proof
assume
not
x in meet (rng ((% I) * F))
;
contradiction
then consider Y being
set such that A11:
(
Y in rng ((% I) * F) & not
x in Y )
by A4, SETFAM_1:def 1;
consider i being
object such that A12:
(
i in dom ((% I) * F) &
Y = ((% I) * F) . i )
by A11, FUNCT_1:def 3;
A13:
Y = (% I) . (F1 . i)
by A12, FINSEQ_3:120;
reconsider i1 =
i as
Nat by A12;
i in dom F
by A1, A2, RELAT_1:27, A12;
then A14:
F . i in rng F
by FUNCT_1:def 3;
F . i in Ideals A
by A14;
then
F . i in { I where I is Ideal of A : verum }
by RING_2:def 3;
then consider Fi being
Ideal of
A such that A15:
Fi = F . i
;
A16:
Y = Fi % I
by Def1, A13, A15;
meet (rng F) c= F . i
by A14, SETFAM_1:3;
then
a * I c= Fi
by A9, A15;
then
a in { b where b is Element of A : b * I c= Fi }
;
hence
contradiction
by A11, A9, A16, IDEAL_1:def 23;
verum
end;
hence
x in meet (rng ((% I) * F))
;
verum
end;
meet (rng ((% I) * F)) c= (% I) . (meet (rng F))
proof
let x be
object ;
TARSKI:def 3 ( not x in meet (rng ((% I) * F)) or x in (% I) . (meet (rng F)) )
assume A18:
x in meet (rng ((% I) * F))
;
x in (% I) . (meet (rng F))
then consider a being
Element of
A such that A19:
x = a
;
A20:
(
dom ((% I) * F1) = dom F1 &
len ((% I) * F1) = len F1 & ( for
i being
Nat st
i in dom ((% I) * F1) holds
((% I) * F1) . i = (% I) . (F1 . i) ) )
by FINSEQ_3:120;
A21:
F is
Function of
(dom F),
(rng F)
by FUNCT_2:1;
for
Y being
set st
Y in rng F holds
a * I c= Y
proof
let Y be
set ;
( Y in rng F implies a * I c= Y )
assume
Y in rng F
;
a * I c= Y
then consider j being
object such that A23:
(
j in dom F &
Y = F . j )
by A21, FUNCT_2:11;
F . j in Ideals A
by A23, A5, FUNCT_1:3;
then
F . j in { I where I is Ideal of A : verum }
by RING_2:def 3;
then consider Fj being
Ideal of
A such that A24:
Fj = F . j
;
A25:
((% I) * F1) . j in rng ((% I) * F)
by A23, A3, FUNCT_1:def 3;
x in ((% I) * F) . j
by A25, A18, SETFAM_1:def 1;
then
x in (% I) . Fj
by A20, A23, A24;
then A26:
x in Fj % I
by Def1;
a in { b where b is Element of A : b * I c= Fj }
by A19, A26, IDEAL_1:def 23;
then consider b1 being
Element of
A such that A27:
(
a = b1 &
b1 * I c= Fj )
;
thus
a * I c= Y
by A23, A24, A27;
verum
end;
then A28:
a * I c= meet (rng F)
by Th6, SETFAM_1:5;
x in (% I) . (meet (rng F))
hence
x in (% I) . (meet (rng F))
;
verum
end;
hence
(% I) . (meet (rng F)) = meet (rng ((% I) * F))
by A6, TARSKI:2; verum