ocv2ss

Description: Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Hypothesis	ocv2ss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	Assertion	ocv2ss	$⊢ T \subseteq S \to \underset{˙}{⊥} (S) \subseteq \underset{˙}{⊥} (T)$

Step	Hyp	Ref	Expression
1		ocv2ss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		sstr2	$⊢ T \subseteq S \to (S \subseteq {Base}_{W} \to T \subseteq {Base}_{W})$
3		idd	$⊢ T \subseteq S \to (x \in {Base}_{W} \to x \in {Base}_{W})$
4		ssralv	$⊢ T \subseteq S \to (\forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)} \to \forall y \in T x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
5	2 3 4	3anim123d	$⊢ T \subseteq S \to ((S \subseteq {Base}_{W} \land x \in {Base}_{W} \land \forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \to (T \subseteq {Base}_{W} \land x \in {Base}_{W} \land \forall y \in T x \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
8		eqid	$⊢ Scalar (W) = Scalar (W)$
9		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
10	6 7 8 9 1	elocv	$⊢ x \in \underset{˙}{⊥} (S) \leftrightarrow (S \subseteq {Base}_{W} \land x \in {Base}_{W} \land \forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
11	6 7 8 9 1	elocv	$⊢ x \in \underset{˙}{⊥} (T) \leftrightarrow (T \subseteq {Base}_{W} \land x \in {Base}_{W} \land \forall y \in T x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
12	5 10 11	3imtr4g	$⊢ T \subseteq S \to (x \in \underset{˙}{⊥} (S) \to x \in \underset{˙}{⊥} (T))$
13	12	ssrdv	$⊢ T \subseteq S \to \underset{˙}{⊥} (S) \subseteq \underset{˙}{⊥} (T)$

Metamath Proof Explorer