Metamath Proof Explorer

Theorem lplncvrlvol

Description: An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypotheses lplncvrlvol.b 
|- B = ( Base ` K )
lplncvrlvol.c 
|- C = (
lplncvrlvol.p 
|- P = ( LPlanes ` K )
lplncvrlvol.v 
|- V = ( LVols ` K )
Assertion lplncvrlvol 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. P <-> Y e. V ) )

Proof

Step Hyp Ref Expression
1 lplncvrlvol.b 
 |-  B = ( Base ` K )
2 lplncvrlvol.c 
 |-  C = (
3 lplncvrlvol.p 
 |-  P = ( LPlanes ` K )
4 lplncvrlvol.v 
 |-  V = ( LVols ` K )
5 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. P ) -> K e. HL )
6 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. P ) -> Y e. B )
7 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. P ) -> X e. P )
8 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. P ) -> X C Y )
9 1 2 3 4 lvoli 
 |-  ( ( ( K e. HL /\ Y e. B /\ X e. P ) /\ X C Y ) -> Y e. V )
10 5 6 7 8 9 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. P ) -> Y e. V )
11 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> K e. HL )
12 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> X e. B )
13 11 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> K e. Lat )
14 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> Y e. B )
15 eqid 
 |-  ( le ` K ) = ( le ` K )
16 1 15 latref 
 |-  ( ( K e. Lat /\ Y e. B ) -> Y ( le ` K ) Y )
17 13 14 16 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> Y ( le ` K ) Y )
18 11 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ Y e. ( Atoms ` K ) ) -> K e. HL )
19 simplr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ Y e. ( Atoms ` K ) ) -> Y e. V )
20 simpr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ Y e. ( Atoms ` K ) ) -> Y e. ( Atoms ` K ) )
21 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
22 15 21 4 lvolnleat 
 |-  ( ( K e. HL /\ Y e. V /\ Y e. ( Atoms ` K ) ) -> -. Y ( le ` K ) Y )
23 18 19 20 22 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ Y e. ( Atoms ` K ) ) -> -. Y ( le ` K ) Y )
24 23 ex 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( Y e. ( Atoms ` K ) -> -. Y ( le ` K ) Y ) )
25 17 24 mt2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> -. Y e. ( Atoms ` K ) )
26 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> X C Y )
27 breq1 
 |-  ( X = ( 0. ` K ) -> ( X C Y <-> ( 0. ` K ) C Y ) )
28 26 27 syl5ibcom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( X = ( 0. ` K ) -> ( 0. ` K ) C Y ) )
29 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
30 1 29 2 21 isat2 
 |-  ( ( K e. HL /\ Y e. B ) -> ( Y e. ( Atoms ` K ) <-> ( 0. ` K ) C Y ) )
31 11 14 30 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( Y e. ( Atoms ` K ) <-> ( 0. ` K ) C Y ) )
32 28 31 sylibrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( X = ( 0. ` K ) -> Y e. ( Atoms ` K ) ) )
33 32 necon3bd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( -. Y e. ( Atoms ` K ) -> X =/= ( 0. ` K ) ) )
34 25 33 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> X =/= ( 0. ` K ) )
35 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
36 35 4 lvolnelln 
 |-  ( ( K e. HL /\ Y e. V ) -> -. Y e. ( LLines ` K ) )
37 11 36 sylancom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> -. Y e. ( LLines ` K ) )
38 11 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ X e. ( Atoms ` K ) ) -> K e. HL )
39 14 adantr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ X e. ( Atoms ` K ) ) -> Y e. B )
40 simpr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ X e. ( Atoms ` K ) ) -> X e. ( Atoms ` K ) )
41 simpllr 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ X e. ( Atoms ` K ) ) -> X C Y )
42 1 2 21 35 llni 
 |-  ( ( ( K e. HL /\ Y e. B /\ X e. ( Atoms ` K ) ) /\ X C Y ) -> Y e. ( LLines ` K ) )
43 38 39 40 41 42 syl31anc 
 |-  ( ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) /\ X e. ( Atoms ` K ) ) -> Y e. ( LLines ` K ) )
44 37 43 mtand 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> -. X e. ( Atoms ` K ) )
45 3 4 lvolnelpln 
 |-  ( ( K e. HL /\ Y e. V ) -> -. Y e. P )
46 11 45 sylancom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> -. Y e. P )
47 1 2 35 3 llncvrlpln 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. ( LLines ` K ) <-> Y e. P ) )
48 47 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( X e. ( LLines ` K ) <-> Y e. P ) )
49 46 48 mtbird 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> -. X e. ( LLines ` K ) )
50 1 15 29 21 35 3 lplnle 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= ( 0. ` K ) /\ -. X e. ( Atoms ` K ) /\ -. X e. ( LLines ` K ) ) ) -> E. z e. P z ( le ` K ) X )
51 11 12 34 44 49 50 syl23anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> E. z e. P z ( le ` K ) X )
52 simpr3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z ( le ` K ) X )
53 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> K e. HL )
54 hlop 
 |-  ( K e. HL -> K e. OP )
55 53 54 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> K e. OP )
56 simpr2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z e. P )
57 1 3 lplnbase 
 |-  ( z e. P -> z e. B )
58 56 57 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z e. B )
59 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> X e. B )
60 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> Y e. B )
61 simpr1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> Y e. V )
62 1 15 2 cvrle 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( le ` K ) Y )
63 62 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> X ( le ` K ) Y )
64 hlpos 
 |-  ( K e. HL -> K e. Poset )
65 53 64 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> K e. Poset )
66 1 15 postr 
 |-  ( ( K e. Poset /\ ( z e. B /\ X e. B /\ Y e. B ) ) -> ( ( z ( le ` K ) X /\ X ( le ` K ) Y ) -> z ( le ` K ) Y ) )
67 65 58 59 60 66 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> ( ( z ( le ` K ) X /\ X ( le ` K ) Y ) -> z ( le ` K ) Y ) )
68 52 63 67 mp2and 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z ( le ` K ) Y )
69 15 2 3 4 lplncvrlvol2 
 |-  ( ( ( K e. HL /\ z e. P /\ Y e. V ) /\ z ( le ` K ) Y ) -> z C Y )
70 53 56 61 68 69 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z C Y )
71 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> X C Y )
72 1 15 2 cvrcmp2 
 |-  ( ( K e. OP /\ ( z e. B /\ X e. B /\ Y e. B ) /\ ( z C Y /\ X C Y ) ) -> ( z ( le ` K ) X <-> z = X ) )
73 55 58 59 60 70 71 72 syl132anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> ( z ( le ` K ) X <-> z = X ) )
74 52 73 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> z = X )
75 74 56 eqeltrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. V /\ z e. P /\ z ( le ` K ) X ) ) -> X e. P )
76 75 3exp2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( Y e. V -> ( z e. P -> ( z ( le ` K ) X -> X e. P ) ) ) )
77 76 imp 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( z e. P -> ( z ( le ` K ) X -> X e. P ) ) )
78 77 rexlimdv 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> ( E. z e. P z ( le ` K ) X -> X e. P ) )
79 51 78 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. V ) -> X e. P )
80 10 79 impbida 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. P <-> Y e. V ) )