Metamath Proof Explorer

Theorem dih1rn

Description: The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014)

Ref Expression
Hypotheses dih1rn.h ⊢ H = LHyp ⁡ K
dih1rn.i ⊢ I = DIsoH ⁡ K ⁡ W
dih1rn.u ⊢ U = DVecH ⁡ K ⁡ W
dih1rn.v ⊢ V = Base U
Assertion dih1rn ⊢ K ∈ HL ∧ W ∈ H → V ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dih1rn.h ⊢ H = LHyp ⁡ K
2 dih1rn.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dih1rn.u ⊢ U = DVecH ⁡ K ⁡ W
4 dih1rn.v ⊢ V = Base U
5 eqid ⊢ 1. ⁡ K = 1. ⁡ K
6 5 1 2 3 4 dih1 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 1. ⁡ K = V
7 hlop ⊢ K ∈ HL → K ∈ OP
8 7 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
9 eqid ⊢ Base K = Base K
10 9 5 op1cl ⊢ K ∈ OP → 1. ⁡ K ∈ Base K
11 8 10 syl ⊢ K ∈ HL ∧ W ∈ H → 1. ⁡ K ∈ Base K
12 9 1 2 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ 1. ⁡ K ∈ Base K → I ⁡ 1. ⁡ K ∈ ran ⁡ I
13 11 12 mpdan ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 1. ⁡ K ∈ ran ⁡ I
14 6 13 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H → V ∈ ran ⁡ I