Theorem dih0sb

Description: A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014)

	Ref	Expression
Hypotheses	dih0sb.h	|- H = ( LHyp ` K )
	dih0sb.o	|- .0. = ( 0. ` K )
	dih0sb.i	|- I = ( ( DIsoH ` K ) ` W )
	dih0sb.u	|- U = ( ( DVecH ` K ) ` W )
	dih0sb.v	|- V = ( Base ` U )
	dih0sb.z	|- Z = ( 0g ` U )
	dih0sb.n	|- N = ( LSpan ` U )
	dih0sb.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dih0sb.x	|- ( ph -> X e. ran I )
Assertion	dih0sb	|- ( ph -> ( X = { Z } <-> ( `' I ` X ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		dih0sb.h	|- H = ( LHyp ` K )
2		dih0sb.o	|- .0. = ( 0. ` K )
3		dih0sb.i	|- I = ( ( DIsoH ` K ) ` W )
4		dih0sb.u	|- U = ( ( DVecH ` K ) ` W )
5		dih0sb.v	|- V = ( Base ` U )
6		dih0sb.z	|- Z = ( 0g ` U )
7		dih0sb.n	|- N = ( LSpan ` U )
8		dih0sb.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dih0sb.x	|- ( ph -> X e. ran I )
10	1 3 4 6	dih0rn	|- ( ( K e. HL /\ W e. H ) -> { Z } e. ran I )
11	8 10	syl	|- ( ph -> { Z } e. ran I )
12	1 3 8 9 11	dihcnv11	|- ( ph -> ( ( `' I ` X ) = ( `' I ` { Z } ) <-> X = { Z } ) )
13	1 2 3 4 6	dih0cnv	|- ( ( K e. HL /\ W e. H ) -> ( `' I ` { Z } ) = .0. )
14	8 13	syl	|- ( ph -> ( `' I ` { Z } ) = .0. )
15	14	eqeq2d	|- ( ph -> ( ( `' I ` X ) = ( `' I ` { Z } ) <-> ( `' I ` X ) = .0. ) )
16	12 15	bitr3d	|- ( ph -> ( X = { Z } <-> ( `' I ` X ) = .0. ) )