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 35719

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 753	. . . 4 $/\$ $/\$ $/\$ $/\$
2		eqid 2382	. . . . . 6
3		eqid 2382	. . . . . 6
4		eqid 2382	. . . . . 6
5		lvolnle3at.v	. . . . . 6
6	2, 3, 4, 5	islvol 35710	. . . . 5 $/\$
7	6	ad2antrr 723	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
8	1, 7	mpbid 210	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
9	8	simprd 461	. 2 $/\$ $/\$ $/\$ $/\$
10		oveq1 6203	. . . . . . . . 9 $.\/$ $.\/$
11	10	oveq1d 6211	. . . . . . . 8 $.\/$ $.\/$ $.\/$ $.\/$
12	11	breq2d 4379	. . . . . . 7 $.\/$ $.\/$ $.\/$ $.\/$
13	12	notbid 292	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
14		simp1l 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simp3l 1022	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		simp21 1027	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17		simp22 1028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		lvolnle3at.l	. . . . . . . . . . . . 13
19		lvolnle3at.j	. . . . . . . . . . . . 13 $.\/$
20		lvolnle3at.a	. . . . . . . . . . . . 13
21	18, 19, 20, 4	lplnnle2at 35678	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$
22	14, 15, 16, 17, 21	syl13anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	2, 4	lplnbase 35671	. . . . . . . . . . . . . . 15
24	15, 23	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		simp1r 1019	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	2, 5	lvolbase 35715	. . . . . . . . . . . . . . 15
27	25, 26	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		simp3r 1023	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		eqid 2382	. . . . . . . . . . . . . . 15
30	2, 29, 3	cvrlt 35408	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
31	14, 24, 27, 28, 30	syl31anc 1229	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		hlpos 35503	. . . . . . . . . . . . . . 15
33	14, 32	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	2, 19, 20	hlatjcl 35504	. . . . . . . . . . . . . . 15 $/\$ $/\$ $.\/$
35	14, 16, 17, 34	syl3anc 1226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	2, 18, 29	pltletr 15718	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	33, 24, 27, 35, 36	syl13anc 1228	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
38	31, 37	mpand 673	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
39	18, 29	pltle 15708	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	14, 15, 35, 39	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
41	38, 40	syld 44	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
42	22, 41	mtod 177	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
43	42	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44		simprr 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
45		hllat 35501	. . . . . . . . . . . . . 14
46	14, 45	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47		simp23 1029	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	2, 20	atbase 35427	. . . . . . . . . . . . . 14
49	47, 48	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	2, 18, 19	latleeqj2 15811	. . . . . . . . . . . . 13 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	46, 49, 35, 50	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
52	51	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
53	44, 52	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
54	53	breq2d 4379	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
55	43, 54	mtbird 299	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
56	55	anassrs 646	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
57		simpl1l 1045	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
58		simpl3l 1049	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
59		simpl2 998	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
60		simpr 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
61	18, 19, 20, 4	lplni2 35674	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
62	57, 59, 60, 61	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
63	29, 4	lplnnlt 35702	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
64	57, 58, 62, 63	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
65	2, 19	latjcl 15798	. . . . . . . . . . . . 13 $/\$ $.\/$ $/\$ $.\/$ $.\/$
66	46, 35, 49, 65	syl3anc 1226	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	2, 18, 29	pltletr 15718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
68	33, 24, 27, 66, 67	syl13anc 1228	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	31, 68	mpand 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
70	69	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	64, 70	mtod 177	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
72	71	anassrs 646	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
73	56, 72	pm2.61dan 789	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
74		eqid 2382	. . . . . . . . . 10
75	74, 19, 20, 4	lplnnle2at 35678	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$
76	14, 15, 17, 47, 75	syl13anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
77	2, 19, 20	hlatjcl 35504	. . . . . . . . . . . 12 $/\$ $/\$ $.\/$
78	14, 17, 47, 77	syl3anc 1226	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
79	2, 18, 29	pltletr 15718	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80	33, 24, 27, 78, 79	syl13anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	31, 80	mpand 673	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
82	74, 29	pltle 15708	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $.\/$ $.\/$
83	14, 15, 78, 82	syl3anc 1226	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
84	81, 83	syld 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
85	76, 84	mtod 177	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
86	19, 20	hlatjidm 35506	. . . . . . . . . 10 $/\$ $.\/$
87	14, 17, 86	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
88	87	oveq1d 6211	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
89	88	breq2d 4379	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
90	85, 89	mtbird 299	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
91	13, 73, 90	pm2.61ne 2697	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
92	91	3expia 1196	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
93	92	expd 434	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
94	93	rexlimdv 2872	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
95	9, 94	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wne 2577

wrex 2733 class class class wbr 4367

cfv 5496 (class class class)co 6196

cbs 14634

cple 14709

cpo 15686

cplt 15687

cjn 15690

clat 15792

ccvr 35400

catm 35401

chlt 35488

clpl 35629

clvol 35630

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-id 4709 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-preset 15674 df-poset 15692 df-plt 15705 df-lub 15721 df-glb 15722 df-join 15723 df-meet 15724 df-p0 15786 df-lat 15793 df-clat 15855 df-oposet 35314 df-ol 35316 df-oml 35317 df-covers 35404 df-ats 35405 df-atl 35436 df-cvlat 35460 df-hlat 35489 df-llines 35635 df-lplanes 35636 df-lvols 35637

This theorem is referenced by: lvolnleat 35720 lvolnlelln 35721 lvolnlelpln 35722 3atnelvolN 35723 4atlem3 35733 dalem39 35848

W3C validator