Metamath Proof Explorer

Theorem siilem2

Description: Lemma for sii . (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses siii.1 ⊢ X = BaseSet ⁡ U
siii.6 ⊢ N = norm CV ⁡ U
siii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
siii.9 ⊢ U ∈ CPreHil OLD
siii.a ⊢ A ∈ X
siii.b ⊢ B ∈ X
siii2.3 ⊢ M = - v ⁡ U
siii2.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion siilem2 ⊢ C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B → B P A = C ⁢ N ⁡ B 2 → A P B ⁢ C ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B

Proof

Step Hyp Ref Expression
1 siii.1 ⊢ X = BaseSet ⁡ U
2 siii.6 ⊢ N = norm CV ⁡ U
3 siii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 siii.9 ⊢ U ∈ CPreHil OLD
5 siii.a ⊢ A ∈ X
6 siii.b ⊢ B ∈ X
7 siii2.3 ⊢ M = - v ⁡ U
8 siii2.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
9 oveq1 ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → C ⁢ N ⁡ B 2 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2
10 9 eqeq2d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → B P A = C ⁢ N ⁡ B 2 ↔ B P A = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2
11 9 oveq2d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → A P B ⁢ C ⁢ N ⁡ B 2 = A P B ⁢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2
12 11 fveq2d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → A P B ⁢ C ⁢ N ⁡ B 2 = A P B ⁢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2
13 12 breq1d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → A P B ⁢ C ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B ↔ A P B ⁢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B
14 10 13 imbi12d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → B P A = C ⁢ N ⁡ B 2 → A P B ⁢ C ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B ↔ B P A = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2 → A P B ⁢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B
15 eleq1 ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → C ∈ ℂ ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ
16 oveq1 ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → C ⁢ A P B = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
17 16 eleq1d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → C ⁢ A P B ∈ ℝ ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ
18 16 breq2d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ≤ C ⁢ A P B ↔ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
19 15 17 18 3anbi123d ⊢ C = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ ∧ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ ∧ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
20 eleq1 ⊢ 0 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ∈ ℂ ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ
21 oveq1 ⊢ 0 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ⋅ A P B = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
22 21 eleq1d ⊢ 0 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ⋅ A P B ∈ ℝ ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ
23 21 breq2d ⊢ 0 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ≤ 0 ⋅ A P B ↔ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
24 20 22 23 3anbi123d ⊢ 0 = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 → 0 ∈ ℂ ∧ 0 ⋅ A P B ∈ ℝ ∧ 0 ≤ 0 ⋅ A P B ↔ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ ∧ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ ∧ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
25 0cn ⊢ 0 ∈ ℂ
26 4 phnvi ⊢ U ∈ NrmCVec
27 1 3 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ∈ ℂ
28 26 5 6 27 mp3an ⊢ A P B ∈ ℂ
29 28 mul02i ⊢ 0 ⋅ A P B = 0
30 0re ⊢ 0 ∈ ℝ
31 29 30 eqeltri ⊢ 0 ⋅ A P B ∈ ℝ
32 0le0 ⊢ 0 ≤ 0
33 32 29 breqtrri ⊢ 0 ≤ 0 ⋅ A P B
34 25 31 33 3pm3.2i ⊢ 0 ∈ ℂ ∧ 0 ⋅ A P B ∈ ℝ ∧ 0 ≤ 0 ⋅ A P B
35 19 24 34 elimhyp ⊢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ ∧ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ ∧ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
36 35 simp1i ⊢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ∈ ℂ
37 35 simp2i ⊢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B ∈ ℝ
38 35 simp3i ⊢ 0 ≤ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ A P B
39 1 2 3 4 5 6 7 8 36 37 38 siilem1 ⊢ B P A = if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2 → A P B ⁢ if C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B C 0 ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B
40 14 39 dedth ⊢ C ∈ ℂ ∧ C ⁢ A P B ∈ ℝ ∧ 0 ≤ C ⁢ A P B → B P A = C ⁢ N ⁡ B 2 → A P B ⁢ C ⁢ N ⁡ B 2 ≤ N ⁡ A ⁢ N ⁡ B