Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalem15 | Structured version Visualization version GIF version |
Description: Lemma for dath 38004. The axis of perspectivity π is a line. (Contributed by NM, 21-Jul-2012.) |
Ref | Expression |
---|---|
dalema.ph | β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) |
dalemc.l | β’ β€ = (leβπΎ) |
dalemc.j | β’ β¨ = (joinβπΎ) |
dalemc.a | β’ π΄ = (AtomsβπΎ) |
dalem15.m | β’ β§ = (meetβπΎ) |
dalem15.n | β’ π = (LLinesβπΎ) |
dalem15.o | β’ π = (LPlanesβπΎ) |
dalem15.y | β’ π = ((π β¨ π) β¨ π ) |
dalem15.z | β’ π = ((π β¨ π) β¨ π) |
dalem15.x | β’ π = (π β§ π) |
Ref | Expression |
---|---|
dalem15 | β’ ((π β§ π β π) β π β π) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalem15.x | . 2 β’ π = (π β§ π) | |
2 | dalema.ph | . . . 4 β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) | |
3 | dalemc.l | . . . 4 β’ β€ = (leβπΎ) | |
4 | dalemc.j | . . . 4 β’ β¨ = (joinβπΎ) | |
5 | dalemc.a | . . . 4 β’ π΄ = (AtomsβπΎ) | |
6 | dalem15.o | . . . 4 β’ π = (LPlanesβπΎ) | |
7 | eqid 2736 | . . . 4 β’ (LVolsβπΎ) = (LVolsβπΎ) | |
8 | dalem15.y | . . . 4 β’ π = ((π β¨ π) β¨ π ) | |
9 | dalem15.z | . . . 4 β’ π = ((π β¨ π) β¨ π) | |
10 | eqid 2736 | . . . 4 β’ (π β¨ πΆ) = (π β¨ πΆ) | |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | dalem14 37945 | . . 3 β’ ((π β§ π β π) β (π β¨ π) β (LVolsβπΎ)) |
12 | 2 | dalemkehl 37891 | . . . . 5 β’ (π β πΎ β HL) |
13 | 2 | dalemyeo 37900 | . . . . 5 β’ (π β π β π) |
14 | 2 | dalemzeo 37901 | . . . . 5 β’ (π β π β π) |
15 | dalem15.m | . . . . . 6 β’ β§ = (meetβπΎ) | |
16 | dalem15.n | . . . . . 6 β’ π = (LLinesβπΎ) | |
17 | 4, 15, 16, 6, 7 | 2lplnmj 37890 | . . . . 5 β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β§ π) β π β (π β¨ π) β (LVolsβπΎ))) |
18 | 12, 13, 14, 17 | syl3anc 1370 | . . . 4 β’ (π β ((π β§ π) β π β (π β¨ π) β (LVolsβπΎ))) |
19 | 18 | adantr 481 | . . 3 β’ ((π β§ π β π) β ((π β§ π) β π β (π β¨ π) β (LVolsβπΎ))) |
20 | 11, 19 | mpbird 256 | . 2 β’ ((π β§ π β π) β (π β§ π) β π) |
21 | 1, 20 | eqeltrid 2841 | 1 β’ ((π β§ π β π) β π β π) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β wb 205 β§ wa 396 β§ w3a 1086 = wceq 1540 β wcel 2105 β wne 2940 class class class wbr 5092 βcfv 6479 (class class class)co 7337 Basecbs 17009 lecple 17066 joincjn 18126 meetcmee 18127 Atomscatm 37530 HLchlt 37617 LLinesclln 37759 LPlanesclpl 37760 LVolsclvol 37761 |
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-3or 1087 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 df-lvols 37768 |
This theorem is referenced by: dalem16 37947 dalem53 37993 |
Copyright terms: Public domain | W3C validator |