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	$⊢ \underset{˙}{⊥} = ocv (W)$
	mrccss.c	$⊢ C = ClSubSp (W)$
	mrccss.f	$⊢ F = mrCls (C)$
Assertion	mrccss	$⊢ (W \in PreHil \land S \subseteq V) \to F (S) = \underset{˙}{⊥} (\underset{˙}{⊥} (S))$

Proof

Step	Hyp	Ref	Expression
1		mrccss.v	$⊢ V = {Base}_{W}$
2		mrccss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3		mrccss.c	$⊢ C = ClSubSp (W)$
4		mrccss.f	$⊢ F = mrCls (C)$
5	1 3	cssmre	$⊢ W \in PreHil \to C \in Moore (V)$
6	5	adantr	$⊢ (W \in PreHil \land S \subseteq V) \to C \in Moore (V)$
7	1 2	ocvocv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
8	1 2	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
9	8	a1i	$⊢ S \subseteq V \to \underset{˙}{⊥} (S) \subseteq V$
10	1 3 2	ocvcss	$⊢ (W \in PreHil \land \underset{˙}{⊥} (S) \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in C$
11	9 10	sylan2	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in C$
12	4	mrcsscl	$⊢ (C \in Moore (V) \land S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \land \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in C) \to F (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
13	6 7 11 12	syl3anc	$⊢ (W \in PreHil \land S \subseteq V) \to F (S) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
14	4	mrcssid	$⊢ (C \in Moore (V) \land S \subseteq V) \to S \subseteq F (S)$
15	5 14	sylan	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq F (S)$
16	2	ocv2ss	$⊢ S \subseteq F (S) \to \underset{˙}{⊥} (F (S)) \subseteq \underset{˙}{⊥} (S)$
17	2	ocv2ss	$⊢ \underset{˙}{⊥} (F (S)) \subseteq \underset{˙}{⊥} (S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (F (S)))$
18	15 16 17	3syl	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (F (S)))$
19	4	mrccl	$⊢ (C \in Moore (V) \land S \subseteq V) \to F (S) \in C$
20	5 19	sylan	$⊢ (W \in PreHil \land S \subseteq V) \to F (S) \in C$
21	2 3	cssi	$⊢ F (S) \in C \to F (S) = \underset{˙}{⊥} (\underset{˙}{⊥} (F (S)))$
22	20 21	syl	$⊢ (W \in PreHil \land S \subseteq V) \to F (S) = \underset{˙}{⊥} (\underset{˙}{⊥} (F (S)))$
23	18 22	sseqtrrd	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq F (S)$
24	13 23	eqssd	$⊢ (W \in PreHil \land S \subseteq V) \to F (S) = \underset{˙}{⊥} (\underset{˙}{⊥} (S))$

Metamath Proof Explorer

Theorem mrccss

Proof