Theorem dalem3

Description: Lemma for dalemdnee . (Contributed by NM, 10-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)$$
	dalem3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dalem3.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
	dalem3.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
	dalem3.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
	dalem3.d	$$⊢D=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)$$
	dalem3.e	$$⊢E=\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)$$
Assertion	dalem3	$$⊢\left(\phi \wedge D\ne Q\right)\to D\ne E$$

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		dalem3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		dalem3.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
7		dalem3.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
8		dalem3.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
9		dalem3.d	$$⊢D=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)$$
10		dalem3.e	$$⊢E=\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)$$
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	2 3 4 6 7	lplnric	$$⊢\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 \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
17	11 12 13 14 15 16	syl131anc	$$⊢\phi \to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
18	17	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
19	1	dalemkelat	$$⊢\phi \to K\in \mathrm{Lat}$$
20		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
21	20 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge R\in A\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
22	11 13 14 21	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
23	1 3 4	dalemtjueb	$$⊢\phi \to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
24	20 2 5	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
25	19 22 23 24	syl3anc	$$⊢\phi \to \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
26	10 25	eqbrtrid	$$⊢\phi \to E\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
27		breq1	$$⊢D=E\to \left(D\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\leftrightarrow E\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
28	26 27	syl5ibrcom	$$⊢\phi \to \left(D=E\to D\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
29	28	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to \left(D=E\to D\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
30	11	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to K\in \mathrm{HL}$$
31	1 2 3 4 5 6 7 8 9	dalemdea	$$⊢\phi \to D\in A$$
32	31	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to D\in A$$
33	14	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to R\in A$$
34	13	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to Q\in A$$
35		simpr	$$⊢\left(\phi \wedge D\ne Q\right)\to D\ne Q$$
36	2 3 4	hlatexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(D\in A\wedge R\in A\wedge Q\in A\right)\wedge D\ne Q\right)\to \left(D\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\to R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\right)$$
37	30 32 33 34 35 36	syl131anc	$$⊢\left(\phi \wedge D\ne Q\right)\to \left(D\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\to R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\right)$$
38	2 3 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
39	11 12 13 38	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
40	1 3 4	dalempjqeb	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
41	1 3 4	dalemsjteb	$$⊢\phi \to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
42	20 2 5	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
43	19 40 41 42	syl3anc	$$⊢\phi \to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
44	9 43	eqbrtrid	$$⊢\phi \to D\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
45	1 4	dalemqeb	$$⊢\phi \to Q\in {\mathrm{Base}}_K$$
46	20 4	atbase	$$⊢D\in A\to D\in {\mathrm{Base}}_K$$
47	31 46	syl	$$⊢\phi \to D\in {\mathrm{Base}}_K$$
48	20 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(Q\in {\mathrm{Base}}_K\wedge D\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\right)\to \left(\left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge D\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
49	19 45 47 40 48	syl13anc	$$⊢\phi \to \left(\left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge D\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
50	39 44 49	mpbi2and	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
51	1 4	dalemreb	$$⊢\phi \to R\in {\mathrm{Base}}_K$$
52	20 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge D\in A\right)\to Q\underset{\dot{}}{\vee }D\in {\mathrm{Base}}_K$$
53	11 13 31 52	syl3anc	$$⊢\phi \to Q\underset{\dot{}}{\vee }D\in {\mathrm{Base}}_K$$
54	20 2	lattr	$$⊢\left(K\in \mathrm{Lat}\wedge \left(R\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }D\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\right)\to \left(\left(R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\wedge \left(Q\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
55	19 51 53 40 54	syl13anc	$$⊢\phi \to \left(\left(R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\wedge \left(Q\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
56	50 55	mpan2d	$$⊢\phi \to \left(R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
57	56	adantr	$$⊢\left(\phi \wedge D\ne Q\right)\to \left(R\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }D\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
58	29 37 57	3syld	$$⊢\left(\phi \wedge D\ne Q\right)\to \left(D=E\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
59	58	necon3bd	$$⊢\left(\phi \wedge D\ne Q\right)\to \left(\neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to D\ne E\right)$$
60	18 59	mpd	$$⊢\left(\phi \wedge D\ne Q\right)\to D\ne E$$