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

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 ⊢ H = LHyp ⁡ K
dihrnss.u ⊢ U = DVecH ⁡ K ⁡ W
dihrnss.i ⊢ I = DIsoH ⁡ K ⁡ W
dihrnss.v ⊢ V = Base U
Assertion dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ V

Proof

Step Hyp Ref Expression
1 dihrnss.h ⊢ H = LHyp ⁡ K
2 dihrnss.u ⊢ U = DVecH ⁡ K ⁡ W
3 dihrnss.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dihrnss.v ⊢ V = Base U
5 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
6 1 2 3 5 dihrnlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ∈ LSubSp ⁡ U
7 4 5 lssss ⊢ X ∈ LSubSp ⁡ U → X ⊆ V
8 6 7 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ V