Theorem lplnri1

Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012)

	Ref	Expression
Hypotheses	lplnri1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lplnri1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lplnri1.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
	lplnri1.y	$$⊢Y=\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
Assertion	lplnri1	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge R\in A\wedge S\in A\right)\wedge Y\in P\right)\to Q\ne R$$

Proof

Step	Hyp	Ref	Expression
1		lplnri1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		lplnri1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		lplnri1.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
4		lplnri1.y	$$⊢Y=\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6	5 1 2 3 4	islpln2ah	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge R\in A\wedge S\in A\right)\right)\to \left(Y\in P\leftrightarrow \left(Q\ne R\wedge \neg S{\le }_K\left(Q\underset{\dot{}}{\vee }R\right)\right)\right)$$
7	6	biimp3a	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge R\in A\wedge S\in A\right)\wedge Y\in P\right)\to \left(Q\ne R\wedge \neg S{\le }_K\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
8	7	simpld	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge R\in A\wedge S\in A\right)\wedge Y\in P\right)\to Q\ne R$$