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=\mathrm{LHyp}\left(K\right)$$
	dia1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dia1.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
Assertion	dia1elN	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to T\in \mathrm{ran}I$$

Proof

Step	Hyp	Ref	Expression
1		dia1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dia1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		dia1.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
4	1 2 3	dia1N	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I\left(W\right)=T$$
5	1 3	diaf11N	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{ran}I$$
6		f1ofun	$$⊢I:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{ran}I\to \mathrm{Fun}I$$
7	5 6	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{Fun}I$$
8	1 3	dia1eldmN	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to W\in \mathrm{dom}I$$
9		fvelrn	$$⊢\left(\mathrm{Fun}I\wedge W\in \mathrm{dom}I\right)\to I\left(W\right)\in \mathrm{ran}I$$
10	7 8 9	syl2anc	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I\left(W\right)\in \mathrm{ran}I$$
11	4 10	eqeltrrd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to T\in \mathrm{ran}I$$