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