Theorem cdlemn11b

Description: Part of proof of Lemma N of Crawley p. 121 line 37. (Contributed by NM, 27-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn11a.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemn11a.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemn11a.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemn11a.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemn11a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemn11a.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
	cdlemn11a.o	$$⊢O=\left(h\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
	cdlemn11a.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemn11a.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemn11a.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	cdlemn11a.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
	cdlemn11a.J	$$⊢J=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
	cdlemn11a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	cdlemn11a.d	$$⊢\underset{\dot{}}{+}={+}_U$$
	cdlemn11a.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	cdlemn11a.f	$$⊢F=\left(\iota h\in T|h\left(P\right)=Q\right)$$
	cdlemn11a.g	$$⊢G=\left(\iota h\in T|h\left(P\right)=N\right)$$
Assertion	cdlemn11b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(N\in A\wedge \neg N\underset{\dot{}}{\le }W\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\wedge J\left(N\right)\subseteq J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)\to ⟨G,{\mathrm{I}\upharpoonright }_T⟩\in \left(J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemn11a.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemn11a.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemn11a.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemn11a.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdlemn11a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdlemn11a.p	$$⊢P=\mathrm{oc}\left(K\right)\left(W\right)$$
7		cdlemn11a.o	$$⊢O=\left(h\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
8		cdlemn11a.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
9		cdlemn11a.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
10		cdlemn11a.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
11		cdlemn11a.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
12		cdlemn11a.J	$$⊢J=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
13		cdlemn11a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
14		cdlemn11a.d	$$⊢\underset{\dot{}}{+}={+}_U$$
15		cdlemn11a.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
16		cdlemn11a.f	$$⊢F=\left(\iota h\in T|h\left(P\right)=Q\right)$$
17		cdlemn11a.g	$$⊢G=\left(\iota h\in T|h\left(P\right)=N\right)$$
18		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(N\in A\wedge \neg N\underset{\dot{}}{\le }W\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\wedge J\left(N\right)\subseteq J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)\to J\left(N\right)\subseteq J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	cdlemn11a	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(N\in A\wedge \neg N\underset{\dot{}}{\le }W\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\wedge J\left(N\right)\subseteq J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)\to ⟨G,{\mathrm{I}\upharpoonright }_T⟩\in J\left(N\right)$$
20	18 19	sseldd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(N\in A\wedge \neg N\underset{\dot{}}{\le }W\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\wedge J\left(N\right)\subseteq J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)\to ⟨G,{\mathrm{I}\upharpoonright }_T⟩\in \left(J\left(Q\right)\underset{\dot{}}{\oplus }I\left(X\right)\right)$$