Metamath Proof Explorer


Theorem dihsslss

Description: The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dihsslss.h H = LHyp K
dihsslss.u U = DVecH K W
dihsslss.i I = DIsoH K W
dihsslss.s S = LSubSp U
Assertion dihsslss K HL W H ran I S

Proof

Step Hyp Ref Expression
1 dihsslss.h H = LHyp K
2 dihsslss.u U = DVecH K W
3 dihsslss.i I = DIsoH K W
4 dihsslss.s S = LSubSp U
5 1 3 dihcnvid2 K HL W H x ran I I I -1 x = x
6 eqid Base K = Base K
7 6 1 3 dihcnvcl K HL W H x ran I I -1 x Base K
8 6 1 3 2 4 dihlss K HL W H I -1 x Base K I I -1 x S
9 7 8 syldan K HL W H x ran I I I -1 x S
10 5 9 eqeltrrd K HL W H x ran I x S
11 10 ex K HL W H x ran I x S
12 11 ssrdv K HL W H ran I S