Theorem dih0

Description: The value of isomorphism H at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 9-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dih0.z	|- .0. = ( 0. ` K )
2		dih0.h	|- H = ( LHyp ` K )
3		dih0.i	|- I = ( ( DIsoH ` K ) ` W )
4		dih0.u	|- U = ( ( DVecH ` K ) ` W )
5		dih0.o	|- O = ( 0g ` U )
6		id	|- ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
7		hlop	|- ( K e. HL -> K e. OP )
8	7	adantr	|- ( ( K e. HL /\ W e. H ) -> K e. OP )
9		eqid	|- ( Base ` K ) = ( Base ` K )
10	9 1	op0cl	|- ( K e. OP -> .0. e. ( Base ` K ) )
11	8 10	syl	|- ( ( K e. HL /\ W e. H ) -> .0. e. ( Base ` K ) )
12	9 2	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
13		eqid	|- ( le ` K ) = ( le ` K )
14	9 13 1	op0le	|- ( ( K e. OP /\ W e. ( Base ` K ) ) -> .0. ( le ` K ) W )
15	7 12 14	syl2an	|- ( ( K e. HL /\ W e. H ) -> .0. ( le ` K ) W )
16		eqid	|- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
17	9 13 2 3 16	dihvalb	|- ( ( ( K e. HL /\ W e. H ) /\ ( .0. e. ( Base ` K ) /\ .0. ( le ` K ) W ) ) -> ( I ` .0. ) = ( ( ( DIsoB ` K ) ` W ) ` .0. ) )
18	6 11 15 17	syl12anc	|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = ( ( ( DIsoB ` K ) ` W ) ` .0. ) )
19	1 2 16 4 5	dib0	|- ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoB ` K ) ` W ) ` .0. ) = { O } )
20	18 19	eqtrd	|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { O } )