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 ⊢ V = Base W
ocvlsp.o ⊢ ⊥ ˙ = ocv ⁡ W
Assertion ocvsscon ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → S ⊆ ⊥ ˙ ⁡ T ↔ T ⊆ ⊥ ˙ ⁡ S

Proof

Step Hyp Ref Expression
1 ocvlsp.v ⊢ V = Base W
2 ocvlsp.o ⊢ ⊥ ˙ = ocv ⁡ W
3 1 2 ocvocv ⊢ W ∈ PreHil ∧ T ⊆ V → T ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ T
4 3 3adant2 ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → T ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ T
5 2 ocv2ss ⊢ S ⊆ ⊥ ˙ ⁡ T → ⊥ ˙ ⁡ ⊥ ˙ ⁡ T ⊆ ⊥ ˙ ⁡ S
6 sstr2 ⊢ T ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ T → ⊥ ˙ ⁡ ⊥ ˙ ⁡ T ⊆ ⊥ ˙ ⁡ S → T ⊆ ⊥ ˙ ⁡ S
7 4 5 6 syl2im ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → S ⊆ ⊥ ˙ ⁡ T → T ⊆ ⊥ ˙ ⁡ S
8 1 2 ocvocv ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
9 8 3adant3 ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
10 2 ocv2ss ⊢ T ⊆ ⊥ ˙ ⁡ S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ T
11 sstr2 ⊢ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ T → S ⊆ ⊥ ˙ ⁡ T
12 9 10 11 syl2im ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → T ⊆ ⊥ ˙ ⁡ S → S ⊆ ⊥ ˙ ⁡ T
13 7 12 impbid ⊢ W ∈ PreHil ∧ S ⊆ V ∧ T ⊆ V → S ⊆ ⊥ ˙ ⁡ T ↔ T ⊆ ⊥ ˙ ⁡ S