Theorem dia2dimlem11

Description: Lemma for dia2dim . Convert ordering hypothesis on RF to subspace membership F e. ( I( U .\/ V ) ) . (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem11.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dia2dimlem11.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dia2dimlem11.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dia2dimlem11.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dia2dimlem11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia2dimlem11.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dia2dimlem11.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dia2dimlem11.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dia2dimlem11.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
	dia2dimlem11.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
	dia2dimlem11.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
	dia2dimlem11.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dia2dimlem11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dia2dimlem11.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
	dia2dimlem11.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
	dia2dimlem11.f	$$⊢\phi \to F\in T$$
	dia2dimlem11.uv	$$⊢\phi \to U\ne V$$
	dia2dimlem11.fe	$$⊢\phi \to F\in I\left(U\underset{\dot{}}{\vee }V\right)$$
Assertion	dia2dimlem11	$$⊢\phi \to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem11.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dimlem11.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dimlem11.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dia2dimlem11.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dia2dimlem11.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		dia2dimlem11.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		dia2dimlem11.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		dia2dimlem11.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
9		dia2dimlem11.s	$$⊢S=\mathrm{LSubSp}\left(Y\right)$$
10		dia2dimlem11.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
11		dia2dimlem11.n	$$⊢N=\mathrm{LSpan}\left(Y\right)$$
12		dia2dimlem11.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
13		dia2dimlem11.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		dia2dimlem11.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
15		dia2dimlem11.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
16		dia2dimlem11.f	$$⊢\phi \to F\in T$$
17		dia2dimlem11.uv	$$⊢\phi \to U\ne V$$
18		dia2dimlem11.fe	$$⊢\phi \to F\in I\left(U\underset{\dot{}}{\vee }V\right)$$
19	1 2 4 5 6 7 8 9 11 12 13 14 15 16 18	dia2dimlem10	$$⊢\phi \to R\left(F\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }V\right)$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 17	dia2dimlem9	$$⊢\phi \to F\in \left(I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)\right)$$