# Metamath Proof Explorer

## Theorem dihfn

Description: Functionality and 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 dihfn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn{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 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 1 2 3 4 5 dihf11 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:{B}\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
7 f1fn ${⊢}{I}:{B}\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\to {I}Fn{B}$
8 6 7 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn{B}$