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

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 𝐼 )