atlatmstc

Description: An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in Kalmbach p. 140; also remark in BeltramettiCassinelli p. 98. ( hatomistici analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atlatmstc.b	\|- B = ( Base ` K )
	atlatmstc.l	\|- .<_ = ( le ` K )
	atlatmstc.u	\|- .1. = ( lub ` K )
	atlatmstc.a	\|- A = ( Atoms ` K )
Assertion	atlatmstc	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A \| y .<_ X } ) = X )

Proof

Step	Hyp	Ref	Expression
1		atlatmstc.b	\|- B = ( Base ` K )
2		atlatmstc.l	\|- .<_ = ( le ` K )
3		atlatmstc.u	\|- .1. = ( lub ` K )
4		atlatmstc.a	\|- A = ( Atoms ` K )
5		simpl2	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> K e. CLat )
6		ssrab2	\|- { y e. B \| y .<_ X } C_ B
7	1 4	atssbase	\|- A C_ B
8		rabss2	\|- ( A C_ B -> { y e. A \| y .<_ X } C_ { y e. B \| y .<_ X } )
9	7 8	ax-mp	\|- { y e. A \| y .<_ X } C_ { y e. B \| y .<_ X }
10	1 2 3	lubss	\|- ( ( K e. CLat /\ { y e. B \| y .<_ X } C_ B /\ { y e. A \| y .<_ X } C_ { y e. B \| y .<_ X } ) -> ( .1. ` { y e. A \| y .<_ X } ) .<_ ( .1. ` { y e. B \| y .<_ X } ) )
11	6 9 10	mp3an23	\|- ( K e. CLat -> ( .1. ` { y e. A \| y .<_ X } ) .<_ ( .1. ` { y e. B \| y .<_ X } ) )
12	5 11	syl	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A \| y .<_ X } ) .<_ ( .1. ` { y e. B \| y .<_ X } ) )
13		atlpos	\|- ( K e. AtLat -> K e. Poset )
14	13	3ad2ant3	\|- ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) -> K e. Poset )
15		simpl	\|- ( ( K e. Poset /\ X e. B ) -> K e. Poset )
16		simpr	\|- ( ( K e. Poset /\ X e. B ) -> X e. B )
17	1 2 3 15 16	lubid	\|- ( ( K e. Poset /\ X e. B ) -> ( .1. ` { y e. B \| y .<_ X } ) = X )
18	14 17	sylan	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. B \| y .<_ X } ) = X )
19	12 18	breqtrd	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A \| y .<_ X } ) .<_ X )
20		breq1	\|- ( y = x -> ( y .<_ X <-> x .<_ X ) )
21	20	elrab	\|- ( x e. { y e. A \| y .<_ X } <-> ( x e. A /\ x .<_ X ) )
22		simpll2	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. { y e. A \| y .<_ X } ) -> K e. CLat )
23		ssrab2	\|- { y e. A \| y .<_ X } C_ A
24	23 7	sstri	\|- { y e. A \| y .<_ X } C_ B
25	1 2 3	lubel	\|- ( ( K e. CLat /\ x e. { y e. A \| y .<_ X } /\ { y e. A \| y .<_ X } C_ B ) -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) )
26	24 25	mp3an3	\|- ( ( K e. CLat /\ x e. { y e. A \| y .<_ X } ) -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) )
27	22 26	sylancom	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. { y e. A \| y .<_ X } ) -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) )
28	27	ex	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( x e. { y e. A \| y .<_ X } -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) )
29	21 28	biimtrrid	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( x e. A /\ x .<_ X ) -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) )
30	29	expdimp	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( x .<_ X -> x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) )
31		simpll3	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> K e. AtLat )
32		eqid	\|- ( 0. ` K ) = ( 0. ` K )
33	32 4	atn0	\|- ( ( K e. AtLat /\ x e. A ) -> x =/= ( 0. ` K ) )
34	31 33	sylancom	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> x =/= ( 0. ` K ) )
35	34	adantr	\|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) /\ x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) -> x =/= ( 0. ` K ) )
36		simpl3	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> K e. AtLat )
37		atllat	\|- ( K e. AtLat -> K e. Lat )
38	36 37	syl	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> K e. Lat )
39	38	adantr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> K e. Lat )
40	1 4	atbase	\|- ( x e. A -> x e. B )
41	40	adantl	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> x e. B )
42	1 3	clatlubcl	\|- ( ( K e. CLat /\ { y e. A \| y .<_ X } C_ B ) -> ( .1. ` { y e. A \| y .<_ X } ) e. B )
43	5 24 42	sylancl	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A \| y .<_ X } ) e. B )
44	43	adantr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( .1. ` { y e. A \| y .<_ X } ) e. B )
45		simpl1	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> K e. OML )
46		omlop	\|- ( K e. OML -> K e. OP )
47	45 46	syl	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> K e. OP )
48		eqid	\|- ( oc ` K ) = ( oc ` K )
49	1 48	opoccl	\|- ( ( K e. OP /\ ( .1. ` { y e. A \| y .<_ X } ) e. B ) -> ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B )
50	47 43 49	syl2anc	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B )
51	50	adantr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B )
52		eqid	\|- ( meet ` K ) = ( meet ` K )
53	1 2 52	latlem12	\|- ( ( K e. Lat /\ ( x e. B /\ ( .1. ` { y e. A \| y .<_ X } ) e. B /\ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B ) ) -> ( ( x .<_ ( .1. ` { y e. A \| y .<_ X } ) /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) )
54	39 41 44 51 53	syl13anc	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( ( x .<_ ( .1. ` { y e. A \| y .<_ X } ) /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) )
55	1 48 52 32	opnoncon	\|- ( ( K e. OP /\ ( .1. ` { y e. A \| y .<_ X } ) e. B ) -> ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) )
56	47 43 55	syl2anc	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) )
57	56	breq2d	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( x .<_ ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( 0. ` K ) ) )
58	57	adantr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( x .<_ ( ( .1. ` { y e. A \| y .<_ X } ) ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( 0. ` K ) ) )
59	1 2 32	ople0	\|- ( ( K e. OP /\ x e. B ) -> ( x .<_ ( 0. ` K ) <-> x = ( 0. ` K ) ) )
60	47 40 59	syl2an	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( x .<_ ( 0. ` K ) <-> x = ( 0. ` K ) ) )
61	54 58 60	3bitrd	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( ( x .<_ ( .1. ` { y e. A \| y .<_ X } ) /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x = ( 0. ` K ) ) )
62	61	biimpa	\|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) /\ ( x .<_ ( .1. ` { y e. A \| y .<_ X } ) /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) -> x = ( 0. ` K ) )
63	62	expr	\|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) /\ x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) -> ( x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) -> x = ( 0. ` K ) ) )
64	63	necon3ad	\|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) /\ x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) -> ( x =/= ( 0. ` K ) -> -. x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
65	35 64	mpd	\|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) /\ x .<_ ( .1. ` { y e. A \| y .<_ X } ) ) -> -. x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) )
66	65	ex	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( x .<_ ( .1. ` { y e. A \| y .<_ X } ) -> -. x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
67	30 66	syld	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( x .<_ X -> -. x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
68		imnan	\|- ( ( x .<_ X -> -. x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> -. ( x .<_ X /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
69	67 68	sylib	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> -. ( x .<_ X /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
70		simplr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> X e. B )
71	1 2 52	latlem12	\|- ( ( K e. Lat /\ ( x e. B /\ X e. B /\ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B ) ) -> ( ( x .<_ X /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) )
72	39 41 70 51 71	syl13anc	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> ( ( x .<_ X /\ x .<_ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) <-> x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) )
73	69 72	mtbid	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ x e. A ) -> -. x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
74	73	nrexdv	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> -. E. x e. A x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
75		simpll3	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) ) -> K e. AtLat )
76		simpr	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> X e. B )
77	1 52	latmcl	\|- ( ( K e. Lat /\ X e. B /\ ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) e. B ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) e. B )
78	38 76 50 77	syl3anc	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) e. B )
79	78	adantr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) e. B )
80		simpr	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) )
81	1 2 32 4	atlex	\|- ( ( K e. AtLat /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) e. B /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) ) -> E. x e. A x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
82	75 79 80 81	syl3anc	\|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) ) -> E. x e. A x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) )
83	82	ex	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) =/= ( 0. ` K ) -> E. x e. A x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) ) )
84	83	necon1bd	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( -. E. x e. A x .<_ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) ) )
85	74 84	mpd	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) )
86	1 2 52 48 32	omllaw3	\|- ( ( K e. OML /\ ( .1. ` { y e. A \| y .<_ X } ) e. B /\ X e. B ) -> ( ( ( .1. ` { y e. A \| y .<_ X } ) .<_ X /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) ) -> ( .1. ` { y e. A \| y .<_ X } ) = X ) )
87	45 43 76 86	syl3anc	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( ( ( .1. ` { y e. A \| y .<_ X } ) .<_ X /\ ( X ( meet ` K ) ( ( oc ` K ) ` ( .1. ` { y e. A \| y .<_ X } ) ) ) = ( 0. ` K ) ) -> ( .1. ` { y e. A \| y .<_ X } ) = X ) )
88	19 85 87	mp2and	\|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A \| y .<_ X } ) = X )

Metamath Proof Explorer

Theorem atlatmstc

Proof