Theorem dihcl

Description: Closure of isomorphism H. (Contributed by NM, 8-Mar-2014)

	Ref	Expression
Hypotheses	dihfn.b	$$⊢B={\mathrm{Base}}_K$$
	dihfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihfn.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	dihcl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\right)\in \mathrm{ran}I$$

Proof

Step	Hyp	Ref	Expression
1		dihfn.b	$$⊢B={\mathrm{Base}}_K$$
2		dihfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihfn.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		eqid	$$⊢\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)=\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
6	1 2 3 4 5	dihf11	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I:B\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
7	6	adantr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to I:B\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
8		f1fn	$$⊢I:B\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)\to IFnB$$
9	7 8	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to IFnB$$
10		fnfvelrn	$$⊢\left(IFnB\wedge X\in B\right)\to I\left(X\right)\in \mathrm{ran}I$$
11	9 10	sylancom	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\right)\in \mathrm{ran}I$$