Theorem dihdm

Description: Domain of isomorphism H. (Contributed by NM, 9-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	dihdm	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{dom}I=B$$

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	1 2 3	dihfn	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to IFnB$$
5	4	fndmd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{dom}I=B$$