Theorem dochoc0

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

	Ref	Expression
Hypotheses	dochoc0.h	|- H = ( LHyp ` K )
	dochoc0.u	|- U = ( ( DVecH ` K ) ` W )
	dochoc0.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochoc0.z	|- .0. = ( 0g ` U )
	dochoc0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	dochoc0	|- ( ph -> ( ._|_ ` ( ._|_ ` { .0. } ) ) = { .0. } )

Proof

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