Theorem cdlemk18-3N

Description: Part of proof of Lemma K of Crawley p. 118. Line 22 on p. 119. N , Y , O , D are k, sigma_2 (p), k_1, f_1. (Contributed by NM, 7-Jul-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemk3.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemk3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemk3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemk3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemk3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemk3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemk3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemk3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemk3.s	$$⊢S=\left(f\in T⟼\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(f\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(f\circ F^{-1}\right)\right)\right)\right)$$
	cdlemk3.u1	$$⊢Y=\left(d\in T,e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\right)\right)$$
Assertion	cdlemk18-3N	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to \left(DYF\right)\left(P\right)=N\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk3.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemk3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemk3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemk3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdlemk3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdlemk3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdlemk3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8		cdlemk3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
9		cdlemk3.s	$$⊢S=\left(f\in T⟼\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(f\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(f\circ F^{-1}\right)\right)\right)\right)$$
10		cdlemk3.u1	$$⊢Y=\left(d\in T,e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\right)\right)$$
11		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to D\in T$$
12		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to F\in T$$
13		eqid	$$⊢S\left(D\right)=S\left(D\right)$$
14		eqid	$$⊢\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)$$
15	1 2 3 4 5 6 7 8 9 10 13 14	cdlemkuu	$$⊢\left(D\in T\wedge F\in T\right)\to DYF=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)\left(F\right)$$
16	11 12 15	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to DYF=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)\left(F\right)$$
17	16	fveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to \left(DYF\right)\left(P\right)=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)\left(F\right)\left(P\right)$$
18	1 2 3 4 5 6 7 8 9 13 14	cdlemk18-2N	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to N\left(P\right)=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(D\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)\left(F\right)\left(P\right)$$
19	17 18	eqtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\in T\wedge D\in T\wedge N\in T\right)\wedge \left(R\left(D\right)\ne R\left(F\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)\right)\to \left(DYF\right)\left(P\right)=N\left(P\right)$$