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	|- .<_ = ( le ` K )
	dia2dimlem8.j	|- .\/ = ( join ` K )
	dia2dimlem8.m	|- ./\ = ( meet ` K )
	dia2dimlem8.a	|- A = ( Atoms ` K )
	dia2dimlem8.h	|- H = ( LHyp ` K )
	dia2dimlem8.t	|- T = ( ( LTrn ` K ) ` W )
	dia2dimlem8.r	|- R = ( ( trL ` K ) ` W )
	dia2dimlem8.y	|- Y = ( ( DVecA ` K ) ` W )
	dia2dimlem8.s	|- S = ( LSubSp ` Y )
	dia2dimlem8.pl	|- .(+) = ( LSSum ` Y )
	dia2dimlem8.n	|- N = ( LSpan ` Y )
	dia2dimlem8.i	|- I = ( ( DIsoA ` K ) ` W )
	dia2dimlem8.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dia2dimlem8.u	|- ( ph -> ( U e. A /\ U .<_ W ) )
	dia2dimlem8.v	|- ( ph -> ( V e. A /\ V .<_ W ) )
	dia2dimlem8.f	|- ( ph -> F e. T )
	dia2dimlem8.rf	|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
	dia2dimlem8.uv	|- ( ph -> U =/= V )
	dia2dimlem8.ru	|- ( ph -> ( R ` F ) =/= U )
	dia2dimlem8.rv	|- ( ph -> ( R ` F ) =/= V )
Assertion	dia2dimlem8	|- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem8.l	|- .<_ = ( le ` K )
2		dia2dimlem8.j	|- .\/ = ( join ` K )
3		dia2dimlem8.m	|- ./\ = ( meet ` K )
4		dia2dimlem8.a	|- A = ( Atoms ` K )
5		dia2dimlem8.h	|- H = ( LHyp ` K )
6		dia2dimlem8.t	|- T = ( ( LTrn ` K ) ` W )
7		dia2dimlem8.r	|- R = ( ( trL ` K ) ` W )
8		dia2dimlem8.y	|- Y = ( ( DVecA ` K ) ` W )
9		dia2dimlem8.s	|- S = ( LSubSp ` Y )
10		dia2dimlem8.pl	|- .(+) = ( LSSum ` Y )
11		dia2dimlem8.n	|- N = ( LSpan ` Y )
12		dia2dimlem8.i	|- I = ( ( DIsoA ` K ) ` W )
13		dia2dimlem8.k	|- ( ph -> ( K e. HL /\ W e. H ) )
14		dia2dimlem8.u	|- ( ph -> ( U e. A /\ U .<_ W ) )
15		dia2dimlem8.v	|- ( ph -> ( V e. A /\ V .<_ W ) )
16		dia2dimlem8.f	|- ( ph -> F e. T )
17		dia2dimlem8.rf	|- ( ph -> ( R ` F ) .<_ ( U .\/ V ) )
18		dia2dimlem8.uv	|- ( ph -> U =/= V )
19		dia2dimlem8.ru	|- ( ph -> ( R ` F ) =/= U )
20		dia2dimlem8.rv	|- ( ph -> ( R ` F ) =/= V )
21		eqid	|- ( ( ( ( oc ` K ) ` W ) .\/ U ) ./\ ( ( F ` ( ( oc ` K ) ` W ) ) .\/ V ) ) = ( ( ( ( oc ` K ) ` W ) .\/ U ) ./\ ( ( F ` ( ( oc ` K ) ` W ) ) .\/ V ) )
22		eqid	|- ( oc ` K ) = ( oc ` K )
23	1 22 4 5	lhpocnel	|- ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
24	13 23	syl	|- ( ph -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
25	1 2 3 4 5 6 7 8 9 10 11 12 21 13 14 15 24 16 17 18 19 20	dia2dimlem7	|- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) )