llncvrlpln

Description: An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012)

	Ref	Expression
Hypotheses	llncvrlpln.b	$⊢ B = {Base}_{K}$
	llncvrlpln.c	$⊢ C = ⋖_{K}$
	llncvrlpln.n	$⊢ N = LLines (K)$
	llncvrlpln.p	$⊢ P = LPlanes (K)$
Assertion	llncvrlpln	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in N \leftrightarrow Y \in P)$

Proof

Step	Hyp	Ref	Expression
1		llncvrlpln.b	$⊢ B = {Base}_{K}$
2		llncvrlpln.c	$⊢ C = ⋖_{K}$
3		llncvrlpln.n	$⊢ N = LLines (K)$
4		llncvrlpln.p	$⊢ P = LPlanes (K)$
5		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in N) \to K \in HL$
6		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in N) \to Y \in B$
7		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in N) \to X \in N$
8		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in N) \to X C Y$
9	1 2 3 4	lplni	$⊢ ((K \in HL \land Y \in B \land X \in N) \land X C Y) \to Y \in P$
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 N) \to Y \in P$
11		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to K \in HL$
12		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to X \in B$
13		eqid	$⊢ Atoms (K) = Atoms (K)$
14	13 4	lplnneat	$⊢ (K \in HL \land Y \in P) \to \neg Y \in Atoms (K)$
15	11 14	sylancom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to \neg Y \in Atoms (K)$
16		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to X C Y$
17		breq1	$⊢ X = 0. (K) \to (X C Y \leftrightarrow 0. (K) C Y)$
18	16 17	syl5ibcom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (X = 0. (K) \to 0. (K) C Y)$
19		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to Y \in B$
20		eqid	$⊢ 0. (K) = 0. (K)$
21	1 20 2 13	isat2	$⊢ (K \in HL \land Y \in B) \to (Y \in Atoms (K) \leftrightarrow 0. (K) C Y)$
22	11 19 21	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (Y \in Atoms (K) \leftrightarrow 0. (K) C Y)$
23	18 22	sylibrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (X = 0. (K) \to Y \in Atoms (K))$
24	23	necon3bd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (\neg Y \in Atoms (K) \to X \neq 0. (K))$
25	15 24	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to X \neq 0. (K)$
26	3 4	lplnnelln	$⊢ (K \in HL \land Y \in P) \to \neg Y \in N$
27	11 26	sylancom	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to \neg Y \in N$
28	1 2 13 3	atcvrlln	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in Atoms (K) \leftrightarrow Y \in N)$
29	28	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (X \in Atoms (K) \leftrightarrow Y \in N)$
30	27 29	mtbird	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to \neg X \in Atoms (K)$
31		eqid	$⊢ \leq_{K} = \leq_{K}$
32	1 31 20 13 3	llnle	$⊢ ((K \in HL \land X \in B) \land (X \neq 0. (K) \land \neg X \in Atoms (K))) \to \exists z \in N z \leq_{K} X$
33	11 12 25 30 32	syl22anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to \exists z \in N z \leq_{K} X$
34		simpr3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z \leq_{K} X$
35		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to K \in HL$
36		hlop	$⊢ K \in HL \to K \in OP$
37	35 36	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to K \in OP$
38		simpr2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z \in N$
39	1 3	llnbase	$⊢ z \in N \to z \in B$
40	38 39	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z \in B$
41		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to X \in B$
42		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to Y \in B$
43		simpr1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to Y \in P$
44	1 31 2	cvrle	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to X \leq_{K} Y$
45	44	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to X \leq_{K} Y$
46		hlpos	$⊢ K \in HL \to K \in Poset$
47	35 46	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to K \in Poset$
48	1 31	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)$
49	47 40 41 42 48	syl13anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to ((z \leq_{K} X \land X \leq_{K} Y) \to z \leq_{K} Y)$
50	34 45 49	mp2and	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z \leq_{K} Y$
51	31 2 3 4	llncvrlpln2	$⊢ ((K \in HL \land z \in N \land Y \in P) \land z \leq_{K} Y) \to z C Y$
52	35 38 43 50 51	syl31anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z C Y$
53		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to X C Y$
54	1 31 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)$
55	37 40 41 42 52 53 54	syl132anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to (z \leq_{K} X \leftrightarrow z = X)$
56	34 55	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to z = X$
57	56 38	eqeltrrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (Y \in P \land z \in N \land z \leq_{K} X)) \to X \in N$
58	57	3exp2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (Y \in P \to (z \in N \to (z \leq_{K} X \to X \in N)))$
59	58	imp	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (z \in N \to (z \leq_{K} X \to X \in N))$
60	59	rexlimdv	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to (\exists z \in N z \leq_{K} X \to X \in N)$
61	33 60	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in P) \to X \in N$
62	10 61	impbida	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in N \leftrightarrow Y \in P)$

Metamath Proof Explorer

Theorem llncvrlpln

Proof