![]() |
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 4334 | . . . 4 β’ (π β π β Β¬ π = β ) | |
2 | lplnbase.p | . . . . 5 β’ π = (LPlanesβπΎ) | |
3 | 2 | eqeq1i 2738 | . . . 4 β’ (π = β β (LPlanesβπΎ) = β ) |
4 | 1, 3 | sylnib 328 | . . 3 β’ (π β π β Β¬ (LPlanesβπΎ) = β ) |
5 | fvprc 6884 | . . 3 β’ (Β¬ πΎ β V β (LPlanesβπΎ) = β ) | |
6 | 4, 5 | nsyl2 141 | . 2 β’ (π β π β πΎ β V) |
7 | lplnbase.b | . . . 4 β’ π΅ = (BaseβπΎ) | |
8 | eqid 2733 | . . . 4 β’ ( β βπΎ) = ( β βπΎ) | |
9 | eqid 2733 | . . . 4 β’ (LLinesβπΎ) = (LLinesβπΎ) | |
10 | 7, 8, 9, 2 | islpln 38401 | . . 3 β’ (πΎ β V β (π β π β (π β π΅ β§ βπ₯ β (LLinesβπΎ)π₯( β βπΎ)π))) |
11 | 10 | simprbda 500 | . 2 β’ ((πΎ β V β§ π β π) β π β π΅) |
12 | 6, 11 | mpancom 687 | 1 β’ (π β π β π β π΅) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 = wceq 1542 β wcel 2107 βwrex 3071 Vcvv 3475 β c0 4323 class class class wbr 5149 βcfv 6544 Basecbs 17144 β ccvr 38132 LLinesclln 38362 LPlanesclpl 38363 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6496 df-fun 6546 df-fv 6552 df-lplanes 38370 |
This theorem is referenced by: islpln2 38407 llnmlplnN 38410 lplnnle2at 38412 lplnneat 38416 lplnnelln 38417 llncvrlpln2 38428 2lplnmN 38430 lplncmp 38433 lplnexatN 38434 lplnexllnN 38435 2llnjaN 38437 islvol3 38447 lvoli3 38448 lvolnle3at 38453 lplncvrlvol2 38486 lplncvrlvol 38487 lvolcmp 38488 2lplnm2N 38492 2lplnmj 38493 dalemyeb 38520 dalem10 38544 dalem16 38550 dalem44 38587 dalem55 38598 |
Copyright terms: Public domain | W3C validator |