# Metamath Proof Explorer

## Theorem ocv2ss

Description: Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis ocv2ss.o = ( ocv ‘ 𝑊 )
Assertion ocv2ss ( 𝑇𝑆 → ( 𝑆 ) ⊆ ( 𝑇 ) )

### Proof

Step Hyp Ref Expression
1 ocv2ss.o = ( ocv ‘ 𝑊 )
2 sstr2 ( 𝑇𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑊 ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) ) )
3 idd ( 𝑇𝑆 → ( 𝑥 ∈ ( Base ‘ 𝑊 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) ) )
4 ssralv ( 𝑇𝑆 → ( ∀ 𝑦𝑆 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ∀ 𝑦𝑇 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
5 2 3 4 3anim123d ( 𝑇𝑆 → ( ( 𝑆 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦𝑆 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑇 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦𝑇 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
6 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
8 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 eqid ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
10 6 7 8 9 1 elocv ( 𝑥 ∈ ( 𝑆 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦𝑆 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
11 6 7 8 9 1 elocv ( 𝑥 ∈ ( 𝑇 ) ↔ ( 𝑇 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦𝑇 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
12 5 10 11 3imtr4g ( 𝑇𝑆 → ( 𝑥 ∈ ( 𝑆 ) → 𝑥 ∈ ( 𝑇 ) ) )
13 12 ssrdv ( 𝑇𝑆 → ( 𝑆 ) ⊆ ( 𝑇 ) )