Theorem dochoc1

Description: The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	dochoc1.h	|- H = ( LHyp ` K )
	dochoc1.u	|- U = ( ( DVecH ` K ) ` W )
	dochoc1.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochoc1.v	|- V = ( Base ` U )
	dochoc1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	dochoc1	|- ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )

Proof

Step	Hyp	Ref	Expression
1		dochoc1.h	|- H = ( LHyp ` K )
2		dochoc1.u	|- U = ( ( DVecH ` K ) ` W )
3		dochoc1.o	|- ._|_ = ( ( ocH ` K ) ` W )
4		dochoc1.v	|- V = ( Base ` U )
5		dochoc1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		eqid	|- ( 0g ` U ) = ( 0g ` U )
7	1 2 3 4 6	doch1	|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` V ) = { ( 0g ` U ) } )
8	7	fveq2d	|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` ( ._|_ ` V ) ) = ( ._|_ ` { ( 0g ` U ) } ) )
9	1 2 3 4 6	doch0	|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = V )
10	8 9	eqtrd	|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` ( ._|_ ` V ) ) = V )
11	5 10	syl	|- ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )