lnnat

Description: A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lnnat.j	$⊢ \underset{˙}{\lor} = join (K)$
2		lnnat.a	$⊢ A = Atoms (K)$
3		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to K \in HL$
4		simpl2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \in A$
5		eqid	$⊢ 0. (K) = 0. (K)$
6		eqid	$⊢ ⋖_{K} = ⋖_{K}$
7	5 6 2	atcvr0	$⊢ (K \in HL \land P \in A) \to 0. (K) ⋖_{K} P$
8	3 4 7	syl2anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to 0. (K) ⋖_{K} P$
9	1 6 2	atcvr1	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P ⋖_{K} (P \underset{˙}{\lor} Q))$
10	9	biimpa	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P ⋖_{K} (P \underset{˙}{\lor} Q)$
11		hlop	$⊢ K \in HL \to K \in OP$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 5	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
14	3 11 13	3syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to 0. (K) \in {Base}_{K}$
15	12 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
16	4 15	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \in {Base}_{K}$
17	3	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to K \in Lat$
18		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to Q \in A$
19	12 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to Q \in {Base}_{K}$
21	12 1	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
22	17 16 20 21	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
23	12 6	cvrntr	$⊢ (K \in HL \land (0. (K) \in {Base}_{K} \land P \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((0. (K) ⋖_{K} P \land P ⋖_{K} (P \underset{˙}{\lor} Q)) \to \neg 0. (K) ⋖_{K} (P \underset{˙}{\lor} Q))$
24	3 14 16 22 23	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to ((0. (K) ⋖_{K} P \land P ⋖_{K} (P \underset{˙}{\lor} Q)) \to \neg 0. (K) ⋖_{K} (P \underset{˙}{\lor} Q))$
25	8 10 24	mp2and	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to \neg 0. (K) ⋖_{K} (P \underset{˙}{\lor} Q)$
26		simpll1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \land P \underset{˙}{\lor} Q \in A) \to K \in HL$
27	5 6 2	atcvr0	$⊢ (K \in HL \land P \underset{˙}{\lor} Q \in A) \to 0. (K) ⋖_{K} (P \underset{˙}{\lor} Q)$
28	26 27	sylancom	$⊢ (((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \land P \underset{˙}{\lor} Q \in A) \to 0. (K) ⋖_{K} (P \underset{˙}{\lor} Q)$
29	25 28	mtand	$⊢ ((K \in HL \land P \in A \land Q \in A) \land P \neq Q) \to \neg P \underset{˙}{\lor} Q \in A$
30	29	ex	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \to \neg P \underset{˙}{\lor} Q \in A)$
31	1 2	hlatjidm	$⊢ (K \in HL \land P \in A) \to P \underset{˙}{\lor} P = P$
32	31	3adant3	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} P = P$
33		simp2	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \in A$
34	32 33	eqeltrd	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} P \in A$
35		oveq2	$⊢ P = Q \to P \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
36	35	eleq1d	$⊢ P = Q \to (P \underset{˙}{\lor} P \in A \leftrightarrow P \underset{˙}{\lor} Q \in A)$
37	34 36	syl5ibcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P = Q \to P \underset{˙}{\lor} Q \in A)$
38	37	necon3bd	$⊢ (K \in HL \land P \in A \land Q \in A) \to (\neg P \underset{˙}{\lor} Q \in A \to P \neq Q)$
39	30 38	impbid	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow \neg P \underset{˙}{\lor} Q \in A)$

Metamath Proof Explorer

Theorem lnnat

Proof