Theorem cdlemk13

Description: Part of proof of Lemma K of Crawley p. 118. Line 13 on p. 119. O , D are k_1, f_1. (Contributed by NM, 1-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk1.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemk1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemk1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemk1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemk1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemk1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemk1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemk1.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemk1.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)$$
	cdlemk1.o	$$⊢O=S\left(D\right)$$
Assertion	cdlemk13	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge D\in T\right)\wedge \left(N\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(D\right)\ne R\left(F\right)\right)\right)\to O\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(D\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(D\circ F^{-1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk1.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemk1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemk1.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemk1.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdlemk1.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdlemk1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdlemk1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8		cdlemk1.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
9		cdlemk1.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		cdlemk1.o	$$⊢O=S\left(D\right)$$
11	10	fveq1i	$$⊢O\left(P\right)=S\left(D\right)\left(P\right)$$
12	1 2 3 5 6 7 8 4 9	cdlemksv2	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge D\in T\right)\wedge \left(N\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(D\right)\ne R\left(F\right)\right)\right)\to S\left(D\right)\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(D\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(D\circ F^{-1}\right)\right)$$
13	11 12	syl5eq	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge D\in T\right)\wedge \left(N\in T\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge R\left(F\right)=R\left(N\right)\right)\wedge \left(F\ne {\mathrm{I}\upharpoonright }_B\wedge D\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(D\right)\ne R\left(F\right)\right)\right)\to O\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(D\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(D\circ F^{-1}\right)\right)$$