Theorem 2atjlej

Description: Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013)

	Ref	Expression
Hypotheses	ps1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ps1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	ps1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	2atjlej	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to R\ne S$$

Proof

Step	Hyp	Ref	Expression
1		ps1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ps1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		ps1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		simp33	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
5		simp1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to K\in \mathrm{HL}$$
6		simp21	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to P\in A$$
7		simp22	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to Q\in A$$
8		simp23	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to P\ne Q$$
9		simp31	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to R\in A$$
10		simp32	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to S\in A$$
11	1 2 3	ps-1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\leftrightarrow P\underset{\dot{}}{\vee }Q=R\underset{\dot{}}{\vee }S\right)$$
12	5 6 7 8 9 10 11	syl132anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\leftrightarrow P\underset{\dot{}}{\vee }Q=R\underset{\dot{}}{\vee }S\right)$$
13	4 12	mpbid	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=R\underset{\dot{}}{\vee }S$$
14	2 3	lnnat	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(P\ne Q\leftrightarrow \neg P\underset{\dot{}}{\vee }Q\in A\right)$$
15	5 6 7 14	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \left(P\ne Q\leftrightarrow \neg P\underset{\dot{}}{\vee }Q\in A\right)$$
16	8 15	mpbid	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \neg P\underset{\dot{}}{\vee }Q\in A$$
17	13 16	eqneltrrd	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \neg R\underset{\dot{}}{\vee }S\in A$$
18	2 3	lnnat	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to \left(R\ne S\leftrightarrow \neg R\underset{\dot{}}{\vee }S\in A\right)$$
19	5 9 10 18	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to \left(R\ne S\leftrightarrow \neg R\underset{\dot{}}{\vee }S\in A\right)$$
20	17 19	mpbird	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge S\in A\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\right)\to R\ne S$$