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 = ( Base ` W )`
mrccss.o
`|- ._|_ = ( ocv ` W )`
mrccss.c
`|- C = ( ClSubSp ` W )`
mrccss.f
`|- F = ( mrCls ` C )`
Assertion mrccss
`|- ( ( W e. PreHil /\ S C_ V ) -> ( F ` S ) = ( ._|_ ` ( ._|_ ` S ) ) )`

Proof

Step Hyp Ref Expression
1 mrccss.v
` |-  V = ( Base ` W )`
2 mrccss.o
` |-  ._|_ = ( ocv ` W )`
3 mrccss.c
` |-  C = ( ClSubSp ` W )`
4 mrccss.f
` |-  F = ( mrCls ` C )`
5 1 3 cssmre
` |-  ( W e. PreHil -> C e. ( Moore ` V ) )`
` |-  ( ( W e. PreHil /\ S C_ V ) -> C e. ( Moore ` V ) )`
7 1 2 ocvocv
` |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( ._|_ ` ( ._|_ ` S ) ) )`
8 1 2 ocvss
` |-  ( ._|_ ` S ) C_ V`
9 8 a1i
` |-  ( S C_ V -> ( ._|_ ` S ) C_ V )`
10 1 3 2 ocvcss
` |-  ( ( W e. PreHil /\ ( ._|_ ` S ) C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) e. C )`
11 9 10 sylan2
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) e. C )`
12 4 mrcsscl
` |-  ( ( C e. ( Moore ` V ) /\ S C_ ( ._|_ ` ( ._|_ ` S ) ) /\ ( ._|_ ` ( ._|_ ` S ) ) e. C ) -> ( F ` S ) C_ ( ._|_ ` ( ._|_ ` S ) ) )`
13 6 7 11 12 syl3anc
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( F ` S ) C_ ( ._|_ ` ( ._|_ ` S ) ) )`
14 4 mrcssid
` |-  ( ( C e. ( Moore ` V ) /\ S C_ V ) -> S C_ ( F ` S ) )`
15 5 14 sylan
` |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ ( F ` S ) )`
16 2 ocv2ss
` |-  ( S C_ ( F ` S ) -> ( ._|_ ` ( F ` S ) ) C_ ( ._|_ ` S ) )`
17 2 ocv2ss
` |-  ( ( ._|_ ` ( F ` S ) ) C_ ( ._|_ ` S ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( ._|_ ` ( ._|_ ` ( F ` S ) ) ) )`
18 15 16 17 3syl
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( ._|_ ` ( ._|_ ` ( F ` S ) ) ) )`
19 4 mrccl
` |-  ( ( C e. ( Moore ` V ) /\ S C_ V ) -> ( F ` S ) e. C )`
20 5 19 sylan
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( F ` S ) e. C )`
21 2 3 cssi
` |-  ( ( F ` S ) e. C -> ( F ` S ) = ( ._|_ ` ( ._|_ ` ( F ` S ) ) ) )`
22 20 21 syl
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( F ` S ) = ( ._|_ ` ( ._|_ ` ( F ` S ) ) ) )`
23 18 22 sseqtrrd
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( F ` S ) )`
24 13 23 eqssd
` |-  ( ( W e. PreHil /\ S C_ V ) -> ( F ` S ) = ( ._|_ ` ( ._|_ ` S ) ) )`