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 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐹 ‘ 𝑆 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )