Theorem dihlss

Description: The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014)

	Ref	Expression
Hypotheses	dihlss.b	|- B = ( Base ` K )
	dihlss.h	|- H = ( LHyp ` K )
	dihlss.i	|- I = ( ( DIsoH ` K ) ` W )
	dihlss.u	|- U = ( ( DVecH ` K ) ` W )
	dihlss.s	|- S = ( LSubSp ` U )
Assertion	dihlss	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. S )

Proof

Step	Hyp	Ref	Expression
1		dihlss.b	|- B = ( Base ` K )
2		dihlss.h	|- H = ( LHyp ` K )
3		dihlss.i	|- I = ( ( DIsoH ` K ) ` W )
4		dihlss.u	|- U = ( ( DVecH ` K ) ` W )
5		dihlss.s	|- S = ( LSubSp ` U )
6		eqid	|- ( le ` K ) = ( le ` K )
7		eqid	|- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
8	1 6 2 3 7	dihvalb	|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
9	1 6 2 4 7 5	diblss	|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` X ) e. S )
10	8 9	eqeltrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( I ` X ) e. S )
11	10	anassrs	|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. B ) /\ X ( le ` K ) W ) -> ( I ` X ) e. S )
12		eqid	|- ( join ` K ) = ( join ` K )
13		eqid	|- ( meet ` K ) = ( meet ` K )
14		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
15		eqid	|- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
16		eqid	|- ( LSSum ` U ) = ( LSSum ` U )
17	1 6 12 13 14 2 3 7 15 4 5 16	dihlsscpre	|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X ( le ` K ) W ) ) -> ( I ` X ) e. S )
18	17	anassrs	|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. B ) /\ -. X ( le ` K ) W ) -> ( I ` X ) e. S )
19	11 18	pm2.61dan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. S )