Metamath Proof Explorer

Theorem dib0

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

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

Proof

Step Hyp Ref Expression
1 dib0.z 
 |-  .0. = ( 0. ` K )
2 dib0.h 
 |-  H = ( LHyp ` K )
3 dib0.i 
 |-  I = ( ( DIsoB ` K ) ` W )
4 dib0.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dib0.o 
 |-  O = ( 0g ` U )
6 fvex 
 |-  ( Base ` K ) e. _V
7 resiexg 
 |-  ( ( Base ` K ) e. _V -> ( _I |` ( Base ` K ) ) e. _V )
8 6 7 ax-mp 
 |-  ( _I |` ( Base ` K ) ) e. _V
9 fvex 
 |-  ( ( LTrn ` K ) ` W ) e. _V
10 9 mptex 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) e. _V
11 8 10 xpsn 
 |-  ( { ( _I |` ( Base ` K ) ) } X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) = { <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. }
12 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
13 hlop 
 |-  ( K e. HL -> K e. OP )
14 13 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. OP )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 15 1 op0cl 
 |-  ( K e. OP -> .0. e. ( Base ` K ) )
17 14 16 syl 
 |-  ( ( K e. HL /\ W e. H ) -> .0. e. ( Base ` K ) )
18 15 2 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
19 eqid 
 |-  ( le ` K ) = ( le ` K )
20 15 19 1 op0le 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> .0. ( le ` K ) W )
21 13 18 20 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> .0. ( le ` K ) W )
22 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
23 eqid 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
24 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
25 15 19 2 22 23 24 3 dibval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( .0. e. ( Base ` K ) /\ .0. ( le ` K ) W ) ) -> ( I ` .0. ) = ( ( ( ( DIsoA ` K ) ` W ) ` .0. ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) )
26 12 17 21 25 syl12anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = ( ( ( ( DIsoA ` K ) ` W ) ` .0. ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) )
27 15 1 2 24 dia0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoA ` K ) ` W ) ` .0. ) = { ( _I |` ( Base ` K ) ) } )
28 27 xpeq1d 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( DIsoA ` K ) ` W ) ` .0. ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) = ( { ( _I |` ( Base ` K ) ) } X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) )
29 26 28 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = ( { ( _I |` ( Base ` K ) ) } X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) )
30 15 2 22 4 5 23 dvh0g 
 |-  ( ( K e. HL /\ W e. H ) -> O = <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. )
31 30 sneqd 
 |-  ( ( K e. HL /\ W e. H ) -> { O } = { <. ( _I |` ( Base ` K ) ) , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) >. } )
32 11 29 31 3eqtr4a 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { O } )