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 = K
llncvrlpln.n N = LLines K
llncvrlpln.p P = LPlanes K
Assertion llncvrlpln K HL X B Y B X C Y X N Y P

Proof

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