Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lplnnle2at Structured version   Visualization version   GIF version

Theorem lplnnle2at 34307
 Description: A lattice line (or atom) cannot majorize a lattice plane. (Contributed by NM, 8-Jul-2012.)
Hypotheses
Ref Expression
lplnnle2at.l = (le‘𝐾)
lplnnle2at.j = (join‘𝐾)
lplnnle2at.a 𝐴 = (Atoms‘𝐾)
lplnnle2at.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
lplnnle2at ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → ¬ 𝑋 (𝑄 𝑅))

Proof of Theorem lplnnle2at
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simpr1 1065 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → 𝑋𝑃)
2 eqid 2621 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
3 eqid 2621 . . . . . 6 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4 eqid 2621 . . . . . 6 (LLines‘𝐾) = (LLines‘𝐾)
5 lplnnle2at.p . . . . . 6 𝑃 = (LPlanes‘𝐾)
62, 3, 4, 5islpln 34296 . . . . 5 (𝐾 ∈ HL → (𝑋𝑃 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LLines‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
76adantr 481 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → (𝑋𝑃 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LLines‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
81, 7mpbid 222 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LLines‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
98simprd 479 . 2 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → ∃𝑦 ∈ (LLines‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10 oveq1 6611 . . . . . . . . 9 (𝑄 = 𝑅 → (𝑄 𝑅) = (𝑅 𝑅))
1110breq2d 4625 . . . . . . . 8 (𝑄 = 𝑅 → (𝑋 (𝑄 𝑅) ↔ 𝑋 (𝑅 𝑅)))
1211notbid 308 . . . . . . 7 (𝑄 = 𝑅 → (¬ 𝑋 (𝑄 𝑅) ↔ ¬ 𝑋 (𝑅 𝑅)))
13 simpl1 1062 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝐾 ∈ HL)
14 simpl3l 1114 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑦 ∈ (LLines‘𝐾))
15 simpl22 1138 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑄𝐴)
16 simpl23 1139 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑅𝐴)
17 simpr 477 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑄𝑅)
18 lplnnle2at.j . . . . . . . . . . 11 = (join‘𝐾)
19 lplnnle2at.a . . . . . . . . . . 11 𝐴 = (Atoms‘𝐾)
2018, 19, 4llni2 34278 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) ∧ 𝑄𝑅) → (𝑄 𝑅) ∈ (LLines‘𝐾))
2113, 15, 16, 17, 20syl31anc 1326 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → (𝑄 𝑅) ∈ (LLines‘𝐾))
22 eqid 2621 . . . . . . . . . 10 (lt‘𝐾) = (lt‘𝐾)
2322, 4llnnlt 34289 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LLines‘𝐾) ∧ (𝑄 𝑅) ∈ (LLines‘𝐾)) → ¬ 𝑦(lt‘𝐾)(𝑄 𝑅))
2413, 14, 21, 23syl3anc 1323 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → ¬ 𝑦(lt‘𝐾)(𝑄 𝑅))
252, 4llnbase 34275 . . . . . . . . . . 11 (𝑦 ∈ (LLines‘𝐾) → 𝑦 ∈ (Base‘𝐾))
2614, 25syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑦 ∈ (Base‘𝐾))
27 simpl21 1137 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑋𝑃)
282, 5lplnbase 34300 . . . . . . . . . . 11 (𝑋𝑃𝑋 ∈ (Base‘𝐾))
2927, 28syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑋 ∈ (Base‘𝐾))
30 simpl3r 1115 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑦( ⋖ ‘𝐾)𝑋)
312, 22, 3cvrlt 34037 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
3213, 26, 29, 30, 31syl31anc 1326 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝑦(lt‘𝐾)𝑋)
33 hlpos 34132 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ Poset)
3413, 33syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → 𝐾 ∈ Poset)
352, 18, 19hlatjcl 34133 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
3613, 15, 16, 35syl3anc 1323 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → (𝑄 𝑅) ∈ (Base‘𝐾))
37 lplnnle2at.l . . . . . . . . . . 11 = (le‘𝐾)
382, 37, 22pltletr 16892 . . . . . . . . . 10 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
3934, 26, 29, 36, 38syl13anc 1325 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
4032, 39mpand 710 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → (𝑋 (𝑄 𝑅) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
4124, 40mtod 189 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑄𝑅) → ¬ 𝑋 (𝑄 𝑅))
42 simp1 1059 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
43 simp3l 1087 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LLines‘𝐾))
44 simp23 1094 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅𝐴)
4537, 19, 4llnnleat 34279 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LLines‘𝐾) ∧ 𝑅𝐴) → ¬ 𝑦 𝑅)
4642, 43, 44, 45syl3anc 1323 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 𝑅)
4743, 25syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
48 simp21 1092 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋𝑃)
4948, 28syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
50 simp3r 1088 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
5142, 47, 49, 50, 31syl31anc 1326 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
52333ad2ant1 1080 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
532, 19atbase 34056 . . . . . . . . . . . . 13 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
5444, 53syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
552, 37, 22pltletr 16892 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 𝑅) → 𝑦(lt‘𝐾)𝑅))
5652, 47, 49, 54, 55syl13anc 1325 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 𝑅) → 𝑦(lt‘𝐾)𝑅))
5751, 56mpand 710 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 𝑅𝑦(lt‘𝐾)𝑅))
5837, 22pltle 16882 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LLines‘𝐾) ∧ 𝑅𝐴) → (𝑦(lt‘𝐾)𝑅𝑦 𝑅))
5942, 43, 44, 58syl3anc 1323 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)𝑅𝑦 𝑅))
6057, 59syld 47 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 𝑅𝑦 𝑅))
6146, 60mtod 189 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 𝑅)
6218, 19hlatjidm 34135 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑅𝐴) → (𝑅 𝑅) = 𝑅)
6342, 44, 62syl2anc 692 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 𝑅) = 𝑅)
6463breq2d 4625 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑅 𝑅) ↔ 𝑋 𝑅))
6561, 64mtbird 315 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑅 𝑅))
6612, 41, 65pm2.61ne 2875 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑄 𝑅))
67663exp 1261 . . . . 5 (𝐾 ∈ HL → ((𝑋𝑃𝑄𝐴𝑅𝐴) → ((𝑦 ∈ (LLines‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 (𝑄 𝑅))))
6867exp4a 632 . . . 4 (𝐾 ∈ HL → ((𝑋𝑃𝑄𝐴𝑅𝐴) → (𝑦 ∈ (LLines‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 (𝑄 𝑅)))))
6968imp 445 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → (𝑦 ∈ (LLines‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 (𝑄 𝑅))))
7069rexlimdv 3023 . 2 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → (∃𝑦 ∈ (LLines‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 (𝑄 𝑅)))
719, 70mpd 15 1 ((𝐾 ∈ HL ∧ (𝑋𝑃𝑄𝐴𝑅𝐴)) → ¬ 𝑋 (𝑄 𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908   class class class wbr 4613  ‘cfv 5847  (class class class)co 6604  Basecbs 15781  lecple 15869  Posetcpo 16861  ltcplt 16862  joincjn 16865   ⋖ ccvr 34029  Atomscatm 34030  HLchlt 34117  LLinesclln 34257  LPlanesclpl 34258 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-preset 16849  df-poset 16867  df-plt 16879  df-lub 16895  df-glb 16896  df-join 16897  df-meet 16898  df-p0 16960  df-lat 16967  df-clat 17029  df-oposet 33943  df-ol 33945  df-oml 33946  df-covers 34033  df-ats 34034  df-atl 34065  df-cvlat 34089  df-hlat 34118  df-llines 34264  df-lplanes 34265 This theorem is referenced by:  lplnnleat  34308  lplnnlelln  34309  2atnelpln  34310  lvolnle3at  34348
 Copyright terms: Public domain W3C validator