lvolnle3at - Mathbox for Norm Megill

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

Theorem lvolnle3at 33218

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 770	. . . 4 $/\$ $/\$ $/\$ $/\$
2		eqid 2471	. . . . . 6
3		eqid 2471	. . . . . 6
4		eqid 2471	. . . . . 6
5		lvolnle3at.v	. . . . . 6
6	2, 3, 4, 5	islvol 33209	. . . . 5 $/\$
7	6	ad2antrr 740	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
8	1, 7	mpbid 215	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
9	8	simprd 470	. 2 $/\$ $/\$ $/\$ $/\$
10		oveq1 6315	. . . . . . . . 9 $.\/$ $.\/$
11	10	oveq1d 6323	. . . . . . . 8 $.\/$ $.\/$ $.\/$ $.\/$
12	11	breq2d 4407	. . . . . . 7 $.\/$ $.\/$ $.\/$ $.\/$
13	12	notbid 301	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
14		simp1l 1054	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp3l 1058	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp21 1063	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp22 1064	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		lvolnle3at.l	. . . . . . . . . . . . 13
19		lvolnle3at.j	. . . . . . . . . . . . 13 $.\/$
20		lvolnle3at.a	. . . . . . . . . . . . 13
21	18, 19, 20, 4	lplnnle2at 33177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$
22	14, 15, 16, 17, 21	syl13anc 1294	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	2, 4	lplnbase 33170	. . . . . . . . . . . . . . 15
24	15, 23	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simp1r 1055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	2, 5	lvolbase 33214	. . . . . . . . . . . . . . 15
27	25, 26	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		simp3r 1059	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		eqid 2471	. . . . . . . . . . . . . . 15
30	2, 29, 3	cvrlt 32907	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
31	14, 24, 27, 28, 30	syl31anc 1295	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		hlpos 33002	. . . . . . . . . . . . . . 15
33	14, 32	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	2, 19, 20	hlatjcl 33003	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
35	14, 16, 17, 34	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	2, 18, 29	pltletr 16295	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	33, 24, 27, 35, 36	syl13anc 1294	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
38	31, 37	mpand 689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
39	18, 29	pltle 16285	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	14, 15, 35, 39	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
41	38, 40	syld 44	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
42	22, 41	mtod 182	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
43	42	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44		simprr 774	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
45		hllat 33000	. . . . . . . . . . . . . 14
46	14, 45	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		simp23 1065	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	2, 20	atbase 32926	. . . . . . . . . . . . . 14
49	47, 48	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	2, 18, 19	latleeqj2 16388	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	46, 49, 35, 50	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
52	51	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
53	44, 52	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
54	53	breq2d 4407	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	43, 54	mtbird 308	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
56	55	anassrs 660	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
57		simpl1l 1081	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
58		simpl3l 1085	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simpl2 1034	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
60		simpr 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
61	18, 19, 20, 4	lplni2 33173	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
62	57, 59, 60, 61	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
63	29, 4	lplnnlt 33201	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
64	57, 58, 62, 63	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
65	2, 19	latjcl 16375	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$
66	46, 35, 49, 65	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	2, 18, 29	pltletr 16295	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
68	33, 24, 27, 66, 67	syl13anc 1294	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	31, 68	mpand 689	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
70	69	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	64, 70	mtod 182	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
72	71	anassrs 660	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
73	56, 72	pm2.61dan 808	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
74		eqid 2471	. . . . . . . . . 10
75	74, 19, 20, 4	lplnnle2at 33177	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
76	14, 15, 17, 47, 75	syl13anc 1294	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
77	2, 19, 20	hlatjcl 33003	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
78	14, 17, 47, 77	syl3anc 1292	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
79	2, 18, 29	pltletr 16295	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80	33, 24, 27, 78, 79	syl13anc 1294	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	31, 80	mpand 689	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
82	74, 29	pltle 16285	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$
83	14, 15, 78, 82	syl3anc 1292	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
84	81, 83	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
85	76, 84	mtod 182	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
86	19, 20	hlatjidm 33005	. . . . . . . . . 10 $/\$ $.\/$
87	14, 17, 86	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
88	87	oveq1d 6323	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
89	88	breq2d 4407	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
90	85, 89	mtbird 308	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
91	13, 73, 90	pm2.61ne 2728	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
92	91	3expia 1233	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
93	92	expd 443	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
94	93	rexlimdv 2870	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
95	9, 94	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wrex 2757 class class class wbr 4395

cfv 5589 (class class class)co 6308

cbs 15199

cple 15275

cpo 16263

cplt 16264

cjn 16267

clat 16369

ccvr 32899

catm 32900

chlt 32987

clpl 33128

clvol 33129

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-preset 16251 df-poset 16269 df-plt 16282 df-lub 16298 df-glb 16299 df-join 16300 df-meet 16301 df-p0 16363 df-lat 16370 df-clat 16432 df-oposet 32813 df-ol 32815 df-oml 32816 df-covers 32903 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988 df-llines 33134 df-lplanes 33135 df-lvols 33136

This theorem is referenced by: lvolnleat 33219 lvolnlelln 33220 lvolnlelpln 33221 3atnelvolN 33222 4atlem3 33232 dalem39 33347

W3C validator