Metamath Proof Explorer

Theorem dochocsp

Description: The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014)

Ref Expression
Hypotheses dochsp.h ⊢ H = LHyp ⁡ K
dochsp.u ⊢ U = DVecH ⁡ K ⁡ W
dochsp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsp.v ⊢ V = Base U
dochsp.n ⊢ N = LSpan ⁡ U
dochsp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsp.x ⊢ φ → X ⊆ V
Assertion dochocsp ⊢ φ → ⊥ ˙ ⁡ N ⁡ X = ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 dochsp.h ⊢ H = LHyp ⁡ K
2 dochsp.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochsp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 dochsp.v ⊢ V = Base U
5 dochsp.n ⊢ N = LSpan ⁡ U
6 dochsp.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochsp.x ⊢ φ → X ⊆ V
8 1 2 6 dvhlmod ⊢ φ → U ∈ LMod
9 4 5 lspssv ⊢ U ∈ LMod ∧ X ⊆ V → N ⁡ X ⊆ V
10 8 7 9 syl2anc ⊢ φ → N ⁡ X ⊆ V
11 4 5 lspssid ⊢ U ∈ LMod ∧ X ⊆ V → X ⊆ N ⁡ X
12 8 7 11 syl2anc ⊢ φ → X ⊆ N ⁡ X
13 1 2 4 3 dochss ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ X ⊆ V ∧ X ⊆ N ⁡ X → ⊥ ˙ ⁡ N ⁡ X ⊆ ⊥ ˙ ⁡ X
14 6 10 12 13 syl3anc ⊢ φ → ⊥ ˙ ⁡ N ⁡ X ⊆ ⊥ ˙ ⁡ X
15 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
16 1 15 2 4 3 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
17 6 7 16 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
18 1 15 3 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
19 6 17 18 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ X
20 1 2 4 3 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
21 6 7 20 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ⊆ V
22 1 2 4 3 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
23 6 21 22 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V
24 1 2 3 4 5 6 7 dochspss ⊢ φ → N ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
25 1 2 4 3 dochss ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ V ∧ N ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ N ⁡ X
26 6 23 24 25 syl3anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ N ⁡ X
27 19 26 eqsstrrd ⊢ φ → ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ N ⁡ X
28 14 27 eqssd ⊢ φ → ⊥ ˙ ⁡ N ⁡ X = ⊥ ˙ ⁡ X