Theorem dihdm

Description: Domain of isomorphism H. (Contributed by NM, 9-Mar-2014)

	Ref	Expression
Hypotheses	dihfn.b	|- B = ( Base ` K )
	dihfn.h	|- H = ( LHyp ` K )
	dihfn.i	|- I = ( ( DIsoH ` K ) ` W )
Assertion	dihdm	|- ( ( K e. HL /\ W e. H ) -> dom I = B )

Proof

Step	Hyp	Ref	Expression
1		dihfn.b	|- B = ( Base ` K )
2		dihfn.h	|- H = ( LHyp ` K )
3		dihfn.i	|- I = ( ( DIsoH ` K ) ` W )
4	1 2 3	dihfn	|- ( ( K e. HL /\ W e. H ) -> I Fn B )
5	4	fndmd	|- ( ( K e. HL /\ W e. H ) -> dom I = B )