Metamath Proof Explorer

Theorem dochssv

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

Ref Expression
Hypotheses dochssv.h ⊢ H = LHyp ⁡ K
dochssv.u ⊢ U = DVecH ⁡ K ⁡ W
dochssv.v ⊢ V = Base U
dochssv.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
Assertion dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V

Proof

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