Theorem lplnexatN

Description: Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnexat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lplnexat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lplnexat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lplnexat.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
	lplnexat.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	lplnexatN	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge X=Y\underset{\dot{}}{\vee }q\right)$$

Proof

Step	Hyp	Ref	Expression
1		lplnexat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lplnexat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		lplnexat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lplnexat.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
5		lplnexat.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
6		simp1	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\to K\in \mathrm{HL}$$
7		simp3	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\to Y\in N$$
8		simp2	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\to X\in P$$
9	6 7 8	3jca	$$⊢\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\to \left(K\in \mathrm{HL}\wedge Y\in N\wedge X\in P\right)$$
10		eqid	$$⊢{⋖}_K={⋖}_K$$
11	1 10 4 5	llncvrlpln2	$$⊢\left(\left(K\in \mathrm{HL}\wedge Y\in N\wedge X\in P\right)\wedge Y\underset{\dot{}}{\le }X\right)\to Y{⋖}_{K}X$$
12	9 11	sylan	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to Y{⋖}_{K}X$$
13		simpl1	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to K\in \mathrm{HL}$$
14		simpl3	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to Y\in N$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16	15 4	llnbase	$$⊢Y\in N\to Y\in {\mathrm{Base}}_K$$
17	14 16	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to Y\in {\mathrm{Base}}_K$$
18		simpl2	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to X\in P$$
19	15 5	lplnbase	$$⊢X\in P\to X\in {\mathrm{Base}}_K$$
20	18 19	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to X\in {\mathrm{Base}}_K$$
21	15 1 2 10 3	cvrval3	$$⊢\left(K\in \mathrm{HL}\wedge Y\in {\mathrm{Base}}_K\wedge X\in {\mathrm{Base}}_K\right)\to \left(Y{⋖}_{K}X\leftrightarrow \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\vee }q=X\right)\right)$$
22	13 17 20 21	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to \left(Y{⋖}_{K}X\leftrightarrow \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\vee }q=X\right)\right)$$
23		eqcom	$$⊢Y\underset{\dot{}}{\vee }q=X\leftrightarrow X=Y\underset{\dot{}}{\vee }q$$
24	23	anbi2i	$$⊢\left(\neg q\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\vee }q=X\right)\leftrightarrow \left(\neg q\underset{\dot{}}{\le }Y\wedge X=Y\underset{\dot{}}{\vee }q\right)$$
25	24	rexbii	$$⊢\exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\vee }q=X\right)\leftrightarrow \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge X=Y\underset{\dot{}}{\vee }q\right)$$
26	22 25	bitrdi	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to \left(Y{⋖}_{K}X\leftrightarrow \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge X=Y\underset{\dot{}}{\vee }q\right)\right)$$
27	12 26	mpbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in P\wedge Y\in N\right)\wedge Y\underset{\dot{}}{\le }X\right)\to \exists q\in A\left(\neg q\underset{\dot{}}{\le }Y\wedge X=Y\underset{\dot{}}{\vee }q\right)$$