Theorem dalemdea

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 11-Aug-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)$$
	dalemdea.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dalemdea.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
	dalemdea.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
	dalemdea.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
	dalemdea.d	$$⊢D=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)$$
Assertion	dalemdea	$$⊢\phi \to D\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		dalemdea.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		dalemdea.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
7		dalemdea.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
8		dalemdea.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
9		dalemdea.d	$$⊢D=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)$$
10	1 2 3 4 6 7	dalem2	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(S\underset{\dot{}}{\vee }T\right)\in O$$
11	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
12	1	dalempea	$$⊢\phi \to P\in A$$
13	1	dalemqea	$$⊢\phi \to Q\in A$$
14	1	dalemrea	$$⊢\phi \to R\in A$$
15	1	dalemyeo	$$⊢\phi \to Y\in O$$
16	3 4 6 7	lplnri1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge Y\in O\right)\to P\ne Q$$
17	11 12 13 14 15 16	syl131anc	$$⊢\phi \to P\ne Q$$
18		eqid	$$⊢\mathrm{LLines}\left(K\right)=\mathrm{LLines}\left(K\right)$$
19	3 4 18	llni2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge P\ne Q\right)\to P\underset{\dot{}}{\vee }Q\in \mathrm{LLines}\left(K\right)$$
20	11 12 13 17 19	syl31anc	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in \mathrm{LLines}\left(K\right)$$
21	1	dalemsea	$$⊢\phi \to S\in A$$
22	1	dalemtea	$$⊢\phi \to T\in A$$
23	1	dalemuea	$$⊢\phi \to U\in A$$
24	1	dalemzeo	$$⊢\phi \to Z\in O$$
25	3 4 6 8	lplnri1	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\wedge Z\in O\right)\to S\ne T$$
26	11 21 22 23 24 25	syl131anc	$$⊢\phi \to S\ne T$$
27	3 4 18	llni2	$$⊢\left(\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\wedge S\ne T\right)\to S\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)$$
28	11 21 22 26 27	syl31anc	$$⊢\phi \to S\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)$$
29	3 5 4 18 6	2llnmj	$$⊢\left(K\in \mathrm{HL}\wedge P\underset{\dot{}}{\vee }Q\in \mathrm{LLines}\left(K\right)\wedge S\underset{\dot{}}{\vee }T\in \mathrm{LLines}\left(K\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\in A\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(S\underset{\dot{}}{\vee }T\right)\in O\right)$$
30	11 20 28 29	syl3anc	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\in A\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }\left(S\underset{\dot{}}{\vee }T\right)\in O\right)$$
31	10 30	mpbird	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\in A$$
32	9 31	eqeltrid	$$⊢\phi \to D\in A$$