Metamath Proof Explorer


Theorem dihrnss

Description: The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dihrnss.h 𝐻 = ( LHyp ‘ 𝐾 )
dihrnss.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihrnss.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihrnss.v 𝑉 = ( Base ‘ 𝑈 )
Assertion dihrnss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋𝑉 )

Proof

Step Hyp Ref Expression
1 dihrnss.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dihrnss.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihrnss.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihrnss.v 𝑉 = ( Base ‘ 𝑈 )
5 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
6 1 2 3 5 dihrnlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
7 4 5 lssss ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) → 𝑋𝑉 )
8 6 7 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋𝑉 )