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