Metamath Proof Explorer

Theorem lhprelat3N

Description: The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 . (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhprelat3.b 
|- B = ( Base ` K )
lhprelat3.l 
|- .<_ = ( le ` K )
lhprelat3.s 
|- .< = ( lt ` K )
lhprelat3.m 
|- ./\ = ( meet ` K )
lhprelat3.c 
|- C = (
lhprelat3.h 
|- H = ( LHyp ` K )
Assertion lhprelat3N 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. w e. H ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) )

Proof

Step Hyp Ref Expression
1 lhprelat3.b 
 |-  B = ( Base ` K )
2 lhprelat3.l 
 |-  .<_ = ( le ` K )
3 lhprelat3.s 
 |-  .< = ( lt ` K )
4 lhprelat3.m 
 |-  ./\ = ( meet ` K )
5 lhprelat3.c 
 |-  C = (
6 lhprelat3.h 
 |-  H = ( LHyp ` K )
7 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> p e. ( Atoms ` K ) )
8 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> K e. HL )
9 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 1 9 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
11 10 adantl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> p e. B )
12 eqid 
 |-  ( oc ` K ) = ( oc ` K )
13 1 12 9 6 lhpoc2N 
 |-  ( ( K e. HL /\ p e. B ) -> ( p e. ( Atoms ` K ) <-> ( ( oc ` K ) ` p ) e. H ) )
14 8 11 13 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( p e. ( Atoms ` K ) <-> ( ( oc ` K ) ` p ) e. H ) )
15 7 14 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( oc ` K ) ` p ) e. H )
16 15 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) /\ ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) ) -> ( ( oc ` K ) ` p ) e. H )
17 hlop 
 |-  ( K e. HL -> K e. OP )
18 8 17 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> K e. OP )
19 8 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> K e. Lat )
20 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> Y e. B )
21 1 12 opoccl 
 |-  ( ( K e. OP /\ p e. B ) -> ( ( oc ` K ) ` p ) e. B )
22 18 11 21 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( oc ` K ) ` p ) e. B )
23 1 4 latmcl 
 |-  ( ( K e. Lat /\ Y e. B /\ ( ( oc ` K ) ` p ) e. B ) -> ( Y ./\ ( ( oc ` K ) ` p ) ) e. B )
24 19 20 22 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( Y ./\ ( ( oc ` K ) ` p ) ) e. B )
25 1 12 5 cvrcon3b 
 |-  ( ( K e. OP /\ ( Y ./\ ( ( oc ` K ) ` p ) ) e. B /\ Y e. B ) -> ( ( Y ./\ ( ( oc ` K ) ` p ) ) C Y <-> ( ( oc ` K ) ` Y ) C ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) ) )
26 18 24 20 25 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( Y ./\ ( ( oc ` K ) ` p ) ) C Y <-> ( ( oc ` K ) ` Y ) C ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) ) )
27 hlol 
 |-  ( K e. HL -> K e. OL )
28 8 27 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> K e. OL )
29 eqid 
 |-  ( join ` K ) = ( join ` K )
30 1 29 4 12 oldmm3N 
 |-  ( ( K e. OL /\ Y e. B /\ p e. B ) -> ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) = ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) )
31 28 20 11 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) = ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) )
32 31 breq2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( ( oc ` K ) ` Y ) C ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) <-> ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) ) )
33 26 32 bitr2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) <-> ( Y ./\ ( ( oc ` K ) ` p ) ) C Y ) )
34 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> X e. B )
35 1 2 12 oplecon3b 
 |-  ( ( K e. OP /\ X e. B /\ ( Y ./\ ( ( oc ` K ) ` p ) ) e. B ) -> ( X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) <-> ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) .<_ ( ( oc ` K ) ` X ) ) )
36 18 34 24 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) <-> ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) .<_ ( ( oc ` K ) ` X ) ) )
37 31 breq1d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( ( oc ` K ) ` ( Y ./\ ( ( oc ` K ) ` p ) ) ) .<_ ( ( oc ` K ) ` X ) <-> ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) )
38 36 37 bitr2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) <-> X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) ) )
39 33 38 anbi12d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) -> ( ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) <-> ( ( Y ./\ ( ( oc ` K ) ` p ) ) C Y /\ X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) ) ) )
40 39 biimpa 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) /\ ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) ) -> ( ( Y ./\ ( ( oc ` K ) ` p ) ) C Y /\ X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) ) )
41 40 ancomd 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) /\ ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) ) -> ( X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) /\ ( Y ./\ ( ( oc ` K ) ` p ) ) C Y ) )
42 oveq2 
 |-  ( w = ( ( oc ` K ) ` p ) -> ( Y ./\ w ) = ( Y ./\ ( ( oc ` K ) ` p ) ) )
43 42 breq2d 
 |-  ( w = ( ( oc ` K ) ` p ) -> ( X .<_ ( Y ./\ w ) <-> X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) ) )
44 42 breq1d 
 |-  ( w = ( ( oc ` K ) ` p ) -> ( ( Y ./\ w ) C Y <-> ( Y ./\ ( ( oc ` K ) ` p ) ) C Y ) )
45 43 44 anbi12d 
 |-  ( w = ( ( oc ` K ) ` p ) -> ( ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) <-> ( X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) /\ ( Y ./\ ( ( oc ` K ) ` p ) ) C Y ) ) )
46 45 rspcev 
 |-  ( ( ( ( oc ` K ) ` p ) e. H /\ ( X .<_ ( Y ./\ ( ( oc ` K ) ` p ) ) /\ ( Y ./\ ( ( oc ` K ) ` p ) ) C Y ) ) -> E. w e. H ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) )
47 16 41 46 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. ( Atoms ` K ) ) /\ ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) ) -> E. w e. H ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) )
48 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> K e. HL )
49 48 17 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> K e. OP )
50 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> Y e. B )
51 1 12 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
52 49 50 51 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( ( oc ` K ) ` Y ) e. B )
53 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X e. B )
54 1 12 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
55 49 53 54 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( ( oc ` K ) ` X ) e. B )
56 simpr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> X .< Y )
57 1 3 12 opltcon3b 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( ( oc ` K ) ` Y ) .< ( ( oc ` K ) ` X ) ) )
58 49 53 50 57 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( X .< Y <-> ( ( oc ` K ) ` Y ) .< ( ( oc ` K ) ` X ) ) )
59 56 58 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( ( oc ` K ) ` Y ) .< ( ( oc ` K ) ` X ) )
60 1 2 3 29 5 9 hlrelat3 
 |-  ( ( ( K e. HL /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` X ) e. B ) /\ ( ( oc ` K ) ` Y ) .< ( ( oc ` K ) ` X ) ) -> E. p e. ( Atoms ` K ) ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) )
61 48 52 55 59 60 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. p e. ( Atoms ` K ) ( ( ( oc ` K ) ` Y ) C ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) p ) .<_ ( ( oc ` K ) ` X ) ) )
62 47 61 r19.29a 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. w e. H ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) )