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 )