This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihfn

Description: Functionality and 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 dihfn ⊢ K ∈ HL ∧ W ∈ H → I Fn 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 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
5 eqid ⊢ LSubSp ⁡ DVecH ⁡ K ⁡ W = LSubSp ⁡ DVecH ⁡ K ⁡ W
6 1 2 3 4 5 dihf11 ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W
7 f1fn ⊢ I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W → I Fn B
8 6 7 syl ⊢ K ∈ HL ∧ W ∈ H → I Fn B