Theorem dih0rn

Description: The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih0rn.h	|- H = ( LHyp ` K )
	dih0rn.i	|- I = ( ( DIsoH ` K ) ` W )
	dih0rn.u	|- U = ( ( DVecH ` K ) ` W )
	dih0rn.o	|- .0. = ( 0g ` U )
Assertion	dih0rn	|- ( ( K e. HL /\ W e. H ) -> { .0. } e. ran I )

Proof

Step	Hyp	Ref	Expression
1		dih0rn.h	|- H = ( LHyp ` K )
2		dih0rn.i	|- I = ( ( DIsoH ` K ) ` W )
3		dih0rn.u	|- U = ( ( DVecH ` K ) ` W )
4		dih0rn.o	|- .0. = ( 0g ` U )
5		eqid	|- ( 0. ` K ) = ( 0. ` K )
6	5 1 2 3 4	dih0	|- ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) = { .0. } )
7		eqid	|- ( Base ` K ) = ( Base ` K )
8	7 1 2	dihfn	|- ( ( K e. HL /\ W e. H ) -> I Fn ( Base ` K ) )
9		hlop	|- ( K e. HL -> K e. OP )
10	9	adantr	|- ( ( K e. HL /\ W e. H ) -> K e. OP )
11	7 5	op0cl	|- ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
12	10 11	syl	|- ( ( K e. HL /\ W e. H ) -> ( 0. ` K ) e. ( Base ` K ) )
13		fnfvelrn	|- ( ( I Fn ( Base ` K ) /\ ( 0. ` K ) e. ( Base ` K ) ) -> ( I ` ( 0. ` K ) ) e. ran I )
14	8 12 13	syl2anc	|- ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) e. ran I )
15	6 14	eqeltrrd	|- ( ( K e. HL /\ W e. H ) -> { .0. } e. ran I )