Metamath Proof Explorer

Theorem lplnribN

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	islpln2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		islpln2a.j	$⊢ \underset{˙}{\lor} = join (K)$
		islpln2a.a	$⊢ A = Atoms (K)$
		islpln2a.p	$⊢ P = LPlanes (K)$
		islpln2a.y	$⊢ Y = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
	Assertion	lplnribN	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to \neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$

Proof

Step	Hyp	Ref	Expression
1		islpln2a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		islpln2a.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islpln2a.a	$⊢ A = Atoms (K)$
4		islpln2a.p	$⊢ P = LPlanes (K)$
5		islpln2a.y	$⊢ Y = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
6	1 2 3	3noncolr1N	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (S \neq Q \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} Q))$
7	6	simprd	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} Q)$
8	7	3expia	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to ((Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} Q))$
9	1 2 3 4 5	islpln2ah	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (Y \in P \leftrightarrow (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
10	2 3	hlatjcom	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \underset{˙}{\lor} S = S \underset{˙}{\lor} Q$
11	10	3adant3r2	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to Q \underset{˙}{\lor} S = S \underset{˙}{\lor} Q$
12	11	breq2d	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (R \underset{˙}{\leq} (Q \underset{˙}{\lor} S) \leftrightarrow R \underset{˙}{\leq} (S \underset{˙}{\lor} Q))$
13	12	notbid	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (\neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} S) \leftrightarrow \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} Q))$
14	8 9 13	3imtr4d	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (Y \in P \to \neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} S))$
15	14	3impia	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land Y \in P) \to \neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$