Theorem cdlemk19y

Description: cdlemk19 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk5.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemk5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemk5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemk5.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemk5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemk5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemk5.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemk5.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemk5.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }R\left(b\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(b\circ F^{-1}\right)\right)$$
	cdlemk5.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }R\left(g\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)\right)$$
Assertion	cdlemk19y	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge F\ne {\mathrm{I}\upharpoonright }_B\right)\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(b\in T\wedge \left(b\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(b\right)\ne R\left(F\right)\right)\right)\right)\to ⦋F/g⦌Y=N\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk5.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemk5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemk5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemk5.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdlemk5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdlemk5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdlemk5.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8		cdlemk5.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
9		cdlemk5.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }R\left(b\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(b\circ F^{-1}\right)\right)$$
10		cdlemk5.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }R\left(g\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)\right)$$
11		eqid	$$⊢\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)=\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)$$
12		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(\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)\left(b\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ b^{-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(\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)\left(b\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ b^{-1}\right)\right)\right)\right)$$
13	1 2 3 4 5 6 7 8 9 10 11 12	cdlemk19ylem	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(F\in T\wedge F\ne {\mathrm{I}\upharpoonright }_B\right)\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(b\in T\wedge \left(b\ne {\mathrm{I}\upharpoonright }_B\wedge R\left(b\right)\ne R\left(F\right)\right)\right)\right)\to ⦋F/g⦌Y=N\left(P\right)$$