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}={\mathrm{Base}}_{{K}}$
dihss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihss.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
Assertion dihss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\subseteq {V}$

Proof

Step Hyp Ref Expression
1 dihss.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dihss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dihss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dihss.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
7 1 2 3 4 6 dihlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in \mathrm{LSubSp}\left({U}\right)$
8 5 6 lssss ${⊢}{I}\left({X}\right)\in \mathrm{LSubSp}\left({U}\right)\to {I}\left({X}\right)\subseteq {V}$
9 7 8 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\subseteq {V}$