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

Metamath Proof Explorer

Theorem ocvocv

Description: A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocvocv ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ocvss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ocvss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
3 1 2 ocvss ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
4 3 a1i ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
5 simpr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
6 5 sselda ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
7 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
8 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
10 1 7 8 9 2 ocvi ⊢ ( ( 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
11 10 ancoms ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
12 11 adantll ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
13 simplll ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑊 ∈ PreHil )
14 4 sselda ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑦 ∈ 𝑉 )
15 6 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑉 )
16 8 7 1 9 iporthcom ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
18 12 17 mpbid ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
19 18 ralrimiva ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
20 1 7 8 9 2 elocv ⊢ ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
21 4 6 19 20 syl3anbrc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
22 21 ex ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
23 22 ssrdv ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )