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	⊢ 𝐻 ∈ Cℋ
	pjhth.2	⊢ ( 𝜑 → 𝐴 ∈ ℋ )
Assertion	pjhthlem2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		pjhth.1	⊢ 𝐻 ∈ Cℋ
2		pjhth.2	⊢ ( 𝜑 → 𝐴 ∈ ℋ )
3	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → 𝐴 ∈ ℋ )
4	1	cheli	⊢ ( 𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ )
5	4	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → 𝑥 ∈ ℋ )
6		hvsubcl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐴 −ℎ 𝑥 ) ∈ ℋ )
7	3 5 6	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → ( 𝐴 −ℎ 𝑥 ) ∈ ℋ )
8	3	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) ∧ 𝑦 ∈ 𝐻 ) → 𝐴 ∈ ℋ )
9		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) ∧ 𝑦 ∈ 𝐻 ) → 𝑥 ∈ 𝐻 )
10		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) ∧ 𝑦 ∈ 𝐻 ) → 𝑦 ∈ 𝐻 )
11		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) ∧ 𝑦 ∈ 𝐻 ) → ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) )
12		eqid	⊢ ( ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) / ( ( 𝑦 ·ih 𝑦 ) + 1 ) ) = ( ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) / ( ( 𝑦 ·ih 𝑦 ) + 1 ) )
13	1 8 9 10 11 12	pjhthlem1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) ∧ 𝑦 ∈ 𝐻 ) → ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) = 0 )
14	13	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → ∀ 𝑦 ∈ 𝐻 ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) = 0 )
15	1	chshii	⊢ 𝐻 ∈ Sℋ
16		shocel	⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐴 −ℎ 𝑥 ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( 𝐴 −ℎ 𝑥 ) ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐻 ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) = 0 ) ) )
17	15 16	ax-mp	⊢ ( ( 𝐴 −ℎ 𝑥 ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( 𝐴 −ℎ 𝑥 ) ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐻 ( ( 𝐴 −ℎ 𝑥 ) ·ih 𝑦 ) = 0 ) )
18	7 14 17	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → ( 𝐴 −ℎ 𝑥 ) ∈ ( ⊥ ‘ 𝐻 ) )
19		hvpncan3	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑥 +ℎ ( 𝐴 −ℎ 𝑥 ) ) = 𝐴 )
20	5 3 19	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → ( 𝑥 +ℎ ( 𝐴 −ℎ 𝑥 ) ) = 𝐴 )
21	20	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → 𝐴 = ( 𝑥 +ℎ ( 𝐴 −ℎ 𝑥 ) ) )
22		oveq2	⊢ ( 𝑦 = ( 𝐴 −ℎ 𝑥 ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑥 +ℎ ( 𝐴 −ℎ 𝑥 ) ) )
23	22	rspceeqv	⊢ ( ( ( 𝐴 −ℎ 𝑥 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 = ( 𝑥 +ℎ ( 𝐴 −ℎ 𝑥 ) ) ) → ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
24	18 21 23	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
25		df-hba	⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
26		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
27	26	hhvs	⊢ −ℎ = ( −𝑣 ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
28	26	hhnm	⊢ normℎ = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
29		eqid	⊢ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
30	29 15	hhssba	⊢ 𝐻 = ( BaseSet ‘ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ )
31	26	hhph	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ CPreHilOLD
32	31	a1i	⊢ ( 𝜑 → ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ CPreHilOLD )
33	26 29	hhsst	⊢ ( 𝐻 ∈ Sℋ → ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) )
34	15 33	ax-mp	⊢ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
35	29 1	hhssbnOLD	⊢ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ CBan
36		elin	⊢ ( ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∩ CBan ) ↔ ( ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∧ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ CBan ) )
37	34 35 36	mpbir2an	⊢ ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∩ CBan )
38	37	a1i	⊢ ( 𝜑 → ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ ∈ ( ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∩ CBan ) )
39	25 27 28 30 32 38 2	minveco	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) )
40		reurex	⊢ ( ∃! 𝑥 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) )
41	39 40	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐻 ∀ 𝑧 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑧 ) ) )
42	24 41	reximddv	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )