:: Prime Ideals and Filters
:: by Grzegorz Bancerek
::
:: Received December 1, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: WAYBEL_7:1
canceled;
theorem :: WAYBEL_7:2
canceled;
theorem Th3: :: WAYBEL_7:3
theorem Th4: :: WAYBEL_7:4
theorem Th5: :: WAYBEL_7:5
theorem :: WAYBEL_7:6
canceled;
theorem :: WAYBEL_7:7
canceled;
theorem Th8: :: WAYBEL_7:8
theorem Th9: :: WAYBEL_7:9
theorem :: WAYBEL_7:10
theorem Th11: :: WAYBEL_7:11
theorem :: WAYBEL_7:12
theorem Th13: :: WAYBEL_7:13
theorem :: WAYBEL_7:14
theorem Th15: :: WAYBEL_7:15
:: deftheorem Def1 defines prime WAYBEL_7:def 1 :
theorem Th16: :: WAYBEL_7:16
theorem :: WAYBEL_7:17
:: deftheorem Def2 defines prime WAYBEL_7:def 2 :
theorem :: WAYBEL_7:18
theorem Th19: :: WAYBEL_7:19
theorem Th20: :: WAYBEL_7:20
theorem Th21: :: WAYBEL_7:21
theorem :: WAYBEL_7:22
theorem :: WAYBEL_7:23
theorem Th24: :: WAYBEL_7:24
theorem Th25: :: WAYBEL_7:25
:: deftheorem Def3 defines ultra WAYBEL_7:def 3 :
Lm1:
for L being with_infima Poset
for F being Filter of L
for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (F \/ X)) holds
ex a being Element of L st
( a in F & x >= a "/\" (inf X) )
theorem Th26: :: WAYBEL_7:26
Lm2:
for L being with_suprema Poset
for I being Ideal of L
for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
theorem Th27: :: WAYBEL_7:27
theorem Th28: :: WAYBEL_7:28
theorem Th29: :: WAYBEL_7:29
theorem Th30: :: WAYBEL_7:30
:: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def 4 :
:: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def 5 :
theorem Th31: :: WAYBEL_7:31
theorem Th32: :: WAYBEL_7:32
theorem :: WAYBEL_7:33
theorem Th34: :: WAYBEL_7:34
theorem :: WAYBEL_7:35
theorem :: WAYBEL_7:36
theorem Th37: :: WAYBEL_7:37
:: deftheorem Def6 defines pseudoprime WAYBEL_7:def 6 :
theorem Th38: :: WAYBEL_7:38
theorem Th39: :: WAYBEL_7:39
theorem :: WAYBEL_7:40
theorem :: WAYBEL_7:41
theorem :: WAYBEL_7:42
theorem :: WAYBEL_7:43
:: deftheorem Def7 defines multiplicative WAYBEL_7:def 7 :
theorem :: WAYBEL_7:44
theorem Th45: :: WAYBEL_7:45
theorem :: WAYBEL_7:46
theorem :: WAYBEL_7:47
Lm3:
now
let L be
lower-bounded continuous LATTICE;
:: thesis: for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) holds
p is prime let p be
Element of
L;
:: thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime )assume that A1:
L -waybelow is
multiplicative
and A2:
for
a,
b being
Element of
L holds
( not
a "/\" b << p or
a <= p or
b <= p )
and A3:
not
p is
prime
;
:: thesis: contradictionconsider x,
y being
Element of
L such that A4:
x "/\" y <= p
and A5:
not
x <= p
and A6:
not
y <= p
by A3, WAYBEL_6:def 6;
A7:
for
a being
Element of
L holds
( not
waybelow a is
empty &
waybelow a is
directed )
;
then consider u being
Element of
L such that A8:
u << x
and A9:
not
u <= p
by A5, WAYBEL_3:24;
consider v being
Element of
L such that A10:
v << y
and A11:
not
v <= p
by A6, A7, WAYBEL_3:24;
A12:
[v,y] in L -waybelow
by A10, WAYBEL_4:def 2;
[u,x] in L -waybelow
by A8, WAYBEL_4:def 2;
then
[(u "/\" v),(x "/\" y)] in L -waybelow
by A1, A12, Th45;
then
u "/\" v << x "/\" y
by WAYBEL_4:def 2;
then
u "/\" v << p
by A4, WAYBEL_3:2;
hence
contradiction
by A2, A9, A11;
:: thesis: verum
end;
theorem Th48: :: WAYBEL_7:48
theorem :: WAYBEL_7:49
theorem :: WAYBEL_7:50