Theorem cdleme31sde

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-Mar-2013)

	Ref	Expression
Hypotheses	cdleme31sde.c	$$⊢D=\left(t\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sde.e	$$⊢E=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sde.x	$$⊢Y=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sde.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme31sde	$$⊢\left(R\in A\wedge S\in A\right)\to ⦋R/s⦌⦋S/t⦌E=Z$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31sde.c	$$⊢D=\left(t\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
2		cdleme31sde.e	$$⊢E=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
3		cdleme31sde.x	$$⊢Y=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
4		cdleme31sde.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
5	2	csbeq2i	$$⊢⦋S/t⦌E=⦋S/t⦌\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
6		nfcvd	$$⊢S\in A\to \underset{\_}{Ⅎ}t\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
7		oveq1	$$⊢t=S\to t\underset{\dot{}}{\vee }U=S\underset{\dot{}}{\vee }U$$
8		oveq2	$$⊢t=S\to P\underset{\dot{}}{\vee }t=P\underset{\dot{}}{\vee }S$$
9	8	oveq1d	$$⊢t=S\to \left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
10	9	oveq2d	$$⊢t=S\to Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)=Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
11	7 10	oveq12d	$$⊢t=S\to \left(t\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
12	11 1 3	3eqtr4g	$$⊢t=S\to D=Y$$
13		oveq2	$$⊢t=S\to s\underset{\dot{}}{\vee }t=s\underset{\dot{}}{\vee }S$$
14	13	oveq1d	$$⊢t=S\to \left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W=\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
15	12 14	oveq12d	$$⊢t=S\to D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)=Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
16	15	oveq2d	$$⊢t=S\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
17	6 16	csbiegf	$$⊢S\in A\to ⦋S/t⦌\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
18	5 17	syl5eq	$$⊢S\in A\to ⦋S/t⦌E=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
19	18	csbeq2dv	$$⊢S\in A\to ⦋R/s⦌⦋S/t⦌E=⦋R/s⦌\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
20		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
21	20 4	cdleme31se	$$⊢R\in A\to ⦋R/s⦌\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)\right)=Z$$
22	19 21	sylan9eqr	$$⊢\left(R\in A\wedge S\in A\right)\to ⦋R/s⦌⦋S/t⦌E=Z$$