Metamath Proof Explorer

Theorem 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 syl5bir 
 |-  ( ( ( 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 )