Theorem lplnri2N

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	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	lplnri2N	$$⊢\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 S$$

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	lplnriaN	$$⊢\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 \neg Q{\le }_K\left(R\underset{\dot{}}{\vee }S\right)$$
7	5 1 2	atnlej2	$$⊢\left(K\in \mathrm{HL}\wedge \left(Q\in A\wedge R\in A\wedge S\in A\right)\wedge \neg Q{\le }_K\left(R\underset{\dot{}}{\vee }S\right)\right)\to Q\ne S$$
8	6 7	syld3an3	$$⊢\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 S$$