Theorem dalemcea

Description: Lemma for dath . Frequently-used utility lemma. Here we show that C must be an atom. This is an assumption in most presentations of Desargues's theorem; instead, we assume only the C is a lattice element, in order to make later substitutions for C easier. (Contributed by NM, 23-Sep-2012)

	Ref	Expression
Hypotheses	dalema.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
	dalemc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dalemc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dalemc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dalem1.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
	dalem1.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
Assertion	dalemcea	$$⊢\phi \to C\in A$$

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
2		dalemc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dalemc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dalemc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dalem1.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
6		dalem1.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
7	1	dalemkeop	$$⊢\phi \to K\in \mathrm{OP}$$
8	1 4	dalemceb	$$⊢\phi \to C\in {\mathrm{Base}}_K$$
9	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
10	1 2 3 4 5 6	dalempjsen	$$⊢\phi \to P\underset{\dot{}}{\vee }S\in \mathrm{LLines}\left(K\right)$$
11	1	dalemqea	$$⊢\phi \to Q\in A$$
12	1	dalemtea	$$⊢\phi \to T\in A$$
13	1 2 3 4 5 6	dalemqnet	$$⊢\phi \to Q\ne T$$
14		eqid	$$⊢\mathrm{LLines}\left(K\right)=\mathrm{LLines}\left(K\right)$$
15	3 4 14	llni2	$$⊢\left(\left(K\in \mathrm{HL}\wedge Q\in A\wedge T\in A\right)\wedge Q\ne T\right)\to Q\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)$$
16	9 11 12 13 15	syl31anc	$$⊢\phi \to Q\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)$$
17	1 2 3 4 5 6	dalem1	$$⊢\phi \to P\underset{\dot{}}{\vee }S\ne Q\underset{\dot{}}{\vee }T$$
18	1	dalem-clpjq	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
19	1 3 4	dalempjqeb	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
20		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
21		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
22	20 2 21	op0le	$$⊢\left(K\in \mathrm{OP}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\to \mathrm{0.}\left(K\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
23	7 19 22	syl2anc	$$⊢\phi \to \mathrm{0.}\left(K\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
24		breq1	$$⊢C=\mathrm{0.}\left(K\right)\to \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \mathrm{0.}\left(K\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
25	23 24	syl5ibrcom	$$⊢\phi \to \left(C=\mathrm{0.}\left(K\right)\to C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
26	25	necon3bd	$$⊢\phi \to \left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to C\ne \mathrm{0.}\left(K\right)\right)$$
27	18 26	mpd	$$⊢\phi \to C\ne \mathrm{0.}\left(K\right)$$
28		eqid	$$⊢{<}_K={<}_K$$
29	20 28 21	opltn0	$$⊢\left(K\in \mathrm{OP}\wedge C\in {\mathrm{Base}}_K\right)\to \left(\mathrm{0.}\left(K\right){<}_{K}C\leftrightarrow C\ne \mathrm{0.}\left(K\right)\right)$$
30	7 8 29	syl2anc	$$⊢\phi \to \left(\mathrm{0.}\left(K\right){<}_{K}C\leftrightarrow C\ne \mathrm{0.}\left(K\right)\right)$$
31	27 30	mpbird	$$⊢\phi \to \mathrm{0.}\left(K\right){<}_{K}C$$
32	1	dalemclpjs	$$⊢\phi \to C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)$$
33	1	dalemclqjt	$$⊢\phi \to C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)$$
34	1	dalemkelat	$$⊢\phi \to K\in \mathrm{Lat}$$
35	1	dalempea	$$⊢\phi \to P\in A$$
36	1	dalemsea	$$⊢\phi \to S\in A$$
37	20 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge S\in A\right)\to P\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
38	9 35 36 37	syl3anc	$$⊢\phi \to P\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
39	20 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge T\in A\right)\to Q\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
40	9 11 12 39	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
41		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
42	20 2 41	latlem12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\right)\to \left(\left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)$$
43	34 8 38 40 42	syl13anc	$$⊢\phi \to \left(\left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)$$
44	32 33 43	mpbi2and	$$⊢\phi \to C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)$$
45		opposet	$$⊢K\in \mathrm{OP}\to K\in \mathrm{Poset}$$
46	7 45	syl	$$⊢\phi \to K\in \mathrm{Poset}$$
47	20 21	op0cl	$$⊢K\in \mathrm{OP}\to \mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K$$
48	7 47	syl	$$⊢\phi \to \mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K$$
49	20 41	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in {\mathrm{Base}}_K$$
50	34 38 40 49	syl3anc	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in {\mathrm{Base}}_K$$
51	20 2 28	pltletr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(\mathrm{0.}\left(K\right)\in {\mathrm{Base}}_K\wedge C\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\mathrm{0.}\left(K\right){<}_{K}C\wedge C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)\to \mathrm{0.}\left(K\right){<}_K\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)$$
52	46 48 8 50 51	syl13anc	$$⊢\phi \to \left(\left(\mathrm{0.}\left(K\right){<}_{K}C\wedge C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)\to \mathrm{0.}\left(K\right){<}_K\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)$$
53	31 44 52	mp2and	$$⊢\phi \to \mathrm{0.}\left(K\right){<}_K\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)$$
54	20 28 21	opltn0	$$⊢\left(K\in \mathrm{OP}\wedge \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in {\mathrm{Base}}_K\right)\to \left(\mathrm{0.}\left(K\right){<}_K\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\ne \mathrm{0.}\left(K\right)\right)$$
55	7 50 54	syl2anc	$$⊢\phi \to \left(\mathrm{0.}\left(K\right){<}_K\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\ne \mathrm{0.}\left(K\right)\right)$$
56	53 55	mpbid	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\ne \mathrm{0.}\left(K\right)$$
57	41 21 4 14	2llnmat	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\underset{\dot{}}{\vee }S\in \mathrm{LLines}\left(K\right)\wedge Q\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)\right)\wedge \left(P\underset{\dot{}}{\vee }S\ne Q\underset{\dot{}}{\vee }T\wedge \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\ne \mathrm{0.}\left(K\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in A$$
58	9 10 16 17 56 57	syl32anc	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in A$$
59	20 2 21 4	leat2	$$⊢\left(\left(K\in \mathrm{OP}\wedge C\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\in A\right)\wedge \left(C\ne \mathrm{0.}\left(K\right)\wedge C\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)\right)\right)\right)\to C=\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)$$
60	7 8 58 27 44 59	syl32anc	$$⊢\phi \to C=\left(P\underset{\dot{}}{\vee }S\right)\mathrm{meet}\left(K\right)\left(Q\underset{\dot{}}{\vee }T\right)$$
61	60 58	eqeltrd	$$⊢\phi \to C\in A$$