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 ) )
6 5 adantr 
 |-  ( ( 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 ) ) )