Theorem dihrnss

Description: The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014)

	Ref	Expression
Hypotheses	dihrnss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihrnss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihrnss.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihrnss.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
Assertion	dihrnss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		dihrnss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihrnss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dihrnss.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dihrnss.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
6	1 2 3 5	dihrnlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
7	4 5	lssss	⊢ ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) → 𝑋 ⊆ 𝑉 )
8	6 7	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )