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 ∈ PreHil ∧ S ⊆ 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 ∈ PreHil → C ∈ Moore ⁡ V
6 5 adantr ⊢ W ∈ PreHil ∧ S ⊆ V → C ∈ Moore ⁡ V
7 1 2 ocvocv ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
8 1 2 ocvss ⊢ ⊥ ˙ ⁡ S ⊆ V
9 8 a1i ⊢ S ⊆ V → ⊥ ˙ ⁡ S ⊆ V
10 1 3 2 ocvcss ⊢ W ∈ PreHil ∧ ⊥ ˙ ⁡ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ C
11 9 10 sylan2 ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ C
12 4 mrcsscl ⊢ C ∈ Moore ⁡ V ∧ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ C → F ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
13 6 7 11 12 syl3anc ⊢ W ∈ PreHil ∧ S ⊆ V → F ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
14 4 mrcssid ⊢ C ∈ Moore ⁡ V ∧ S ⊆ V → S ⊆ F ⁡ S
15 5 14 sylan ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ F ⁡ S
16 2 ocv2ss ⊢ S ⊆ F ⁡ S → ⊥ ˙ ⁡ F ⁡ S ⊆ ⊥ ˙ ⁡ S
17 2 ocv2ss ⊢ ⊥ ˙ ⁡ F ⁡ S ⊆ ⊥ ˙ ⁡ S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ F ⁡ S
18 15 16 17 3syl ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ F ⁡ S
19 4 mrccl ⊢ C ∈ Moore ⁡ V ∧ S ⊆ V → F ⁡ S ∈ C
20 5 19 sylan ⊢ W ∈ PreHil ∧ S ⊆ V → F ⁡ S ∈ C
21 2 3 cssi ⊢ F ⁡ S ∈ C → F ⁡ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ F ⁡ S
22 20 21 syl ⊢ W ∈ PreHil ∧ S ⊆ V → F ⁡ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ F ⁡ S
23 18 22 sseqtrrd ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ F ⁡ S
24 13 23 eqssd ⊢ W ∈ PreHil ∧ S ⊆ V → F ⁡ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S