This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )