Metamath Proof Explorer


Theorem dia0

Description: The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses dia0.b
|- B = ( Base ` K )
dia0.z
|- .0. = ( 0. ` K )
dia0.h
|- H = ( LHyp ` K )
dia0.i
|- I = ( ( DIsoA ` K ) ` W )
Assertion dia0
|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { ( _I |` B ) } )

Proof

Step Hyp Ref Expression
1 dia0.b
 |-  B = ( Base ` K )
2 dia0.z
 |-  .0. = ( 0. ` K )
3 dia0.h
 |-  H = ( LHyp ` K )
4 dia0.i
 |-  I = ( ( DIsoA ` K ) ` W )
5 id
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
6 hlatl
 |-  ( K e. HL -> K e. AtLat )
7 1 2 atl0cl
 |-  ( K e. AtLat -> .0. e. B )
8 6 7 syl
 |-  ( K e. HL -> .0. e. B )
9 8 adantr
 |-  ( ( K e. HL /\ W e. H ) -> .0. e. B )
10 1 3 lhpbase
 |-  ( W e. H -> W e. B )
11 eqid
 |-  ( le ` K ) = ( le ` K )
12 1 11 2 atl0le
 |-  ( ( K e. AtLat /\ W e. B ) -> .0. ( le ` K ) W )
13 6 10 12 syl2an
 |-  ( ( K e. HL /\ W e. H ) -> .0. ( le ` K ) W )
14 eqid
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
16 1 11 3 14 15 4 diaval
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( .0. e. B /\ .0. ( le ` K ) W ) ) -> ( I ` .0. ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } )
17 5 9 13 16 syl12anc
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } )
18 6 ad2antrr
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> K e. AtLat )
19 1 3 14 15 trlcl
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. B )
20 1 11 2 atlle0
 |-  ( ( K e. AtLat /\ ( ( ( trL ` K ) ` W ) ` f ) e. B ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) )
21 18 19 20 syl2anc
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) )
22 1 2 3 14 15 trlid0b
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( f = ( _I |` B ) <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) )
23 21 22 bitr4d
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> f = ( _I |` B ) ) )
24 23 rabbidva
 |-  ( ( K e. HL /\ W e. H ) -> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } = { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } )
25 1 3 14 idltrn
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. ( ( LTrn ` K ) ` W ) )
26 rabsn
 |-  ( ( _I |` B ) e. ( ( LTrn ` K ) ` W ) -> { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } = { ( _I |` B ) } )
27 25 26 syl
 |-  ( ( K e. HL /\ W e. H ) -> { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } = { ( _I |` B ) } )
28 17 24 27 3eqtrd
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { ( _I |` B ) } )