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

Metamath Proof Explorer

Theorem dia1N

Description: The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1.h 
|- H = ( LHyp ` K )
dia1.t 
|- T = ( ( LTrn ` K ) ` W )
dia1.i 
|- I = ( ( DIsoA ` K ) ` W )
Assertion dia1N 
|- ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )

Proof

Step Hyp Ref Expression
1 dia1.h 
 |-  H = ( LHyp ` K )
2 dia1.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dia1.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 5 1 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
7 6 adantl 
 |-  ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
8 hllat 
 |-  ( K e. HL -> K e. Lat )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 5 9 latref 
 |-  ( ( K e. Lat /\ W e. ( Base ` K ) ) -> W ( le ` K ) W )
11 8 6 10 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> W ( le ` K ) W )
12 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
13 5 9 1 2 12 3 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( W e. ( Base ` K ) /\ W ( le ` K ) W ) ) -> ( I ` W ) = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
14 4 7 11 13 syl12anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` W ) = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
15 9 1 2 12 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
16 15 ralrimiva 
 |-  ( ( K e. HL /\ W e. H ) -> A. f e. T ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
17 rabid2 
 |-  ( T = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } <-> A. f e. T ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
18 16 17 sylibr 
 |-  ( ( K e. HL /\ W e. H ) -> T = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
19 14 18 eqtr4d 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )