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 33114

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 761	. . . 4 $/\$ $/\$ $/\$ $/\$
2		eqid 2423	. . . . . 6
3		eqid 2423	. . . . . 6
4		eqid 2423	. . . . . 6
5		lvolnle3at.v	. . . . . 6
6	2, 3, 4, 5	islvol 33105	. . . . 5 $/\$
7	6	ad2antrr 731	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
8	1, 7	mpbid 214	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
9	8	simprd 465	. 2 $/\$ $/\$ $/\$ $/\$
10		oveq1 6311	. . . . . . . . 9 $.\/$ $.\/$
11	10	oveq1d 6319	. . . . . . . 8 $.\/$ $.\/$ $.\/$ $.\/$
12	11	breq2d 4434	. . . . . . 7 $.\/$ $.\/$ $.\/$ $.\/$
13	12	notbid 296	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
14		simp1l 1030	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp3l 1034	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp21 1039	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp22 1040	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		lvolnle3at.l	. . . . . . . . . . . . 13
19		lvolnle3at.j	. . . . . . . . . . . . 13 $.\/$
20		lvolnle3at.a	. . . . . . . . . . . . 13
21	18, 19, 20, 4	lplnnle2at 33073	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$
22	14, 15, 16, 17, 21	syl13anc 1267	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	2, 4	lplnbase 33066	. . . . . . . . . . . . . . 15
24	15, 23	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simp1r 1031	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	2, 5	lvolbase 33110	. . . . . . . . . . . . . . 15
27	25, 26	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		simp3r 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		eqid 2423	. . . . . . . . . . . . . . 15
30	2, 29, 3	cvrlt 32803	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
31	14, 24, 27, 28, 30	syl31anc 1268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		hlpos 32898	. . . . . . . . . . . . . . 15
33	14, 32	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	2, 19, 20	hlatjcl 32899	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
35	14, 16, 17, 34	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	2, 18, 29	pltletr 16214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	33, 24, 27, 35, 36	syl13anc 1267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
38	31, 37	mpand 680	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
39	18, 29	pltle 16204	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	14, 15, 35, 39	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
41	38, 40	syld 46	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
42	22, 41	mtod 181	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
43	42	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44		simprr 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
45		hllat 32896	. . . . . . . . . . . . . 14
46	14, 45	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		simp23 1041	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	2, 20	atbase 32822	. . . . . . . . . . . . . 14
49	47, 48	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	2, 18, 19	latleeqj2 16307	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	46, 49, 35, 50	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
52	51	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
53	44, 52	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
54	53	breq2d 4434	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	43, 54	mtbird 303	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
56	55	anassrs 653	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
57		simpl1l 1057	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
58		simpl3l 1061	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simpl2 1010	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
60		simpr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
61	18, 19, 20, 4	lplni2 33069	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
62	57, 59, 60, 61	syl3anc 1265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
63	29, 4	lplnnlt 33097	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
64	57, 58, 62, 63	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
65	2, 19	latjcl 16294	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$
66	46, 35, 49, 65	syl3anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	2, 18, 29	pltletr 16214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
68	33, 24, 27, 66, 67	syl13anc 1267	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	31, 68	mpand 680	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
70	69	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	64, 70	mtod 181	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
72	71	anassrs 653	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
73	56, 72	pm2.61dan 799	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
74		eqid 2423	. . . . . . . . . 10
75	74, 19, 20, 4	lplnnle2at 33073	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
76	14, 15, 17, 47, 75	syl13anc 1267	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
77	2, 19, 20	hlatjcl 32899	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
78	14, 17, 47, 77	syl3anc 1265	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
79	2, 18, 29	pltletr 16214	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80	33, 24, 27, 78, 79	syl13anc 1267	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	31, 80	mpand 680	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
82	74, 29	pltle 16204	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$
83	14, 15, 78, 82	syl3anc 1265	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
84	81, 83	syld 46	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
85	76, 84	mtod 181	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
86	19, 20	hlatjidm 32901	. . . . . . . . . 10 $/\$ $.\/$
87	14, 17, 86	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
88	87	oveq1d 6319	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
89	88	breq2d 4434	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
90	85, 89	mtbird 303	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
91	13, 73, 90	pm2.61ne 2740	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
92	91	3expia 1208	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
93	92	expd 438	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
94	93	rexlimdv 2916	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
95	9, 94	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wne 2619

wrex 2777 class class class wbr 4422

cfv 5600 (class class class)co 6304

cbs 15118

cple 15194

cpo 16182

cplt 16183

cjn 16186

clat 16288

ccvr 32795

catm 32796

chlt 32883

clpl 33024

clvol 33025

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4535 ax-sep 4545 ax-nul 4554 ax-pow 4601 ax-pr 4659 ax-un 6596

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-ral 2781 df-rex 2782 df-reu 2783 df-rab 2785 df-v 3084 df-sbc 3302 df-csb 3398 df-dif 3441 df-un 3443 df-in 3445 df-ss 3452 df-nul 3764 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4219 df-iun 4300 df-br 4423 df-opab 4482 df-mpt 4483 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-riota 6266 df-ov 6307 df-oprab 6308 df-preset 16170 df-poset 16188 df-plt 16201 df-lub 16217 df-glb 16218 df-join 16219 df-meet 16220 df-p0 16282 df-lat 16289 df-clat 16351 df-oposet 32709 df-ol 32711 df-oml 32712 df-covers 32799 df-ats 32800 df-atl 32831 df-cvlat 32855 df-hlat 32884 df-llines 33030 df-lplanes 33031 df-lvols 33032

This theorem is referenced by: lvolnleat 33115 lvolnlelln 33116 lvolnlelpln 33117 3atnelvolN 33118 4atlem3 33128 dalem39 33243

W3C validator