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 35108

Description: Lemma for dath 35183. 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 35070	. . 3
3	1	dalempea 35073	. . 3
4	1	dalemqea 35074	. . 3
5	1	dalemsea 35076	. . 3
6	1	dalemtea 35077	. . 3
7		dalemc.j	. . . 4 $.\/$
8		dalemc.a	. . . 4
9	7, 8	hlatj4 34821	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
10	2, 3, 4, 5, 6, 9	syl122anc 1236	. 2 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
11		dalemc.l	. . . . 5
12		dalem1.o	. . . . 5
13		dalem1.y	. . . . 5 $.\/$ $.\/$
14	1, 11, 7, 8, 12, 13	dalempjsen 35100	. . . 4 $.\/$
15	1, 11, 7, 8, 12, 13	dalemqnet 35099	. . . . 5
16		eqid 2441	. . . . . 6
17	7, 8, 16	llni2 34959	. . . . 5 $/\$ $/\$ $/\$ $.\/$
18	2, 4, 6, 15, 17	syl31anc 1230	. . . 4 $.\/$
19	1, 11, 7, 8, 12, 13	dalem1 35106	. . . 4 $.\/$ $.\/$
20	1, 11, 7, 8, 12, 13	dalemcea 35107	. . . . 5
21	1	dalemclpjs 35081	. . . . 5 $.\/$
22	1	dalemclqjt 35082	. . . . 5 $.\/$
23		eqid 2441	. . . . . 6
24		eqid 2441	. . . . . 6
25	11, 23, 24, 8, 16	2llnm4 35017	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
26	2, 20, 14, 18, 21, 22, 25	syl132anc 1245	. . . 4 $.\/$ $.\/$
27	23, 24, 8, 16	2llnmat 34971	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
28	2, 14, 18, 19, 26, 27	syl32anc 1235	. . 3 $.\/$ $.\/$
29	7, 23, 8, 16, 12	2llnmj 35007	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
30	2, 14, 18, 29	syl3anc 1227	. . 3 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31	28, 30	mpbid 210	. 2 $.\/$ $.\/$ $.\/$
32	10, 31	eqeltrd 2529	1 $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 972

wceq 1381

wcel 1802

wne 2636 class class class wbr 4434

cfv 5575 (class class class)co 6278

cbs 14506

cple 14578

cjn 15444

cmee 15445

cp0 15538

catm 34711

chlt 34798

clln 34938

clpl 34939

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4545 ax-sep 4555 ax-nul 4563 ax-pow 4612 ax-pr 4673 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-ral 2796 df-rex 2797 df-reu 2798 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3419 df-dif 3462 df-un 3464 df-in 3466 df-ss 3473 df-nul 3769 df-if 3924 df-pw 3996 df-sn 4012 df-pr 4014 df-op 4018 df-uni 4232 df-iun 4314 df-br 4435 df-opab 4493 df-mpt 4494 df-id 4782 df-xp 4992 df-rel 4993 df-cnv 4994 df-co 4995 df-dm 4996 df-rn 4997 df-res 4998 df-ima 4999 df-iota 5538 df-fun 5577 df-fn 5578 df-f 5579 df-f1 5580 df-fo 5581 df-f1o 5582 df-fv 5583 df-riota 6239 df-ov 6281 df-oprab 6282 df-preset 15428 df-poset 15446 df-plt 15459 df-lub 15475 df-glb 15476 df-join 15477 df-meet 15478 df-p0 15540 df-lat 15547 df-clat 15609 df-oposet 34624 df-ol 34626 df-oml 34627 df-covers 34714 df-ats 34715 df-atl 34746 df-cvlat 34770 df-hlat 34799 df-llines 34945 df-lplanes 34946

This theorem is referenced by: dalemdea 35109

W3C validator