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 ⊢ H = LHyp ⁡ K
dochlss.u ⊢ U = DVecH ⁡ K ⁡ W
dochlss.v ⊢ V = Base U
dochlss.s ⊢ S = LSubSp ⁡ U
dochlss.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
Assertion dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ S

Proof

Step Hyp Ref Expression
1 dochlss.h ⊢ H = LHyp ⁡ K
2 dochlss.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochlss.v ⊢ V = Base U
4 dochlss.s ⊢ S = LSubSp ⁡ U
5 dochlss.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
7 1 6 2 3 5 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
8 1 2 6 4 dihrnlss ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ X ∈ S
9 7 8 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ S