Description: The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dihss.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| dihss.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| dihss.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| dihss.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| dihss.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | ||
| Assertion | dihss | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dihss.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| 2 | dihss.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 3 | dihss.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 4 | dihss.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 5 | dihss.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | |
| 6 | eqid | ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 ) | |
| 7 | 1 2 3 4 6 | dihlss | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) ) |
| 8 | 5 6 | lssss | ⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 ) |
| 9 | 7 8 | syl | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 ) |