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	$⊢ \underset{˙}{⊥} = ocv (W)$
	Assertion	ocvsscon	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to (S \subseteq \underset{˙}{⊥} (T) \leftrightarrow T \subseteq \underset{˙}{⊥} (S))$

Proof

Step	Hyp	Ref	Expression
1		ocvlsp.v	$⊢ V = {Base}_{W}$
2		ocvlsp.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3	1 2	ocvocv	$⊢ (W \in PreHil \land T \subseteq V) \to T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
4	3	3adant2	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
5	2	ocv2ss	$⊢ S \subseteq \underset{˙}{⊥} (T) \to \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq \underset{˙}{⊥} (S)$
6		sstr2	$⊢ T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq \underset{˙}{⊥} (S) \to T \subseteq \underset{˙}{⊥} (S))$
7	4 5 6	syl2im	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to (S \subseteq \underset{˙}{⊥} (T) \to T \subseteq \underset{˙}{⊥} (S))$
8	1 2	ocvocv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
9	8	3adant3	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
10	2	ocv2ss	$⊢ T \subseteq \underset{˙}{⊥} (S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq \underset{˙}{⊥} (T)$
11		sstr2	$⊢ S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq \underset{˙}{⊥} (T) \to S \subseteq \underset{˙}{⊥} (T))$
12	9 10 11	syl2im	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to (T \subseteq \underset{˙}{⊥} (S) \to S \subseteq \underset{˙}{⊥} (T))$
13	7 12	impbid	$⊢ (W \in PreHil \land S \subseteq V \land T \subseteq V) \to (S \subseteq \underset{˙}{⊥} (T) \leftrightarrow T \subseteq \underset{˙}{⊥} (S))$