Metamath Proof Explorer

Theorem 2atmat0

Description: The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012)

		Ref	Expression
	Hypotheses	2atmatz.j	$⊢ \underset{˙}{\lor} = join (K)$
		2atmatz.m	$⊢ \underset{˙}{\land} = meet (K)$
		2atmatz.z	$⊢ \underset{˙}{0} = 0. (K)$
		2atmatz.a	$⊢ A = Atoms (K)$
	Assertion	2atmat0	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		2atmatz.j	$⊢ \underset{˙}{\lor} = join (K)$
2		2atmatz.m	$⊢ \underset{˙}{\land} = meet (K)$
3		2atmatz.z	$⊢ \underset{˙}{0} = 0. (K)$
4		2atmatz.a	$⊢ A = Atoms (K)$
5		simpl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (K \in HL \land P \in A \land Q \in A)$
6		simpr1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to R \in A$
7		simpr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to S \in A$
8	7	orcd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to (S \in A \lor S = \underset{˙}{0})$
9		simpr3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S$
10	1 2 3 4	2at0mat0	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land (S \in A \lor S = \underset{˙}{0}) \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$
11	5 6 8 9 10	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \underset{˙}{\lor} Q \neq R \underset{˙}{\lor} S)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) \in A \lor (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} S) = \underset{˙}{0})$