# 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 𝑉 = ( Base ‘ 𝑊 )
mrccss.o = ( ocv ‘ 𝑊 )
mrccss.c 𝐶 = ( ClSubSp ‘ 𝑊 )
mrccss.f 𝐹 = ( mrCls ‘ 𝐶 )
Assertion mrccss ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) = ( ‘ ( 𝑆 ) ) )

### Proof

Step Hyp Ref Expression
1 mrccss.v 𝑉 = ( Base ‘ 𝑊 )
2 mrccss.o = ( ocv ‘ 𝑊 )
3 mrccss.c 𝐶 = ( ClSubSp ‘ 𝑊 )
4 mrccss.f 𝐹 = ( mrCls ‘ 𝐶 )
5 1 3 cssmre ( 𝑊 ∈ PreHil → 𝐶 ∈ ( Moore ‘ 𝑉 ) )
6 5 adantr ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → 𝐶 ∈ ( Moore ‘ 𝑉 ) )
7 1 2 ocvocv ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → 𝑆 ⊆ ( ‘ ( 𝑆 ) ) )
8 1 2 ocvss ( 𝑆 ) ⊆ 𝑉
9 8 a1i ( 𝑆𝑉 → ( 𝑆 ) ⊆ 𝑉 )
10 1 3 2 ocvcss ( ( 𝑊 ∈ PreHil ∧ ( 𝑆 ) ⊆ 𝑉 ) → ( ‘ ( 𝑆 ) ) ∈ 𝐶 )
11 9 10 sylan2 ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( ‘ ( 𝑆 ) ) ∈ 𝐶 )
12 4 mrcsscl ( ( 𝐶 ∈ ( Moore ‘ 𝑉 ) ∧ 𝑆 ⊆ ( ‘ ( 𝑆 ) ) ∧ ( ‘ ( 𝑆 ) ) ∈ 𝐶 ) → ( 𝐹𝑆 ) ⊆ ( ‘ ( 𝑆 ) ) )
13 6 7 11 12 syl3anc ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) ⊆ ( ‘ ( 𝑆 ) ) )
14 4 mrcssid ( ( 𝐶 ∈ ( Moore ‘ 𝑉 ) ∧ 𝑆𝑉 ) → 𝑆 ⊆ ( 𝐹𝑆 ) )
15 5 14 sylan ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → 𝑆 ⊆ ( 𝐹𝑆 ) )
16 2 ocv2ss ( 𝑆 ⊆ ( 𝐹𝑆 ) → ( ‘ ( 𝐹𝑆 ) ) ⊆ ( 𝑆 ) )
17 2 ocv2ss ( ( ‘ ( 𝐹𝑆 ) ) ⊆ ( 𝑆 ) → ( ‘ ( 𝑆 ) ) ⊆ ( ‘ ( ‘ ( 𝐹𝑆 ) ) ) )
18 15 16 17 3syl ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( ‘ ( 𝑆 ) ) ⊆ ( ‘ ( ‘ ( 𝐹𝑆 ) ) ) )
19 4 mrccl ( ( 𝐶 ∈ ( Moore ‘ 𝑉 ) ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) ∈ 𝐶 )
20 5 19 sylan ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) ∈ 𝐶 )
21 2 3 cssi ( ( 𝐹𝑆 ) ∈ 𝐶 → ( 𝐹𝑆 ) = ( ‘ ( ‘ ( 𝐹𝑆 ) ) ) )
22 20 21 syl ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) = ( ‘ ( ‘ ( 𝐹𝑆 ) ) ) )
23 18 22 sseqtrrd ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( ‘ ( 𝑆 ) ) ⊆ ( 𝐹𝑆 ) )
24 13 23 eqssd ( ( 𝑊 ∈ PreHil ∧ 𝑆𝑉 ) → ( 𝐹𝑆 ) = ( ‘ ( 𝑆 ) ) )