Theorem dia2dimlem8

Description: Lemma for dia2dim . Eliminate no-longer used auxiliary atoms P and Q . (Contributed by NM, 8-Sep-2014)

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

Proof

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