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