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

Metamath Proof Explorer

Theorem mrccss

Proof