This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem llncvrlpln

Description: An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012)

Ref Expression
Hypotheses llncvrlpln.b 
|- B = ( Base ` K )
llncvrlpln.c 
|- C = (
llncvrlpln.n 
|- N = ( LLines ` K )
llncvrlpln.p 
|- P = ( LPlanes ` K )
Assertion llncvrlpln 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. N <-> Y e. P ) )

Proof

Step Hyp Ref Expression
1 llncvrlpln.b 
 |-  B = ( Base ` K )
2 llncvrlpln.c 
 |-  C = (
3 llncvrlpln.n 
 |-  N = ( LLines ` K )
4 llncvrlpln.p 
 |-  P = ( LPlanes ` K )
5 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. N ) -> K e. HL )
6 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. N ) -> Y e. B )
7 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. N ) -> X e. N )
8 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. N ) -> X C Y )
9 1 2 3 4 lplni 
 |-  ( ( ( K e. HL /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. P )
10 5 6 7 8 9 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ X e. N ) -> Y e. P )
11 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> K e. HL )
12 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> X e. B )
13 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
14 13 4 lplnneat 
 |-  ( ( K e. HL /\ Y e. P ) -> -. Y e. ( Atoms ` K ) )
15 11 14 sylancom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> -. Y e. ( Atoms ` K ) )
16 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> X C Y )
17 breq1 
 |-  ( X = ( 0. ` K ) -> ( X C Y <-> ( 0. ` K ) C Y ) )
18 16 17 syl5ibcom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( X = ( 0. ` K ) -> ( 0. ` K ) C Y ) )
19 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> Y e. B )
20 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
21 1 20 2 13 isat2 
 |-  ( ( K e. HL /\ Y e. B ) -> ( Y e. ( Atoms ` K ) <-> ( 0. ` K ) C Y ) )
22 11 19 21 syl2anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( Y e. ( Atoms ` K ) <-> ( 0. ` K ) C Y ) )
23 18 22 sylibrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( X = ( 0. ` K ) -> Y e. ( Atoms ` K ) ) )
24 23 necon3bd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( -. Y e. ( Atoms ` K ) -> X =/= ( 0. ` K ) ) )
25 15 24 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> X =/= ( 0. ` K ) )
26 3 4 lplnnelln 
 |-  ( ( K e. HL /\ Y e. P ) -> -. Y e. N )
27 11 26 sylancom 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> -. Y e. N )
28 1 2 13 3 atcvrlln 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. ( Atoms ` K ) <-> Y e. N ) )
29 28 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( X e. ( Atoms ` K ) <-> Y e. N ) )
30 27 29 mtbird 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> -. X e. ( Atoms ` K ) )
31 eqid 
 |-  ( le ` K ) = ( le ` K )
32 1 31 20 13 3 llnle 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( X =/= ( 0. ` K ) /\ -. X e. ( Atoms ` K ) ) ) -> E. z e. N z ( le ` K ) X )
33 11 12 25 30 32 syl22anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> E. z e. N z ( le ` K ) X )
34 simpr3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z ( le ` K ) X )
35 simpll1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> K e. HL )
36 hlop 
 |-  ( K e. HL -> K e. OP )
37 35 36 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> K e. OP )
38 simpr2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z e. N )
39 1 3 llnbase 
 |-  ( z e. N -> z e. B )
40 38 39 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z e. B )
41 simpll2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> X e. B )
42 simpll3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> Y e. B )
43 simpr1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> Y e. P )
44 1 31 2 cvrle 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( le ` K ) Y )
45 44 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> X ( le ` K ) Y )
46 hlpos 
 |-  ( K e. HL -> K e. Poset )
47 35 46 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> K e. Poset )
48 1 31 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 ) )
49 47 40 41 42 48 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> ( ( z ( le ` K ) X /\ X ( le ` K ) Y ) -> z ( le ` K ) Y ) )
50 34 45 49 mp2and 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z ( le ` K ) Y )
51 31 2 3 4 llncvrlpln2 
 |-  ( ( ( K e. HL /\ z e. N /\ Y e. P ) /\ z ( le ` K ) Y ) -> z C Y )
52 35 38 43 50 51 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z C Y )
53 simplr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> X C Y )
54 1 31 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 ) )
55 37 40 41 42 52 53 54 syl132anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> ( z ( le ` K ) X <-> z = X ) )
56 34 55 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> z = X )
57 56 38 eqeltrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ ( Y e. P /\ z e. N /\ z ( le ` K ) X ) ) -> X e. N )
58 57 3exp2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( Y e. P -> ( z e. N -> ( z ( le ` K ) X -> X e. N ) ) ) )
59 58 imp 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( z e. N -> ( z ( le ` K ) X -> X e. N ) ) )
60 59 rexlimdv 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> ( E. z e. N z ( le ` K ) X -> X e. N ) )
61 33 60 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ Y e. P ) -> X e. N )
62 10 61 impbida 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X e. N <-> Y e. P ) )