lplnri3N

Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnri1.j	$⊢ \underset{˙}{\lor} = join (K)$
	lplnri1.a	$⊢ A = Atoms (K)$
	lplnri1.p	$⊢ P = LPlanes (K)$
	lplnri1.y	$⊢ Y = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
Assertion	lplnri3N	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to R \neq S$

Step	Hyp	Ref	Expression
1		lplnri1.j	$⊢ \underset{˙}{\lor} = join (K)$
2		lplnri1.a	$⊢ A = Atoms (K)$
3		lplnri1.p	$⊢ P = LPlanes (K)$
4		lplnri1.y	$⊢ Y = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
5		simp1	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to K \in HL$
6		simp22	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to R \in A$
7		simp21	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to Q \in A$
8		simp23	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to S \in A$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	9 1 2 3 4	lplnribN	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to \neg R \leq_{K} (Q \underset{˙}{\lor} S)$
11	9 1 2	atnlej2	$⊢ (K \in HL \land (R \in A \land Q \in A \land S \in A) \land \neg R \leq_{K} (Q \underset{˙}{\lor} S)) \to R \neq S$
12	5 6 7 8 10 11	syl131anc	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to R \neq S$

Metamath Proof Explorer