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

Metamath Proof Explorer

Theorem dihsslss

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

Ref Expression
Hypotheses dihsslss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihsslss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihsslss.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihsslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion dihsslss ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 dihsslss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihsslss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dihsslss.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihsslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 1 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) = 𝑥 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 1 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) )
8 6 1 3 2 4 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) ∈ 𝑆 )
9 7 8 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) ∈ 𝑆 )
10 5 9 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ∈ 𝑆 )
11 10 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ ran 𝐼 → 𝑥 ∈ 𝑆 ) )
12 11 ssrdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )