This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ocvlsp

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

Ref Expression
Hypotheses ocvlsp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvlsp.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
ocvlsp.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion ocvlsp ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝑁 ‘ 𝑆 ) ) = ( ⊥ ‘ 𝑆 ) )

Proof

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