Theorem dihdm

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

	Ref	Expression
Hypotheses	dihfn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihfn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dihdm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dihfn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dihfn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4	1 2 3	dihfn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn 𝐵 )
5	4	fndmd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = 𝐵 )