Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lplnexatN | Structured version Visualization version GIF version |
Description: Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
Ref | Expression |
---|---|
lplnexat.l | ⊢ ≤ = (le‘𝐾) |
lplnexat.j | ⊢ ∨ = (join‘𝐾) |
lplnexat.a | ⊢ 𝐴 = (Atoms‘𝐾) |
lplnexat.n | ⊢ 𝑁 = (LLines‘𝐾) |
lplnexat.p | ⊢ 𝑃 = (LPlanes‘𝐾) |
Ref | Expression |
---|---|
lplnexatN | ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1135 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → 𝐾 ∈ HL) | |
2 | simp3 1137 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → 𝑌 ∈ 𝑁) | |
3 | simp2 1136 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → 𝑋 ∈ 𝑃) | |
4 | 1, 2, 3 | 3jca 1127 | . . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → (𝐾 ∈ HL ∧ 𝑌 ∈ 𝑁 ∧ 𝑋 ∈ 𝑃)) |
5 | lplnexat.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
6 | eqid 2736 | . . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾) | |
7 | lplnexat.n | . . . 4 ⊢ 𝑁 = (LLines‘𝐾) | |
8 | lplnexat.p | . . . 4 ⊢ 𝑃 = (LPlanes‘𝐾) | |
9 | 5, 6, 7, 8 | llncvrlpln2 37825 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑁 ∧ 𝑋 ∈ 𝑃) ∧ 𝑌 ≤ 𝑋) → 𝑌( ⋖ ‘𝐾)𝑋) |
10 | 4, 9 | sylan 580 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝑌( ⋖ ‘𝐾)𝑋) |
11 | simpl1 1190 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝐾 ∈ HL) | |
12 | simpl3 1192 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝑌 ∈ 𝑁) | |
13 | eqid 2736 | . . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
14 | 13, 7 | llnbase 37777 | . . . . 5 ⊢ (𝑌 ∈ 𝑁 → 𝑌 ∈ (Base‘𝐾)) |
15 | 12, 14 | syl 17 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝑌 ∈ (Base‘𝐾)) |
16 | simpl2 1191 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝑋 ∈ 𝑃) | |
17 | 13, 8 | lplnbase 37802 | . . . . 5 ⊢ (𝑋 ∈ 𝑃 → 𝑋 ∈ (Base‘𝐾)) |
18 | 16, 17 | syl 17 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → 𝑋 ∈ (Base‘𝐾)) |
19 | lplnexat.j | . . . . 5 ⊢ ∨ = (join‘𝐾) | |
20 | lplnexat.a | . . . . 5 ⊢ 𝐴 = (Atoms‘𝐾) | |
21 | 13, 5, 19, 6, 20 | cvrval3 37681 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) → (𝑌( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ (𝑌 ∨ 𝑞) = 𝑋))) |
22 | 11, 15, 18, 21 | syl3anc 1370 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → (𝑌( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ (𝑌 ∨ 𝑞) = 𝑋))) |
23 | eqcom 2743 | . . . . 5 ⊢ ((𝑌 ∨ 𝑞) = 𝑋 ↔ 𝑋 = (𝑌 ∨ 𝑞)) | |
24 | 23 | anbi2i 623 | . . . 4 ⊢ ((¬ 𝑞 ≤ 𝑌 ∧ (𝑌 ∨ 𝑞) = 𝑋) ↔ (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞))) |
25 | 24 | rexbii 3093 | . . 3 ⊢ (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ (𝑌 ∨ 𝑞) = 𝑋) ↔ ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞))) |
26 | 22, 25 | bitrdi 286 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → (𝑌( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞)))) |
27 | 10, 26 | mpbid 231 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∃wrex 3070 class class class wbr 5092 ‘cfv 6479 (class class class)co 7337 Basecbs 17009 lecple 17066 joincjn 18126 ⋖ ccvr 37529 Atomscatm 37530 HLchlt 37617 LLinesclln 37759 LPlanesclpl 37760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-riota 7293 df-ov 7340 df-oprab 7341 df-proset 18110 df-poset 18128 df-plt 18145 df-lub 18161 df-glb 18162 df-join 18163 df-meet 18164 df-p0 18240 df-lat 18247 df-clat 18314 df-oposet 37443 df-ol 37445 df-oml 37446 df-covers 37533 df-ats 37534 df-atl 37565 df-cvlat 37589 df-hlat 37618 df-llines 37766 df-lplanes 37767 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |