llnmlplnN - Mathbox for Norm Megill

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

Theorem llnmlplnN 35364

Description: The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
llnmlpln.l
llnmlpln.m	$./\$
llnmlpln.z
llnmlpln.a
llnmlpln.n
llnmlpln.p

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

Proof of Theorem llnmlplnN Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 756	. 2 $/\$ $/\$ $/\$ $/\$ $./\$
2		simp11 1026	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
3		hllat 35189	. . . . . . . 8
4	2, 3	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
5		simp12 1027	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
6		eqid 2457	. . . . . . . . 9
7		llnmlpln.n	. . . . . . . . 9
8	6, 7	llnbase 35334	. . . . . . . 8
9	5, 8	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
10		simp13 1028	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
11		llnmlpln.p	. . . . . . . . 9
12	6, 11	lplnbase 35359	. . . . . . . 8
13	10, 12	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
14		llnmlpln.m	. . . . . . . 8 $./\$
15	6, 14	latmcl 15808	. . . . . . 7 $/\$ $/\$ $./\$
16	4, 9, 13, 15	syl3anc 1228	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17		simp2r 1023	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
18		simp3 998	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
19		llnmlpln.l	. . . . . . 7
20		llnmlpln.z	. . . . . . 7
21		llnmlpln.a	. . . . . . 7
22	6, 19, 20, 21, 7	llnle 35343	. . . . . 6 $/\$ $./\$ $/\$ $./\$ $/\$ $./\$ $./\$
23	2, 16, 17, 18, 22	syl22anc 1229	. . . . 5 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
24	4	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
25	16	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
26	9	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
27	6, 19, 14	latmle1 15832	. . . . . . . 8 $/\$ $/\$ $./\$
28	4, 9, 13, 27	syl3anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
29	28	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
30	6, 7	llnbase 35334	. . . . . . . . . 10
31	30	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
32		simprr 757	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
33	6, 19, 24, 31, 25, 26, 32, 29	lattrd 15814	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
34		simpl11 1071	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
35		simprl 756	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
36		simpl12 1072	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
37	19, 7	llncmp 35347	. . . . . . . . 9 $/\$ $/\$
38	34, 35, 36, 37	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
39	33, 38	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
40	39, 32	eqbrtrrd 4478	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
41	6, 19, 24, 25, 26, 29, 40	latasymd 15813	. . . . 5 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
42	23, 41	rexlimddv 2953	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
43	6, 19, 14	latleeqm1 15835	. . . . 5 $/\$ $/\$ $./\$
44	4, 9, 13, 43	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
45	42, 44	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
46	45	3expia 1198	. 2 $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
47	1, 46	mt3d 125	1 $/\$ $/\$ $/\$ $/\$ $./\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wcel 1819

wne 2652

wrex 2808 class class class wbr 4456

cfv 5594 (class class class)co 6296

cbs 14643

cple 14718

cmee 15700

cp0 15793

clat 15801

catm 35089

chlt 35176

clln 35316

clpl 35317

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-preset 15683 df-poset 15701 df-plt 15714 df-lub 15730 df-glb 15731 df-join 15732 df-meet 15733 df-p0 15795 df-lat 15802 df-clat 15864 df-oposet 35002 df-ol 35004 df-oml 35005 df-covers 35092 df-ats 35093 df-atl 35124 df-cvlat 35148 df-hlat 35177 df-llines 35323 df-lplanes 35324

This theorem is referenced by: (None)

W3C validator