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 33183

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 755	. 2 $/\$ $/\$ $/\$ $/\$ $./\$
2		simp11 1018	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
3		hllat 33008	. . . . . . . 8
4	2, 3	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
5		simp12 1019	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
6		eqid 2443	. . . . . . . . 9
7		llnmlpln.n	. . . . . . . . 9
8	6, 7	llnbase 33153	. . . . . . . 8
9	5, 8	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
10		simp13 1020	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
11		llnmlpln.p	. . . . . . . . 9
12	6, 11	lplnbase 33178	. . . . . . . 8
13	10, 12	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
14		llnmlpln.m	. . . . . . . 8 $./\$
15	6, 14	latmcl 15222	. . . . . . 7 $/\$ $/\$ $./\$
16	4, 9, 13, 15	syl3anc 1218	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
17		simp2r 1015	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
18		simp3 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
19		llnmlpln.l	. . . . . . 7
20		llnmlpln.z	. . . . . . 7
21		llnmlpln.a	. . . . . . 7
22	6, 19, 20, 21, 7	llnle 33162	. . . . . 6 $/\$ $./\$ $/\$ $./\$ $/\$ $./\$ $./\$
23	2, 16, 17, 18, 22	syl22anc 1219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
24	4	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
25	16	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
26	9	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
27	6, 19, 14	latmle1 15246	. . . . . . . 8 $/\$ $/\$ $./\$
28	4, 9, 13, 27	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
29	28	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
30	6, 7	llnbase 33153	. . . . . . . . . 10
31	30	ad2antrl 727	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
32		simprr 756	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
33	6, 19, 24, 31, 25, 26, 32, 29	lattrd 15228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
34		simpl11 1063	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
35		simprl 755	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
36		simpl12 1064	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
37	19, 7	llncmp 33166	. . . . . . . . 9 $/\$ $/\$
38	34, 35, 36, 37	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
39	33, 38	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$
40	39, 32	eqbrtrrd 4314	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
41	6, 19, 24, 25, 26, 29, 40	latasymd 15227	. . . . 5 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $/\$ $/\$ $./\$ $./\$
42	23, 41	rexlimddv 2845	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
43	6, 19, 14	latleeqm1 15249	. . . . 5 $/\$ $/\$ $./\$
44	4, 9, 13, 43	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$ $./\$
45	42, 44	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$ $./\$ $/\$ $./\$
46	45	3expia 1189	. 2 $/\$ $/\$ $/\$ $/\$ $./\$ $./\$
47	1, 46	mt3d 125	1 $/\$ $/\$ $/\$ $/\$ $./\$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2606

wrex 2716 class class class wbr 4292

cfv 5418 (class class class)co 6091

cbs 14174

cple 14245

cmee 15115

cp0 15207

clat 15215

catm 32908

chlt 32995

clln 33135

clpl 33136

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-id 4636 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-poset 15116 df-plt 15128 df-lub 15144 df-glb 15145 df-join 15146 df-meet 15147 df-p0 15209 df-lat 15216 df-clat 15278 df-oposet 32821 df-ol 32823 df-oml 32824 df-covers 32911 df-ats 32912 df-atl 32943 df-cvlat 32967 df-hlat 32996 df-llines 33142 df-lplanes 33143

This theorem is referenced by: (None)

W3C validator