pjcss

Description: A projection subspace is an (algebraically) closed subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Step	Hyp	Ref	Expression
1		pjcss.k	$⊢ K = proj (W)$
2		pjcss.c	$⊢ C = ClSubSp (W)$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4		eqid	$⊢ ocv (W) = ocv (W)$
5		eqid	$⊢ LSSum (W) = LSSum (W)$
6		simpl	$⊢ (W \in PreHil \land x \in dom K) \to W \in PreHil$
7		eqid	$⊢ LSubSp (W) = LSubSp (W)$
8	3 7 4 5 1	pjdm2	$⊢ W \in PreHil \to (x \in dom K \leftrightarrow (x \in LSubSp (W) \land x LSSum (W) ocv (W) (x) = {Base}_{W}))$
9	8	simprbda	$⊢ (W \in PreHil \land x \in dom K) \to x \in LSubSp (W)$
10	3 7	lssss	$⊢ x \in LSubSp (W) \to x \subseteq {Base}_{W}$
11	9 10	syl	$⊢ (W \in PreHil \land x \in dom K) \to x \subseteq {Base}_{W}$
12	3 4	ocvss	$⊢ ocv (W) (ocv (W) (x)) \subseteq {Base}_{W}$
13	8	simplbda	$⊢ (W \in PreHil \land x \in dom K) \to x LSSum (W) ocv (W) (x) = {Base}_{W}$
14	12 13	sseqtrrid	$⊢ (W \in PreHil \land x \in dom K) \to ocv (W) (ocv (W) (x)) \subseteq x LSSum (W) ocv (W) (x)$
15	2 3 4 5 6 11 14	lsmcss	$⊢ (W \in PreHil \land x \in dom K) \to x \in C$
16	15	ex	$⊢ W \in PreHil \to (x \in dom K \to x \in C)$
17	16	ssrdv	$⊢ W \in PreHil \to dom K \subseteq C$

Metamath Proof Explorer