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 𝐻 = ( LHyp ‘ 𝐾 )
dih1rn.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih1rn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih1rn.v 𝑉 = ( Base ‘ 𝑈 )
Assertion dih1rn ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑉 ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dih1rn.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dih1rn.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dih1rn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dih1rn.v 𝑉 = ( Base ‘ 𝑈 )
5 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
6 5 1 2 3 4 dih1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) = 𝑉 )
7 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 7 adantr ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐾 ∈ OP )
9 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 5 op1cl ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
12 9 1 2 dihcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) ∈ ran 𝐼 )
13 11 12 mpdan ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐼 ‘ ( 1. ‘ 𝐾 ) ) ∈ ran 𝐼 )
14 6 13 eqeltrrd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑉 ∈ ran 𝐼 )