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

Metamath Proof Explorer

Theorem dia1elN

Description: The largest subspace in the range of partial isomorphism A. (Contributed by NM, 5-Dec-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 dia1elN 
|- ( ( K e. HL /\ W e. H ) -> T e. ran I )

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 1 2 3 dia1N 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )
5 1 3 diaf11N 
 |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
6 f1ofun 
 |-  ( I : dom I -1-1-onto-> ran I -> Fun I )
7 5 6 syl 
 |-  ( ( K e. HL /\ W e. H ) -> Fun I )
8 1 3 dia1eldmN 
 |-  ( ( K e. HL /\ W e. H ) -> W e. dom I )
9 fvelrn 
 |-  ( ( Fun I /\ W e. dom I ) -> ( I ` W ) e. ran I )
10 7 8 9 syl2anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` W ) e. ran I )
11 4 10 eqeltrrd 
 |-  ( ( K e. HL /\ W e. H ) -> T e. ran I )