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 𝐼 ⊆ 𝑆 )