Theorem dalemrot

Description: Lemma for dath . Rotate triangles Y = P Q R and Z = S T U to allow reuse of analogous proofs. (Contributed by NM, 14-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)$$
	dalemrot.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
	dalemrot.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
Assertion	dalemrot	$$⊢\phi \to \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(Q\in A\wedge R\in A\wedge P\in A\right)\wedge \left(T\in A\wedge U\in A\wedge S\in A\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }P\in O\wedge \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S\in O\right)\wedge \left(\left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\wedge C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)\right)\right)$$

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		dalemrot.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
6		dalemrot.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
7	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
8	1 4	dalemceb	$$⊢\phi \to C\in {\mathrm{Base}}_K$$
9	7 8	jca	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)$$
10	1	dalemqea	$$⊢\phi \to Q\in A$$
11	1	dalemrea	$$⊢\phi \to R\in A$$
12	1	dalempea	$$⊢\phi \to P\in A$$
13	10 11 12	3jca	$$⊢\phi \to \left(Q\in A\wedge R\in A\wedge P\in A\right)$$
14	1	dalemtea	$$⊢\phi \to T\in A$$
15	1	dalemuea	$$⊢\phi \to U\in A$$
16	1	dalemsea	$$⊢\phi \to S\in A$$
17	14 15 16	3jca	$$⊢\phi \to \left(T\in A\wedge U\in A\wedge S\in A\right)$$
18	9 13 17	3jca	$$⊢\phi \to \left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(Q\in A\wedge R\in A\wedge P\in A\right)\wedge \left(T\in A\wedge U\in A\wedge S\in A\right)\right)$$
19	1 3 4	dalemqrprot	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }P=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
20	1	dalemyeo	$$⊢\phi \to Y\in O$$
21	5 20	eqeltrrid	$$⊢\phi \to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in O$$
22	19 21	eqeltrd	$$⊢\phi \to \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }P\in O$$
23	3 4	hlatjrot	$$⊢\left(K\in \mathrm{HL}\wedge \left(T\in A\wedge U\in A\wedge S\in A\right)\right)\to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
24	7 14 15 16 23	syl13anc	$$⊢\phi \to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
25	1	dalemzeo	$$⊢\phi \to Z\in O$$
26	6 25	eqeltrrid	$$⊢\phi \to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O$$
27	24 26	eqeltrd	$$⊢\phi \to \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S\in O$$
28	22 27	jca	$$⊢\phi \to \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }P\in O\wedge \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S\in O\right)$$
29		simp312	$$⊢\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)\to \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
30	1 29	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
31		simp313	$$⊢\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)\to \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)$$
32	1 31	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)$$
33	1	dalem-clpjq	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
34	30 32 33	3jca	$$⊢\phi \to \left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
35		simp322	$$⊢\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)\to \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)$$
36	1 35	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)$$
37		simp323	$$⊢\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)\to \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)$$
38	1 37	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)$$
39		simp321	$$⊢\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)\to \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
40	1 39	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
41	36 38 40	3jca	$$⊢\phi \to \left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
42	1	dalemclqjt	$$⊢\phi \to C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)$$
43	1	dalemclrju	$$⊢\phi \to C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)$$
44	1	dalemclpjs	$$⊢\phi \to C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)$$
45	42 43 44	3jca	$$⊢\phi \to \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\wedge C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)$$
46	34 41 45	3jca	$$⊢\phi \to \left(\left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\wedge C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)\right)$$
47	18 28 46	3jca	$$⊢\phi \to \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(Q\in A\wedge R\in A\wedge P\in A\right)\wedge \left(T\in A\wedge U\in A\wedge S\in A\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }P\in O\wedge \left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }S\in O\right)\wedge \left(\left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\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)\wedge \neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\wedge C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)\right)\right)$$