Theorem dihcnvid2

Description: The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014)

	Ref	Expression
Hypotheses	dihcnvid2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihcnvid2.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
Assertion	dihcnvid2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		dihcnvid2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dihcnvid2.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
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	3 1 2 4 5	dihf11	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I:{\mathrm{Base}}_K\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
7		f1f1orn	$$⊢I:{\mathrm{Base}}_K\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)\to I:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}\mathrm{ran}I$$
8	6 7	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}\mathrm{ran}I$$
9		f1ocnvfv2	$$⊢\left(I:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}\mathrm{ran}I\wedge X\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(X\right)\right)=X$$
10	8 9	sylan	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{ran}I\right)\to I\left(I^{-1}\left(X\right)\right)=X$$