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

Metamath Proof Explorer

Theorem dihss

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

Ref Expression
Hypotheses dihss.b ⊢ B = Base K
dihss.h ⊢ H = LHyp ⁡ K
dihss.i ⊢ I = DIsoH ⁡ K ⁡ W
dihss.u ⊢ U = DVecH ⁡ K ⁡ W
dihss.v ⊢ V = Base U
Assertion dihss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ⊆ V

Proof

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