This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lplnllnneN

Description: Two lattice lines defined by atoms defining a lattice plane are not equal. (Contributed by NM, 9-Oct-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	lplnllnneN	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to Q \underset{˙}{\lor} S \neq R \underset{˙}{\lor} S$

Proof

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		eqid	$⊢ \leq_{K} = \leq_{K}$
6	5 1 2 3 4	lplnriaN	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to \neg Q \leq_{K} (R \underset{˙}{\lor} S)$
7		simpl1	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to K \in HL$
8		simpl21	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to Q \in A$
9		simpl23	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to S \in A$
10	5 1 2	hlatlej1	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \leq_{K} (Q \underset{˙}{\lor} S)$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to Q \leq_{K} (Q \underset{˙}{\lor} S)$
12		simpr	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S$
13	11 12	breqtrd	$⊢ ((K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \land Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S) \to Q \leq_{K} (R \underset{˙}{\lor} S)$
14	13	ex	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to (Q \underset{˙}{\lor} S = R \underset{˙}{\lor} S \to Q \leq_{K} (R \underset{˙}{\lor} S))$
15	14	necon3bd	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to (\neg Q \leq_{K} (R \underset{˙}{\lor} S) \to Q \underset{˙}{\lor} S \neq R \underset{˙}{\lor} S)$
16	6 15	mpd	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to Q \underset{˙}{\lor} S \neq R \underset{˙}{\lor} S$