Theorem dibdiadm

Description: Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	dibfna.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dibfna.j	⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dibfna.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dibdiadm	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		dibfna.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dibfna.j	⊢ 𝐽 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3		dibfna.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
4	1 2 3	dibfna	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom 𝐽 )
5	4	fndmd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom 𝐽 )