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 𝐼 ) → 𝑋 ⊆ 𝑉 ) |
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 𝐼 ) → 𝑋 ⊆ 𝑉 ) |