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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
llncvrlpln.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
llncvrlpln.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
llncvrlpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion llncvrlpln ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑃 ) )

Proof

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