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 ∧ 𝑆𝑉 ) → 𝑆 ⊆ ( ‘ ( 𝑆 ) ) )