Metamath Proof Explorer

Theorem pjth2

Description: Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015)

		Ref	Expression
	Hypotheses	pjth2.j	$⊢ J = TopOpen (W)$
		pjth2.l	$⊢ L = LSubSp (W)$
		pjth2.k	$⊢ K = proj (W)$
	Assertion	pjth2	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \in dom K$

Proof

Step	Hyp	Ref	Expression
1		pjth2.j	$⊢ J = TopOpen (W)$
2		pjth2.l	$⊢ L = LSubSp (W)$
3		pjth2.k	$⊢ K = proj (W)$
4		simp2	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \in L$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6		eqid	$⊢ LSSum (W) = LSSum (W)$
7		eqid	$⊢ ocv (W) = ocv (W)$
8	5 6 7 1 2	pjth	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U LSSum (W) ocv (W) (U) = {Base}_{W}$
9		hlphl	$⊢ W \in ℂHil \to W \in PreHil$
10	9	3ad2ant1	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to W \in PreHil$
11	5 2 7 6 3	pjdm2	$⊢ W \in PreHil \to (U \in dom K \leftrightarrow (U \in L \land U LSSum (W) ocv (W) (U) = {Base}_{W}))$
12	10 11	syl	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to (U \in dom K \leftrightarrow (U \in L \land U LSSum (W) ocv (W) (U) = {Base}_{W}))$
13	4 8 12	mpbir2and	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \in dom K$