![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lplnbase | Structured version Visualization version GIF version |
Description: A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012.) |
Ref | Expression |
---|---|
lplnbase.b | ⊢ 𝐵 = (Base‘𝐾) |
lplnbase.p | ⊢ 𝑃 = (LPlanes‘𝐾) |
Ref | Expression |
---|---|
lplnbase | ⊢ (𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 4148 | . . . 4 ⊢ (𝑋 ∈ 𝑃 → ¬ 𝑃 = ∅) | |
2 | lplnbase.p | . . . . 5 ⊢ 𝑃 = (LPlanes‘𝐾) | |
3 | 2 | eqeq1i 2783 | . . . 4 ⊢ (𝑃 = ∅ ↔ (LPlanes‘𝐾) = ∅) |
4 | 1, 3 | sylnib 320 | . . 3 ⊢ (𝑋 ∈ 𝑃 → ¬ (LPlanes‘𝐾) = ∅) |
5 | fvprc 6441 | . . 3 ⊢ (¬ 𝐾 ∈ V → (LPlanes‘𝐾) = ∅) | |
6 | 4, 5 | nsyl2 145 | . 2 ⊢ (𝑋 ∈ 𝑃 → 𝐾 ∈ V) |
7 | lplnbase.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
8 | eqid 2778 | . . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾) | |
9 | eqid 2778 | . . . 4 ⊢ (LLines‘𝐾) = (LLines‘𝐾) | |
10 | 7, 8, 9, 2 | islpln 35689 | . . 3 ⊢ (𝐾 ∈ V → (𝑋 ∈ 𝑃 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑥 ∈ (LLines‘𝐾)𝑥( ⋖ ‘𝐾)𝑋))) |
11 | 10 | simprbda 494 | . 2 ⊢ ((𝐾 ∈ V ∧ 𝑋 ∈ 𝑃) → 𝑋 ∈ 𝐵) |
12 | 6, 11 | mpancom 678 | 1 ⊢ (𝑋 ∈ 𝑃 → 𝑋 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ∃wrex 3091 Vcvv 3398 ∅c0 4141 class class class wbr 4888 ‘cfv 6137 Basecbs 16259 ⋖ ccvr 35421 LLinesclln 35650 LPlanesclpl 35651 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-iota 6101 df-fun 6139 df-fv 6145 df-lplanes 35658 |
This theorem is referenced by: islpln2 35695 llnmlplnN 35698 lplnnle2at 35700 lplnneat 35704 lplnnelln 35705 llncvrlpln2 35716 2lplnmN 35718 lplncmp 35721 lplnexatN 35722 lplnexllnN 35723 2llnjaN 35725 islvol3 35735 lvoli3 35736 lvolnle3at 35741 lplncvrlvol2 35774 lplncvrlvol 35775 lvolcmp 35776 2lplnm2N 35780 2lplnmj 35781 dalemyeb 35808 dalem10 35832 dalem16 35838 dalem44 35875 dalem55 35886 |
Copyright terms: Public domain | W3C validator |