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{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	2atmatz.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	2atmatz.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	2atmatz.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	2atmat0	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\wedge P\underset{\dot{}}{\vee }Q\ne R\underset{\dot{}}{\vee }S\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }S\right)\in A\vee \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }S\right)=\underset{\dot{}}{0}\right)$$

Proof

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