atcvrneN

Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atcvrne.j	$⊢ \underset{˙}{\lor} = join (K)$
	atcvrne.c	$⊢ C = ⋖_{K}$
	atcvrne.a	$⊢ A = Atoms (K)$
Assertion	atcvrneN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to Q \neq R$

Proof

Step	Hyp	Ref	Expression
1		atcvrne.j	$⊢ \underset{˙}{\lor} = join (K)$
2		atcvrne.c	$⊢ C = ⋖_{K}$
3		atcvrne.a	$⊢ A = Atoms (K)$
4		hlatl	$⊢ K \in HL \to K \in AtLat$
5	4	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to K \in AtLat$
6		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to P \in A$
7		eqid	$⊢ 0. (K) = 0. (K)$
8	7 3	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq 0. (K)$
9	5 6 8	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to P \neq 0. (K)$
10		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to K \in HL$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	6 12	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to P \in {Base}_{K}$
14		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to Q \in A$
15		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to R \in A$
16		simp3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to P C (Q \underset{˙}{\lor} R)$
17	11 1 7 2 3	atcvrj0	$⊢ (K \in HL \land (P \in {Base}_{K} \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to (P = 0. (K) \leftrightarrow Q = R)$
18	10 13 14 15 16 17	syl131anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to (P = 0. (K) \leftrightarrow Q = R)$
19	18	necon3bid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to (P \neq 0. (K) \leftrightarrow Q \neq R)$
20	9 19	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P C (Q \underset{˙}{\lor} R)) \to Q \neq R$

Metamath Proof Explorer

Theorem atcvrneN

Proof