lplncvrlvol

Description: An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012)

	Ref	Expression
Hypotheses	lplncvrlvol.b	$⊢ B = {Base}_{K}$
	lplncvrlvol.c	$⊢ C = ⋖_{K}$
	lplncvrlvol.p	$⊢ P = LPlanes (K)$
	lplncvrlvol.v	$⊢ V = LVols (K)$
Assertion	lplncvrlvol	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in P \leftrightarrow Y \in V)$

Proof

Step	Hyp	Ref	Expression
1		lplncvrlvol.b	$⊢ B = {Base}_{K}$
2		lplncvrlvol.c	$⊢ C = ⋖_{K}$
3		lplncvrlvol.p	$⊢ P = LPlanes (K)$
4		lplncvrlvol.v	$⊢ V = LVols (K)$
5		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in P) \to K \in HL$
6		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in P) \to Y \in B$
7		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in P) \to X \in P$
8		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in P) \to X C Y$
9	1 2 3 4	lvoli	$⊢ ((K \in HL \land Y \in B \land X \in P) \land X C Y) \to Y \in V$
10	5 6 7 8 9	syl31anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in P) \to Y \in V$
11		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to K \in HL$
12		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to X \in B$
13	11	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to K \in Lat$
14		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to Y \in B$
15		eqid	$⊢ \leq_{K} = \leq_{K}$
16	1 15	latref	$⊢ (K \in Lat \land Y \in B) \to Y \leq_{K} Y$
17	13 14 16	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to Y \leq_{K} Y$
18	11	adantr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land Y \in Atoms (K)) \to K \in HL$
19		simplr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land Y \in Atoms (K)) \to Y \in V$
20		simpr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land Y \in Atoms (K)) \to Y \in Atoms (K)$
21		eqid	$⊢ Atoms (K) = Atoms (K)$
22	15 21 4	lvolnleat	$⊢ (K \in HL \land Y \in V \land Y \in Atoms (K)) \to \neg Y \leq_{K} Y$
23	18 19 20 22	syl3anc	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land Y \in Atoms (K)) \to \neg Y \leq_{K} Y$
24	23	ex	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (Y \in Atoms (K) \to \neg Y \leq_{K} Y)$
25	17 24	mt2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \neg Y \in Atoms (K)$
26		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to X C Y$
27		breq1	$⊢ X = 0. (K) \to (X C Y \leftrightarrow 0. (K) C Y)$
28	26 27	syl5ibcom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (X = 0. (K) \to 0. (K) C Y)$
29		eqid	$⊢ 0. (K) = 0. (K)$
30	1 29 2 21	isat2	$⊢ (K \in HL \land Y \in B) \to (Y \in Atoms (K) \leftrightarrow 0. (K) C Y)$
31	11 14 30	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (Y \in Atoms (K) \leftrightarrow 0. (K) C Y)$
32	28 31	sylibrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (X = 0. (K) \to Y \in Atoms (K))$
33	32	necon3bd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (\neg Y \in Atoms (K) \to X \neq 0. (K))$
34	25 33	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to X \neq 0. (K)$
35		eqid	$⊢ LLines (K) = LLines (K)$
36	35 4	lvolnelln	$⊢ (K \in HL \land Y \in V) \to \neg Y \in LLines (K)$
37	11 36	sylancom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \neg Y \in LLines (K)$
38	11	adantr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land X \in Atoms (K)) \to K \in HL$
39	14	adantr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land X \in Atoms (K)) \to Y \in B$
40		simpr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land X \in Atoms (K)) \to X \in Atoms (K)$
41		simpllr	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land X \in Atoms (K)) \to X C Y$
42	1 2 21 35	llni	$⊢ ((K \in HL \land Y \in B \land X \in Atoms (K)) \land X C Y) \to Y \in LLines (K)$
43	38 39 40 41 42	syl31anc	$⊢ ((((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \land X \in Atoms (K)) \to Y \in LLines (K)$
44	37 43	mtand	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \neg X \in Atoms (K)$
45	3 4	lvolnelpln	$⊢ (K \in HL \land Y \in V) \to \neg Y \in P$
46	11 45	sylancom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \neg Y \in P$
47	1 2 35 3	llncvrlpln	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in LLines (K) \leftrightarrow Y \in P)$
48	47	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (X \in LLines (K) \leftrightarrow Y \in P)$
49	46 48	mtbird	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \neg X \in LLines (K)$
50	1 15 29 21 35 3	lplnle	$⊢ ((K \in HL \land X \in B) \land (X \neq 0. (K) \land \neg X \in Atoms (K) \land \neg X \in LLines (K))) \to \exists z \in P z \leq_{K} X$
51	11 12 34 44 49 50	syl23anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to \exists z \in P z \leq_{K} X$
52		simpr3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z \leq_{K} X$
53		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to K \in HL$
54		hlop	$⊢ K \in HL \to K \in OP$
55	53 54	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to K \in OP$
56		simpr2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z \in P$
57	1 3	lplnbase	$⊢ z \in P \to z \in B$
58	56 57	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z \in B$
59		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to X \in B$
60		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to Y \in B$
61		simpr1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to Y \in V$
62	1 15 2	cvrle	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to X \leq_{K} Y$
63	62	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to X \leq_{K} Y$
64		hlpos	$⊢ K \in HL \to K \in Poset$
65	53 64	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to K \in Poset$
66	1 15	postr	$⊢ (K \in Poset \land (z \in B \land X \in B \land Y \in B)) \to ((z \leq_{K} X \land X \leq_{K} Y) \to z \leq_{K} Y)$
67	65 58 59 60 66	syl13anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to ((z \leq_{K} X \land X \leq_{K} Y) \to z \leq_{K} Y)$
68	52 63 67	mp2and	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z \leq_{K} Y$
69	15 2 3 4	lplncvrlvol2	$⊢ ((K \in HL \land z \in P \land Y \in V) \land z \leq_{K} Y) \to z C Y$
70	53 56 61 68 69	syl31anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z C Y$
71		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to X C Y$
72	1 15 2	cvrcmp2	$⊢ (K \in OP \land (z \in B \land X \in B \land Y \in B) \land (z C Y \land X C Y)) \to (z \leq_{K} X \leftrightarrow z = X)$
73	55 58 59 60 70 71 72	syl132anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to (z \leq_{K} X \leftrightarrow z = X)$
74	52 73	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to z = X$
75	74 56	eqeltrrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in V \land z \in P \land z \leq_{K} X)) \to X \in P$
76	75	3exp2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (Y \in V \to (z \in P \to (z \leq_{K} X \to X \in P)))$
77	76	imp	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (z \in P \to (z \leq_{K} X \to X \in P))$
78	77	rexlimdv	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to (\exists z \in P z \leq_{K} X \to X \in P)$
79	51 78	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in V) \to X \in P$
80	10 79	impbida	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in P \leftrightarrow Y \in V)$

Metamath Proof Explorer

Theorem lplncvrlvol

Proof