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

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 ⊢ ( 𝑇 ⊆ 𝑆 → ( ⊥ ‘ 𝑆 ) ⊆ ( ⊥ ‘ 𝑇 ) )