isline4N

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isline4.b	$⊢ B = {Base}_{K}$
	isline4.c	$⊢ C = ⋖_{K}$
	isline4.a	$⊢ A = Atoms (K)$
	isline4.n	$⊢ N = Lines (K)$
	isline4.m	$⊢ M = pmap (K)$
Assertion	isline4N	$⊢ (K \in HL \land X \in B) \to (M (X) \in N \leftrightarrow \exists p \in A p C X)$

Proof

Step	Hyp	Ref	Expression
1		isline4.b	$⊢ B = {Base}_{K}$
2		isline4.c	$⊢ C = ⋖_{K}$
3		isline4.a	$⊢ A = Atoms (K)$
4		isline4.n	$⊢ N = Lines (K)$
5		isline4.m	$⊢ M = pmap (K)$
6		eqid	$⊢ join (K) = join (K)$
7	1 6 3 4 5	isline3	$⊢ (K \in HL \land X \in B) \to (M (X) \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p join (K) q))$
8		simpll	$⊢ ((K \in HL \land X \in B) \land p \in A) \to K \in HL$
9	1 3	atbase	$⊢ p \in A \to p \in B$
10	9	adantl	$⊢ ((K \in HL \land X \in B) \land p \in A) \to p \in B$
11		simplr	$⊢ ((K \in HL \land X \in B) \land p \in A) \to X \in B$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13	1 12 6 2 3	cvrval3	$⊢ (K \in HL \land p \in B \land X \in B) \to (p C X \leftrightarrow \exists q \in A (\neg q \leq_{K} p \land p join (K) q = X))$
14	8 10 11 13	syl3anc	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (p C X \leftrightarrow \exists q \in A (\neg q \leq_{K} p \land p join (K) q = X))$
15		hlatl	$⊢ K \in HL \to K \in AtLat$
16	15	ad3antrrr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to K \in AtLat$
17		simpr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to q \in A$
18		simplr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to p \in A$
19	12 3	atncmp	$⊢ (K \in AtLat \land q \in A \land p \in A) \to (\neg q \leq_{K} p \leftrightarrow q \neq p)$
20	16 17 18 19	syl3anc	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to (\neg q \leq_{K} p \leftrightarrow q \neq p)$
21		necom	$⊢ q \neq p \leftrightarrow p \neq q$
22	20 21	bitrdi	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to (\neg q \leq_{K} p \leftrightarrow p \neq q)$
23		eqcom	$⊢ p join (K) q = X \leftrightarrow X = p join (K) q$
24	23	a1i	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to (p join (K) q = X \leftrightarrow X = p join (K) q)$
25	22 24	anbi12d	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to ((\neg q \leq_{K} p \land p join (K) q = X) \leftrightarrow (p \neq q \land X = p join (K) q))$
26	25	rexbidva	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (\exists q \in A (\neg q \leq_{K} p \land p join (K) q = X) \leftrightarrow \exists q \in A (p \neq q \land X = p join (K) q))$
27	14 26	bitrd	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (p C X \leftrightarrow \exists q \in A (p \neq q \land X = p join (K) q))$
28	27	rexbidva	$⊢ (K \in HL \land X \in B) \to (\exists p \in A p C X \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p join (K) q))$
29	7 28	bitr4d	$⊢ (K \in HL \land X \in B) \to (M (X) \in N \leftrightarrow \exists p \in A p C X)$

Metamath Proof Explorer

Theorem isline4N

Proof