Theorem dochlss

Description: A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014)

	Ref	Expression
Hypotheses	dochlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochlss.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	dochlss.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dochlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dochlss.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		dochlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		dochlss.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7	1 6 2 3 5	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
8	1 2 6 4	dihrnlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )
9	7 8	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )