Metamath Proof Explorer

Theorem ocvlsp

Description: The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvlsp.v ⊢ V = Base W
ocvlsp.o ⊢ ⊥ ˙ = ocv ⁡ W
ocvlsp.n ⊢ N = LSpan ⁡ W
Assertion ocvlsp ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ N ⁡ S = ⊥ ˙ ⁡ S

Proof

Step Hyp Ref Expression
1 ocvlsp.v ⊢ V = Base W
2 ocvlsp.o ⊢ ⊥ ˙ = ocv ⁡ W
3 ocvlsp.n ⊢ N = LSpan ⁡ W
4 phllmod ⊢ W ∈ PreHil → W ∈ LMod
5 1 3 lspssid ⊢ W ∈ LMod ∧ S ⊆ V → S ⊆ N ⁡ S
6 4 5 sylan ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ N ⁡ S
7 2 ocv2ss ⊢ S ⊆ N ⁡ S → ⊥ ˙ ⁡ N ⁡ S ⊆ ⊥ ˙ ⁡ S
8 6 7 syl ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ N ⁡ S ⊆ ⊥ ˙ ⁡ S
9 1 2 ocvss ⊢ ⊥ ˙ ⁡ S ⊆ V
10 9 a1i ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ⊆ V
11 1 2 ocvocv ⊢ W ∈ PreHil ∧ ⊥ ˙ ⁡ S ⊆ V → ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
12 10 11 syldan ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
13 4 adantr ⊢ W ∈ PreHil ∧ S ⊆ V → W ∈ LMod
14 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
15 1 2 14 ocvlss ⊢ W ∈ PreHil ∧ ⊥ ˙ ⁡ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ LSubSp ⁡ W
16 10 15 syldan ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ LSubSp ⁡ W
17 1 2 ocvocv ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
18 14 3 lspssp ⊢ W ∈ LMod ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ LSubSp ⁡ W ∧ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → N ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
19 13 16 17 18 syl3anc ⊢ W ∈ PreHil ∧ S ⊆ V → N ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
20 2 ocv2ss ⊢ N ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ N ⁡ S
21 19 20 syl ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ N ⁡ S
22 12 21 sstrd ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ N ⁡ S
23 8 22 eqssd ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ N ⁡ S = ⊥ ˙ ⁡ S