Theorem dochssv

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

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

Proof

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