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

Metamath Proof Explorer

Theorem ocvsscon

Description: Two ways to say that S and T are orthogonal subspaces. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvlsp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvlsp.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocvsscon ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ↔ 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ocvlsp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ocvlsp.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
3 1 2 ocvocv ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) )
4 3 3adant2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) )
5 2 ocv2ss ⊢ ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ⊆ ( ⊥ ‘ 𝑆 ) )
6 sstr2 ⊢ ( 𝑇 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ⊆ ( ⊥ ‘ 𝑆 ) → 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) )
7 4 5 6 syl2im ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) → 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) )
8 1 2 ocvocv ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
9 8 3adant3 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
10 2 ocv2ss ⊢ ( 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑇 ) )
11 sstr2 ⊢ ( 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( ⊥ ‘ 𝑇 ) → 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ) )
12 9 10 11 syl2im ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) → 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ) )
13 7 12 impbid ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉 ) → ( 𝑆 ⊆ ( ⊥ ‘ 𝑇 ) ↔ 𝑇 ⊆ ( ⊥ ‘ 𝑆 ) ) )