Metamath Proof Explorer

Theorem dihcl

Description: Closure of isomorphism H. (Contributed by NM, 8-Mar-2014)

Ref Expression
Hypotheses dihfn.b ⊢ B = Base K
dihfn.h ⊢ H = LHyp ⁡ K
dihfn.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ ran ⁡ I

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 6 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W
8 f1fn ⊢ I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W → I Fn B
9 7 8 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I Fn B
10 fnfvelrn ⊢ I Fn B ∧ X ∈ B → I ⁡ X ∈ ran ⁡ I
11 9 10 sylancom ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ ran ⁡ I