Theorem islinei

Description: Condition implying "is a line". (Contributed by NM, 3-Feb-2012)

	Ref	Expression
Hypotheses	isline.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isline.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	isline.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	isline.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
Assertion	islinei	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to X\in N$$

Proof

Step	Hyp	Ref	Expression
1		isline.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		isline.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		isline.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		isline.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
5		simpl2	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to Q\in A$$
6		simpl3	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to R\in A$$
7		simpr	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)$$
8		neeq1	$$⊢q=Q\to \left(q\ne r\leftrightarrow Q\ne r\right)$$
9		oveq1	$$⊢q=Q\to q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r$$
10	9	breq2d	$$⊢q=Q\to \left(p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\leftrightarrow p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right)$$
11	10	rabbidv	$$⊢q=Q\to \left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}$$
12	11	eqeq2d	$$⊢q=Q\to \left(X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\leftrightarrow X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
13	8 12	anbi12d	$$⊢q=Q\to \left(\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\leftrightarrow \left(Q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
14		neeq2	$$⊢r=R\to \left(Q\ne r\leftrightarrow Q\ne R\right)$$
15		oveq2	$$⊢r=R\to Q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }R$$
16	15	breq2d	$$⊢r=R\to \left(p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\leftrightarrow p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
17	16	rabbidv	$$⊢r=R\to \left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}$$
18	17	eqeq2d	$$⊢r=R\to \left(X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}\leftrightarrow X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)$$
19	14 18	anbi12d	$$⊢r=R\to \left(\left(Q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }r\right)\right\}\right)\leftrightarrow \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)$$
20	13 19	rspc2ev	$$⊢\left(Q\in A\wedge R\in A\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
21	5 6 7 20	syl3anc	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
22		simpl1	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to K\in D$$
23	1 2 3 4	isline	$$⊢K\in D\to \left(X\in N\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
24	22 23	syl	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to \left(X\in N\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
25	21 24	mpbird	$$⊢\left(\left(K\in D\wedge Q\in A\wedge R\in A\right)\wedge \left(Q\ne R\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right\}\right)\right)\to X\in N$$