Metamath Proof Explorer

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 ∈ C ℋ
pjhth.2 ⊢ φ → A ∈ ℋ
Assertion pjhthlem2 ⊢ φ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y

Proof

Step Hyp Ref Expression
1 pjhth.1 ⊢ H ∈ C ℋ
2 pjhth.2 ⊢ φ → A ∈ ℋ
3 2 adantr ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → A ∈ ℋ
4 1 cheli ⊢ x ∈ H → x ∈ ℋ
5 4 ad2antrl ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → x ∈ ℋ
6 hvsubcl ⊢ A ∈ ℋ ∧ x ∈ ℋ → A - ℎ x ∈ ℋ
7 3 5 6 syl2anc ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → A - ℎ x ∈ ℋ
8 3 adantr ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z ∧ y ∈ H → A ∈ ℋ
9 simplrl ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z ∧ y ∈ H → x ∈ H
10 simpr ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z ∧ y ∈ H → y ∈ H
11 simplrr ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z ∧ y ∈ H → ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z
12 eqid ⊢ A - ℎ x ⋅ ih y y ⋅ ih y + 1 = A - ℎ x ⋅ ih y y ⋅ ih y + 1
13 1 8 9 10 11 12 pjhthlem1 ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z ∧ y ∈ H → A - ℎ x ⋅ ih y = 0
14 13 ralrimiva ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → ∀ y ∈ H A - ℎ x ⋅ ih y = 0
15 1 chshii ⊢ H ∈ S ℋ
16 shocel ⊢ H ∈ S ℋ → A - ℎ x ∈ ⊥ ⁡ H ↔ A - ℎ x ∈ ℋ ∧ ∀ y ∈ H A - ℎ x ⋅ ih y = 0
17 15 16 ax-mp ⊢ A - ℎ x ∈ ⊥ ⁡ H ↔ A - ℎ x ∈ ℋ ∧ ∀ y ∈ H A - ℎ x ⋅ ih y = 0
18 7 14 17 sylanbrc ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → A - ℎ x ∈ ⊥ ⁡ H
19 hvpncan3 ⊢ x ∈ ℋ ∧ A ∈ ℋ → x + ℎ A - ℎ x = A
20 5 3 19 syl2anc ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → x + ℎ A - ℎ x = A
21 20 eqcomd ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → A = x + ℎ A - ℎ x
22 oveq2 ⊢ y = A - ℎ x → x + ℎ y = x + ℎ A - ℎ x
23 22 rspceeqv ⊢ A - ℎ x ∈ ⊥ ⁡ H ∧ A = x + ℎ A - ℎ x → ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
24 18 21 23 syl2anc ⊢ φ ∧ x ∈ H ∧ ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
25 df-hba ⊢ ℋ = BaseSet ⁡ + ℎ ⋅ ℎ norm ℎ
26 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
27 26 hhvs ⊢ - ℎ = - v ⁡ + ℎ ⋅ ℎ norm ℎ
28 26 hhnm ⊢ norm ℎ = norm CV ⁡ + ℎ ⋅ ℎ norm ℎ
29 eqid ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H = + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
30 29 15 hhssba ⊢ H = BaseSet ⁡ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H
31 26 hhph ⊢ + ℎ ⋅ ℎ norm ℎ ∈ CPreHil OLD
32 31 a1i ⊢ φ → + ℎ ⋅ ℎ norm ℎ ∈ CPreHil OLD
33 26 29 hhsst ⊢ H ∈ S ℋ → + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
34 15 33 ax-mp ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ
35 29 1 hhssbnOLD ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ CBan
36 elin ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ ∩ CBan ↔ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ ∧ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ CBan
37 34 35 36 mpbir2an ⊢ + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ ∩ CBan
38 37 a1i ⊢ φ → + ℎ ↾ H × H ⋅ ℎ ↾ ℂ × H norm ℎ ↾ H ∈ SubSp ⁡ + ℎ ⋅ ℎ norm ℎ ∩ CBan
39 25 27 28 30 32 38 2 minveco ⊢ φ → ∃! x ∈ H ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z
40 reurex ⊢ ∃! x ∈ H ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z → ∃ x ∈ H ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z
41 39 40 syl ⊢ φ → ∃ x ∈ H ∀ z ∈ H norm ℎ ⁡ A - ℎ x ≤ norm ℎ ⁡ A - ℎ z
42 24 41 reximddv ⊢ φ → ∃ x ∈ H ∃ y ∈ ⊥ ⁡ H A = x + ℎ y