islln3

Description: The predicate "is a lattice line". (Contributed by NM, 17-Jun-2012)

	Ref	Expression
Hypotheses	islln3.b	$⊢ B = {Base}_{K}$
	islln3.j	$⊢ \underset{˙}{\lor} = join (K)$
	islln3.a	$⊢ A = Atoms (K)$
	islln3.n	$⊢ N = LLines (K)$
Assertion	islln3	$⊢ (K \in HL \land X \in B) \to (X \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$

Proof

Step	Hyp	Ref	Expression
1		islln3.b	$⊢ B = {Base}_{K}$
2		islln3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islln3.a	$⊢ A = Atoms (K)$
4		islln3.n	$⊢ N = LLines (K)$
5		eqid	$⊢ ⋖_{K} = ⋖_{K}$
6	1 5 3 4	islln4	$⊢ (K \in HL \land X \in B) \to (X \in N \leftrightarrow \exists p \in A p ⋖_{K} X)$
7		simpll	$⊢ ((K \in HL \land X \in B) \land p \in A) \to K \in HL$
8	1 3	atbase	$⊢ p \in A \to p \in B$
9	8	adantl	$⊢ ((K \in HL \land X \in B) \land p \in A) \to p \in B$
10		simplr	$⊢ ((K \in HL \land X \in B) \land p \in A) \to X \in B$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	1 11 2 5 3	cvrval3	$⊢ (K \in HL \land p \in B \land X \in B) \to (p ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \leq_{K} p \land p \underset{˙}{\lor} q = X))$
13	7 9 10 12	syl3anc	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (p ⋖_{K} X \leftrightarrow \exists q \in A (\neg q \leq_{K} p \land p \underset{˙}{\lor} q = X))$
14		hlatl	$⊢ K \in HL \to K \in AtLat$
15	14	ad3antrrr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to K \in AtLat$
16		simpr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to q \in A$
17		simplr	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to p \in A$
18	11 3	atncmp	$⊢ (K \in AtLat \land q \in A \land p \in A) \to (\neg q \leq_{K} p \leftrightarrow q \neq p)$
19	15 16 17 18	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)$
20		necom	$⊢ q \neq p \leftrightarrow p \neq q$
21	19 20	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)$
22		eqcom	$⊢ p \underset{˙}{\lor} q = X \leftrightarrow X = p \underset{˙}{\lor} q$
23	22	a1i	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to (p \underset{˙}{\lor} q = X \leftrightarrow X = p \underset{˙}{\lor} q)$
24	21 23	anbi12d	$⊢ (((K \in HL \land X \in B) \land p \in A) \land q \in A) \to ((\neg q \leq_{K} p \land p \underset{˙}{\lor} q = X) \leftrightarrow (p \neq q \land X = p \underset{˙}{\lor} q))$
25	24	rexbidva	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (\exists q \in A (\neg q \leq_{K} p \land p \underset{˙}{\lor} q = X) \leftrightarrow \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$
26	13 25	bitrd	$⊢ ((K \in HL \land X \in B) \land p \in A) \to (p ⋖_{K} X \leftrightarrow \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$
27	26	rexbidva	$⊢ (K \in HL \land X \in B) \to (\exists p \in A p ⋖_{K} X \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$
28	6 27	bitrd	$⊢ (K \in HL \land X \in B) \to (X \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$

Metamath Proof Explorer

Theorem islln3

Proof