Theorem dalemswapyzps

Description: Lemma for dath . Swap the Y and Z planes, along with dummy concurrency (center of perspectivity) atoms c and d , to allow reuse of analogous proofs. (Contributed by NM, 17-Aug-2012)

	Ref	Expression
Hypotheses	dalem.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)$$
	dalem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dalem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dalem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dalem.ps	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
Assertion	dalemswapyzps	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(\left(d\in A\wedge c\in A\right)\wedge \neg d\underset{\dot{}}{\le }Z\wedge \left(c\ne d\wedge \neg c\underset{\dot{}}{\le }Z\wedge C\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }c\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dalem.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		dalem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dalem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dalem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dalem.ps	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
6	5	dalemddea	$$⊢\psi \to d\in A$$
7	5	dalemccea	$$⊢\psi \to c\in A$$
8	6 7	jca	$$⊢\psi \to \left(d\in A\wedge c\in A\right)$$
9	8	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(d\in A\wedge c\in A\right)$$
10	5	dalem-ddly	$$⊢\psi \to \neg d\underset{\dot{}}{\le }Y$$
11	10	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \neg d\underset{\dot{}}{\le }Y$$
12		simp2	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to Y=Z$$
13	12	breq2d	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(d\underset{\dot{}}{\le }Y\leftrightarrow d\underset{\dot{}}{\le }Z\right)$$
14	11 13	mtbid	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \neg d\underset{\dot{}}{\le }Z$$
15	5	dalemccnedd	$$⊢\psi \to c\ne d$$
16	15	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\ne d$$
17	5	dalem-ccly	$$⊢\psi \to \neg c\underset{\dot{}}{\le }Y$$
18	17	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \neg c\underset{\dot{}}{\le }Y$$
19	12	breq2d	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(c\underset{\dot{}}{\le }Y\leftrightarrow c\underset{\dot{}}{\le }Z\right)$$
20	18 19	mtbid	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \neg c\underset{\dot{}}{\le }Z$$
21	5	dalemclccjdd	$$⊢\psi \to C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)$$
22	21	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)$$
23	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
24	23	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to K\in \mathrm{HL}$$
25	7	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\in A$$
26	6	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\in A$$
27	3 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge c\in A\wedge d\in A\right)\to c\underset{\dot{}}{\vee }d=d\underset{\dot{}}{\vee }c$$
28	24 25 26 27	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\underset{\dot{}}{\vee }d=d\underset{\dot{}}{\vee }c$$
29	22 28	breqtrd	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }c\right)$$
30	16 20 29	3jca	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(c\ne d\wedge \neg c\underset{\dot{}}{\le }Z\wedge C\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }c\right)\right)$$
31	9 14 30	3jca	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(\left(d\in A\wedge c\in A\right)\wedge \neg d\underset{\dot{}}{\le }Z\wedge \left(c\ne d\wedge \neg c\underset{\dot{}}{\le }Z\wedge C\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }c\right)\right)\right)$$