This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 ∈ 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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )