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