lvolnle3at - Mathbox for Norm Megill

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

Theorem lvolnle3at 33143

Description: A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.)

**Hypotheses**
Ref	Expression
lvolnle3at.l
lvolnle3at.j	$.\/$
lvolnle3at.a
lvolnle3at.v

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

Proof of Theorem lvolnle3at Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 754	. . . 4 $/\$ $/\$ $/\$ $/\$
2		eqid 2438	. . . . . 6
3		eqid 2438	. . . . . 6
4		eqid 2438	. . . . . 6
5		lvolnle3at.v	. . . . . 6
6	2, 3, 4, 5	islvol 33134	. . . . 5 $/\$
7	6	ad2antrr 725	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
8	1, 7	mpbid 210	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
9	8	simprd 463	. 2 $/\$ $/\$ $/\$ $/\$
10		oveq1 6093	. . . . . . . . 9 $.\/$ $.\/$
11	10	oveq1d 6101	. . . . . . . 8 $.\/$ $.\/$ $.\/$ $.\/$
12	11	breq2d 4299	. . . . . . 7 $.\/$ $.\/$ $.\/$ $.\/$
13	12	notbid 294	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
14		simp1l 1012	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp3l 1016	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp21 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp22 1022	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		lvolnle3at.l	. . . . . . . . . . . . 13
19		lvolnle3at.j	. . . . . . . . . . . . 13 $.\/$
20		lvolnle3at.a	. . . . . . . . . . . . 13
21	18, 19, 20, 4	lplnnle2at 33102	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$
22	14, 15, 16, 17, 21	syl13anc 1220	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	2, 4	lplnbase 33095	. . . . . . . . . . . . . . 15
24	15, 23	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simp1r 1013	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	2, 5	lvolbase 33139	. . . . . . . . . . . . . . 15
27	25, 26	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		simp3r 1017	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		eqid 2438	. . . . . . . . . . . . . . 15
30	2, 29, 3	cvrlt 32832	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
31	14, 24, 27, 28, 30	syl31anc 1221	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		hlpos 32927	. . . . . . . . . . . . . . 15
33	14, 32	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	2, 19, 20	hlatjcl 32928	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
35	14, 16, 17, 34	syl3anc 1218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	2, 18, 29	pltletr 15133	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	33, 24, 27, 35, 36	syl13anc 1220	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
38	31, 37	mpand 675	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
39	18, 29	pltle 15123	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	14, 15, 35, 39	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
41	38, 40	syld 44	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
42	22, 41	mtod 177	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
43	42	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44		simprr 756	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
45		hllat 32925	. . . . . . . . . . . . . 14
46	14, 45	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		simp23 1023	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	2, 20	atbase 32851	. . . . . . . . . . . . . 14
49	47, 48	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	2, 18, 19	latleeqj2 15226	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	46, 49, 35, 50	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
52	51	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
53	44, 52	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
54	53	breq2d 4299	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	43, 54	mtbird 301	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
56	55	anassrs 648	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
57		simpl1l 1039	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
58		simpl3l 1043	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simpl2 992	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
60		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
61	18, 19, 20, 4	lplni2 33098	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
62	57, 59, 60, 61	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
63	29, 4	lplnnlt 33126	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
64	57, 58, 62, 63	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
65	2, 19	latjcl 15213	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$
66	46, 35, 49, 65	syl3anc 1218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	2, 18, 29	pltletr 15133	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
68	33, 24, 27, 66, 67	syl13anc 1220	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	31, 68	mpand 675	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
70	69	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	64, 70	mtod 177	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
72	71	anassrs 648	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
73	56, 72	pm2.61dan 789	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
74		eqid 2438	. . . . . . . . . 10
75	74, 19, 20, 4	lplnnle2at 33102	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
76	14, 15, 17, 47, 75	syl13anc 1220	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
77	2, 19, 20	hlatjcl 32928	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
78	14, 17, 47, 77	syl3anc 1218	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
79	2, 18, 29	pltletr 15133	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80	33, 24, 27, 78, 79	syl13anc 1220	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	31, 80	mpand 675	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
82	74, 29	pltle 15123	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$
83	14, 15, 78, 82	syl3anc 1218	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
84	81, 83	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
85	76, 84	mtod 177	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
86	19, 20	hlatjidm 32930	. . . . . . . . . 10 $/\$ $.\/$
87	14, 17, 86	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
88	87	oveq1d 6101	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
89	88	breq2d 4299	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
90	85, 89	mtbird 301	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
91	13, 73, 90	pm2.61ne 2681	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
92	91	3expia 1189	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
93	92	expd 436	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
94	93	rexlimdv 2835	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
95	9, 94	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2601

wrex 2711 class class class wbr 4287

cfv 5413 (class class class)co 6086

cbs 14166

cple 14237

cpo 15102

cplt 15103

cjn 15106

clat 15207

ccvr 32824

catm 32825

chlt 32912

clpl 33053

clvol 33054

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 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

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 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-lat 15208 df-clat 15270 df-oposet 32738 df-ol 32740 df-oml 32741 df-covers 32828 df-ats 32829 df-atl 32860 df-cvlat 32884 df-hlat 32913 df-llines 33059 df-lplanes 33060 df-lvols 33061

This theorem is referenced by: lvolnleat 33144 lvolnlelln 33145 lvolnlelpln 33146 3atnelvolN 33147 4atlem3 33157 dalem39 33272

W3C validator