pjth

Description: Projection Theorem: Any Hilbert space vector A can be decomposed uniquely into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of Beran p. 102 (existence part). (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 14-May-2014)

	Ref	Expression
Hypotheses	pjth.v	$⊢ V = {Base}_{W}$
	pjth.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	pjth.o	$⊢ O = ocv (W)$
	pjth.j	$⊢ J = TopOpen (W)$
	pjth.l	$⊢ L = LSubSp (W)$
Assertion	pjth	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \underset{˙}{\oplus} O (U) = V$

Proof

Step	Hyp	Ref	Expression
1		pjth.v	$⊢ V = {Base}_{W}$
2		pjth.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		pjth.o	$⊢ O = ocv (W)$
4		pjth.j	$⊢ J = TopOpen (W)$
5		pjth.l	$⊢ L = LSubSp (W)$
6		hlphl	$⊢ W \in ℂHil \to W \in PreHil$
7	6	3ad2ant1	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to W \in PreHil$
8		phllmod	$⊢ W \in PreHil \to W \in LMod$
9	7 8	syl	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to W \in LMod$
10		simp2	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \in L$
11	1 5	lssss	$⊢ U \in L \to U \subseteq V$
12	11	3ad2ant2	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \subseteq V$
13	1 3 5	ocvlss	$⊢ (W \in PreHil \land U \subseteq V) \to O (U) \in L$
14	7 12 13	syl2anc	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to O (U) \in L$
15	5 2	lsmcl	$⊢ (W \in LMod \land U \in L \land O (U) \in L) \to U \underset{˙}{\oplus} O (U) \in L$
16	9 10 14 15	syl3anc	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \underset{˙}{\oplus} O (U) \in L$
17	1 5	lssss	$⊢ U \underset{˙}{\oplus} O (U) \in L \to U \underset{˙}{\oplus} O (U) \subseteq V$
18	16 17	syl	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \underset{˙}{\oplus} O (U) \subseteq V$
19		eqid	$⊢ norm (W) = norm (W)$
20		eqid	$⊢ +_{W} = +_{W}$
21		eqid	$⊢ -_{W} = -_{W}$
22		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
23		simpl1	$⊢ ((W \in ℂHil \land U \in L \land U \in Clsd (J)) \land x \in V) \to W \in ℂHil$
24		simpl2	$⊢ ((W \in ℂHil \land U \in L \land U \in Clsd (J)) \land x \in V) \to U \in L$
25		simpr	$⊢ ((W \in ℂHil \land U \in L \land U \in Clsd (J)) \land x \in V) \to x \in V$
26		simpl3	$⊢ ((W \in ℂHil \land U \in L \land U \in Clsd (J)) \land x \in V) \to U \in Clsd (J)$
27	1 19 20 21 22 5 23 24 25 4 2 3 26	pjthlem2	$⊢ ((W \in ℂHil \land U \in L \land U \in Clsd (J)) \land x \in V) \to x \in (U \underset{˙}{\oplus} O (U))$
28	18 27	eqelssd	$⊢ (W \in ℂHil \land U \in L \land U \in Clsd (J)) \to U \underset{˙}{\oplus} O (U) = V$

Metamath Proof Explorer

Theorem pjth

Proof