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

Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝑆 )