# Metamath Proof Explorer

## Theorem mrccss

Description: The Moore closure corresponding to the system of closed subspaces is the double orthocomplement operation. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses mrccss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
mrccss.o
mrccss.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
mrccss.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
Assertion mrccss

### Proof

Step Hyp Ref Expression
1 mrccss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 mrccss.o
3 mrccss.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
4 mrccss.f ${⊢}{F}=\mathrm{mrCls}\left({C}\right)$
5 1 3 cssmre ${⊢}{W}\in \mathrm{PreHil}\to {C}\in \mathrm{Moore}\left({V}\right)$
6 5 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {S}\subseteq {V}\right)\to {C}\in \mathrm{Moore}\left({V}\right)$
7 1 2 ocvocv
8 1 2 ocvss
9 8 a1i
10 1 3 2 ocvcss
11 9 10 sylan2
12 4 mrcsscl
13 6 7 11 12 syl3anc
14 4 mrcssid ${⊢}\left({C}\in \mathrm{Moore}\left({V}\right)\wedge {S}\subseteq {V}\right)\to {S}\subseteq {F}\left({S}\right)$
15 5 14 sylan ${⊢}\left({W}\in \mathrm{PreHil}\wedge {S}\subseteq {V}\right)\to {S}\subseteq {F}\left({S}\right)$
16 2 ocv2ss
17 2 ocv2ss
18 15 16 17 3syl
19 4 mrccl ${⊢}\left({C}\in \mathrm{Moore}\left({V}\right)\wedge {S}\subseteq {V}\right)\to {F}\left({S}\right)\in {C}$
20 5 19 sylan ${⊢}\left({W}\in \mathrm{PreHil}\wedge {S}\subseteq {V}\right)\to {F}\left({S}\right)\in {C}$
21 2 3 cssi
22 20 21 syl
23 18 22 sseqtrrd
24 13 23 eqssd