atcvrlln

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

	Ref	Expression
Hypotheses	atcvrlln.b	$⊢ B = {Base}_{K}$
	atcvrlln.c	$⊢ C = ⋖_{K}$
	atcvrlln.a	$⊢ A = Atoms (K)$
	atcvrlln.n	$⊢ N = LLines (K)$
Assertion	atcvrlln	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in A \leftrightarrow Y \in N)$

Proof

Step	Hyp	Ref	Expression
1		atcvrlln.b	$⊢ B = {Base}_{K}$
2		atcvrlln.c	$⊢ C = ⋖_{K}$
3		atcvrlln.a	$⊢ A = Atoms (K)$
4		atcvrlln.n	$⊢ N = LLines (K)$
5		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in A) \to K \in HL$
6		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in A) \to Y \in B$
7		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in A) \to X \in A$
8		simplr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land X \in A) \to X C Y$
9	1 2 3 4	llni	$⊢ ((K \in HL \land Y \in B \land X \in A) \land X C Y) \to Y \in N$
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 A) \to Y \in N$
11		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to Y \in N$
12		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to K \in HL$
13		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to Y \in B$
14		eqid	$⊢ join (K) = join (K)$
15	1 14 3 4	islln3	$⊢ (K \in HL \land Y \in B) \to (Y \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land Y = p join (K) q))$
16	12 13 15	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to (Y \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land Y = p join (K) q))$
17	11 16	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to \exists p \in A \exists q \in A (p \neq q \land Y = p join (K) q)$
18		simp1l1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to K \in HL$
19		simp1l2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to X \in B$
20		simp2l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to p \in A$
21		simp2r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to q \in A$
22		simp3l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to p \neq q$
23		simp1r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to X C Y$
24		simp3r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to Y = p join (K) q$
25	23 24	breqtrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to X C (p join (K) q)$
26	1 14 2 3	cvrat2	$⊢ (K \in HL \land (X \in B \land p \in A \land q \in A) \land (p \neq q \land X C (p join (K) q))) \to X \in A$
27	18 19 20 21 22 25 26	syl132anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land (p \in A \land q \in A) \land (p \neq q \land Y = p join (K) q)) \to X \in A$
28	27	3exp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to ((p \in A \land q \in A) \to ((p \neq q \land Y = p join (K) q) \to X \in A))$
29	28	rexlimdvv	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (\exists p \in A \exists q \in A (p \neq q \land Y = p join (K) q) \to X \in A)$
30	29	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to (\exists p \in A \exists q \in A (p \neq q \land Y = p join (K) q) \to X \in A)$
31	17 30	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land Y \in N) \to X \in A$
32	10 31	impbida	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \in A \leftrightarrow Y \in N)$

Metamath Proof Explorer

Theorem atcvrlln

Proof