Metamath Proof Explorer

Theorem islln2a

Description: The predicate "is a lattice line" in terms of atoms. (Contributed by NM, 15-Jul-2012)

		Ref	Expression
	Hypotheses	islln2a.j	$⊢ \underset{˙}{\lor} = join (K)$
		islln2a.a	$⊢ A = Atoms (K)$
		islln2a.n	$⊢ N = LLines (K)$
	Assertion	islln2a	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \underset{˙}{\lor} Q \in N \leftrightarrow P \neq Q)$

Proof

Step	Hyp	Ref	Expression
1		islln2a.j	$⊢ \underset{˙}{\lor} = join (K)$
2		islln2a.a	$⊢ A = Atoms (K)$
3		islln2a.n	$⊢ N = LLines (K)$
4		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
5	1 2	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
6	5	3adant2	$⊢ (K \in HL \land P \in A \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
7	4 6	sylan9eqr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P = Q) \to P \underset{˙}{\lor} Q = Q$
8	2 3	llnneat	$⊢ (K \in HL \land Q \in N) \to \neg Q \in A$
9	8	adantlr	$⊢ ((K \in HL \land P \in A) \land Q \in N) \to \neg Q \in A$
10	9	ex	$⊢ (K \in HL \land P \in A) \to (Q \in N \to \neg Q \in A)$
11	10	con2d	$⊢ (K \in HL \land P \in A) \to (Q \in A \to \neg Q \in N)$
12	11	3impia	$⊢ (K \in HL \land P \in A \land Q \in A) \to \neg Q \in N$
13	12	adantr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P = Q) \to \neg Q \in N$
14	7 13	eqneltrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P = Q) \to \neg P \underset{˙}{\lor} Q \in N$
15	14	ex	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P = Q \to \neg P \underset{˙}{\lor} Q \in N)$
16	15	necon2ad	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \underset{˙}{\lor} Q \in N \to P \neq Q)$
17	1 2 3	llni2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in N$
18	17	ex	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \to P \underset{˙}{\lor} Q \in N)$
19	16 18	impbid	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \underset{˙}{\lor} Q \in N \leftrightarrow P \neq Q)$