Theorem pjhthlem2

Description: Lemma for pjhth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjhth.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjhth.2	$$⊢\phi \to A\in \mathscr{H}$$
Assertion	pjhthlem2	$$⊢\phi \to \exists x\in H\exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$

Proof

Step	Hyp	Ref	Expression
1		pjhth.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjhth.2	$$⊢\phi \to A\in \mathscr{H}$$
3	2	adantr	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to A\in \mathscr{H}$$
4	1	cheli	$$⊢x\in H\to x\in \mathscr{H}$$
5	4	ad2antrl	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to x\in \mathscr{H}$$
6		hvsubcl	$$⊢\left(A\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to A{-}_{ℎ}x\in \mathscr{H}$$
7	3 5 6	syl2anc	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to A{-}_{ℎ}x\in \mathscr{H}$$
8	3	adantr	$$⊢\left(\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\wedge y\in H\right)\to A\in \mathscr{H}$$
9		simplrl	$$⊢\left(\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\wedge y\in H\right)\to x\in H$$
10		simpr	$$⊢\left(\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\wedge y\in H\right)\to y\in H$$
11		simplrr	$$⊢\left(\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\wedge y\in H\right)\to \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)$$
12		eqid	$$⊢\frac{\left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y}{\left(y{\cdot }_{\mathrm{ih}}y\right)+1}=\frac{\left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y}{\left(y{\cdot }_{\mathrm{ih}}y\right)+1}$$
13	1 8 9 10 11 12	pjhthlem1	$$⊢\left(\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\wedge y\in H\right)\to \left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y=0$$
14	13	ralrimiva	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to \forall y\in H\left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y=0$$
15	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
16		shocel	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(A{-}_{ℎ}x\in \perp \left(H\right)\leftrightarrow \left(A{-}_{ℎ}x\in \mathscr{H}\wedge \forall y\in H\left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y=0\right)\right)$$
17	15 16	ax-mp	$$⊢A{-}_{ℎ}x\in \perp \left(H\right)\leftrightarrow \left(A{-}_{ℎ}x\in \mathscr{H}\wedge \forall y\in H\left(A{-}_{ℎ}x\right){\cdot }_{\mathrm{ih}}y=0\right)$$
18	7 14 17	sylanbrc	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to A{-}_{ℎ}x\in \perp \left(H\right)$$
19		hvpncan3	$$⊢\left(x\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to x{+}_{ℎ}\left(A{-}_{ℎ}x\right)=A$$
20	5 3 19	syl2anc	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to x{+}_{ℎ}\left(A{-}_{ℎ}x\right)=A$$
21	20	eqcomd	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to A=x{+}_{ℎ}\left(A{-}_{ℎ}x\right)$$
22		oveq2	$$⊢y=A{-}_{ℎ}x\to x{+}_{ℎ}y=x{+}_{ℎ}\left(A{-}_{ℎ}x\right)$$
23	22	rspceeqv	$$⊢\left(A{-}_{ℎ}x\in \perp \left(H\right)\wedge A=x{+}_{ℎ}\left(A{-}_{ℎ}x\right)\right)\to \exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$
24	18 21 23	syl2anc	$$⊢\left(\phi \wedge \left(x\in H\wedge \forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\right)\right)\to \exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$
25		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
26		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
27	26	hhvs	$$⊢{-}_{ℎ}={-}_v\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
28	26	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
29		eqid	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
30	29 15	hhssba	$$⊢H=\mathrm{BaseSet}\left(⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\right)$$
31	26	hhph	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in {CPreHil}_{\mathrm{OLD}}$$
32	31	a1i	$$⊢\phi \to ⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in {CPreHil}_{\mathrm{OLD}}$$
33	26 29	hhsst	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to ⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
34	15 33	ax-mp	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
35	29 1	hhssbnOLD	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \mathrm{CBan}$$
36		elin	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \left(\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\cap \mathrm{CBan}\right)\leftrightarrow \left(⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\wedge ⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \mathrm{CBan}\right)$$
37	34 35 36	mpbir2an	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \left(\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\cap \mathrm{CBan}\right)$$
38	37	a1i	$$⊢\phi \to ⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩\in \left(\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\cap \mathrm{CBan}\right)$$
39	25 27 28 30 32 38 2	minveco	$$⊢\phi \to \exists !x\in H\forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)$$
40		reurex	$$⊢\exists !x\in H\forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)\to \exists x\in H\forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)$$
41	39 40	syl	$$⊢\phi \to \exists x\in H\forall z\in H{norm}_{ℎ}\left(A{-}_{ℎ}x\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}z\right)$$
42	24 41	reximddv	$$⊢\phi \to \exists x\in H\exists y\in \perp \left(H\right)A=x{+}_{ℎ}y$$