dalem2 - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalem2		Structured version Unicode version

Theorem dalem2 35798

Description: Lemma for dath 35873. Show the lines

and

form a plane. (Contributed by NM, 11-Aug-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalemc.l
dalemc.j	$.\/$
dalemc.a
dalem1.o
dalem1.y	$.\/$ $.\/$

**Assertion**
Ref	Expression
dalem2	$.\/$ $.\/$ $.\/$

**Proof of Theorem dalem2**
Step	Hyp	Ref	Expression
1		dalema.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemkehl 35760	. . 3
3	1	dalempea 35763	. . 3
4	1	dalemqea 35764	. . 3
5	1	dalemsea 35766	. . 3
6	1	dalemtea 35767	. . 3
7		dalemc.j	. . . 4 $.\/$
8		dalemc.a	. . . 4
9	7, 8	hlatj4 35511	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
10	2, 3, 4, 5, 6, 9	syl122anc 1235	. 2 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
11		dalemc.l	. . . . 5
12		dalem1.o	. . . . 5
13		dalem1.y	. . . . 5 $.\/$ $.\/$
14	1, 11, 7, 8, 12, 13	dalempjsen 35790	. . . 4 $.\/$
15	1, 11, 7, 8, 12, 13	dalemqnet 35789	. . . . 5
16		eqid 2382	. . . . . 6
17	7, 8, 16	llni2 35649	. . . . 5 $/\$ $/\$ $/\$ $.\/$
18	2, 4, 6, 15, 17	syl31anc 1229	. . . 4 $.\/$
19	1, 11, 7, 8, 12, 13	dalem1 35796	. . . 4 $.\/$ $.\/$
20	1, 11, 7, 8, 12, 13	dalemcea 35797	. . . . 5
21	1	dalemclpjs 35771	. . . . 5 $.\/$
22	1	dalemclqjt 35772	. . . . 5 $.\/$
23		eqid 2382	. . . . . 6
24		eqid 2382	. . . . . 6
25	11, 23, 24, 8, 16	2llnm4 35707	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
26	2, 20, 14, 18, 21, 22, 25	syl132anc 1244	. . . 4 $.\/$ $.\/$
27	23, 24, 8, 16	2llnmat 35661	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
28	2, 14, 18, 19, 26, 27	syl32anc 1234	. . 3 $.\/$ $.\/$
29	7, 23, 8, 16, 12	2llnmj 35697	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
30	2, 14, 18, 29	syl3anc 1226	. . 3 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31	28, 30	mpbid 210	. 2 $.\/$ $.\/$ $.\/$
32	10, 31	eqeltrd 2470	1 $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wne 2577 class class class wbr 4367

cfv 5496 (class class class)co 6196

cbs 14634

cple 14709

cjn 15690

cmee 15691

cp0 15784

catm 35401

chlt 35488

clln 35628

clpl 35629

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-preset 15674 df-poset 15692 df-plt 15705 df-lub 15721 df-glb 15722 df-join 15723 df-meet 15724 df-p0 15786 df-lat 15793 df-clat 15855 df-oposet 35314 df-ol 35316 df-oml 35317 df-covers 35404 df-ats 35405 df-atl 35436 df-cvlat 35460 df-hlat 35489 df-llines 35635 df-lplanes 35636

This theorem is referenced by: dalemdea 35799

W3C validator