# Metamath Proof Explorer

## Theorem ocv2ss

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

Ref Expression
Hypothesis ocv2ss.o
Assertion ocv2ss

### Proof

Step Hyp Ref Expression
1 ocv2ss.o
2 sstr2 ${⊢}{T}\subseteq {S}\to \left({S}\subseteq {\mathrm{Base}}_{{W}}\to {T}\subseteq {\mathrm{Base}}_{{W}}\right)$
3 idd ${⊢}{T}\subseteq {S}\to \left({x}\in {\mathrm{Base}}_{{W}}\to {x}\in {\mathrm{Base}}_{{W}}\right)$
4 ssralv ${⊢}{T}\subseteq {S}\to \left(\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\to \forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
5 2 3 4 3anim123d ${⊢}{T}\subseteq {S}\to \left(\left({S}\subseteq {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)\to \left({T}\subseteq {\mathrm{Base}}_{{W}}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge \forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
7 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
8 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
9 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
10 6 7 8 9 1 elocv
11 6 7 8 9 1 elocv
12 5 10 11 3imtr4g
13 12 ssrdv