cssincl

Description: The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Hypothesis	css0.c	$⊢ C = ClSubSp (W)$
	Assertion	cssincl	$⊢ (W \in PreHil \land A \in C \land B \in C) \to A \cap B \in C$

Step	Hyp	Ref	Expression
1		css0.c	$⊢ C = ClSubSp (W)$
2		eqid	$⊢ {Base}_{W} = {Base}_{W}$
3		eqid	$⊢ ocv (W) = ocv (W)$
4	2 3	ocvss	$⊢ ocv (W) (A) \subseteq {Base}_{W}$
5	2 3	ocvss	$⊢ ocv (W) (B) \subseteq {Base}_{W}$
6	4 5	unssi	$⊢ ocv (W) (A) \cup ocv (W) (B) \subseteq {Base}_{W}$
7	2 1 3	ocvcss	$⊢ (W \in PreHil \land ocv (W) (A) \cup ocv (W) (B) \subseteq {Base}_{W}) \to ocv (W) (ocv (W) (A) \cup ocv (W) (B)) \in C$
8	6 7	mpan2	$⊢ W \in PreHil \to ocv (W) (ocv (W) (A) \cup ocv (W) (B)) \in C$
9	3 1	cssi	$⊢ A \in C \to A = ocv (W) (ocv (W) (A))$
10	3 1	cssi	$⊢ B \in C \to B = ocv (W) (ocv (W) (B))$
11	9 10	ineqan12d	$⊢ (A \in C \land B \in C) \to A \cap B = ocv (W) (ocv (W) (A)) \cap ocv (W) (ocv (W) (B))$
12	3	unocv	$⊢ ocv (W) (ocv (W) (A) \cup ocv (W) (B)) = ocv (W) (ocv (W) (A)) \cap ocv (W) (ocv (W) (B))$
13	11 12	eqtr4di	$⊢ (A \in C \land B \in C) \to A \cap B = ocv (W) (ocv (W) (A) \cup ocv (W) (B))$
14	13	eleq1d	$⊢ (A \in C \land B \in C) \to (A \cap B \in C \leftrightarrow ocv (W) (ocv (W) (A) \cup ocv (W) (B)) \in C)$
15	8 14	syl5ibrcom	$⊢ W \in PreHil \to ((A \in C \land B \in C) \to A \cap B \in C)$
16	15	3impib	$⊢ (W \in PreHil \land A \in C \land B \in C) \to A \cap B \in C$

Metamath Proof Explorer