Metamath Proof Explorer

Theorem ocvz

Description: The orthocomplement of the zero subspace. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvz.v ⊢ V = Base W
ocvz.o ⊢ ⊥ ˙ = ocv ⁡ W
ocvz.z ⊢ 0 ˙ = 0 W
Assertion ocvz ⊢ W ∈ PreHil → ⊥ ˙ ⁡ 0 ˙ = V

Proof

Step Hyp Ref Expression
1 ocvz.v ⊢ V = Base W
2 ocvz.o ⊢ ⊥ ˙ = ocv ⁡ W
3 ocvz.z ⊢ 0 ˙ = 0 W
4 phllmod ⊢ W ∈ PreHil → W ∈ LMod
5 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
6 3 5 lsp0 ⊢ W ∈ LMod → LSpan ⁡ W ⁡ ∅ = 0 ˙
7 4 6 syl ⊢ W ∈ PreHil → LSpan ⁡ W ⁡ ∅ = 0 ˙
8 7 fveq2d ⊢ W ∈ PreHil → ⊥ ˙ ⁡ LSpan ⁡ W ⁡ ∅ = ⊥ ˙ ⁡ 0 ˙
9 0ss ⊢ ∅ ⊆ V
10 1 2 5 ocvlsp ⊢ W ∈ PreHil ∧ ∅ ⊆ V → ⊥ ˙ ⁡ LSpan ⁡ W ⁡ ∅ = ⊥ ˙ ⁡ ∅
11 9 10 mpan2 ⊢ W ∈ PreHil → ⊥ ˙ ⁡ LSpan ⁡ W ⁡ ∅ = ⊥ ˙ ⁡ ∅
12 1 2 ocv0 ⊢ ⊥ ˙ ⁡ ∅ = V
13 11 12 eqtrdi ⊢ W ∈ PreHil → ⊥ ˙ ⁡ LSpan ⁡ W ⁡ ∅ = V
14 8 13 eqtr3d ⊢ W ∈ PreHil → ⊥ ˙ ⁡ 0 ˙ = V