Metamath Proof Explorer

Theorem siilem2

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

Ref Expression
Hypotheses siii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
siii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
siii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
siii.9 ⊢ 𝑈 ∈ CPreHilOLD
siii.a ⊢ 𝐴 ∈ 𝑋
siii.b ⊢ 𝐵 ∈ 𝑋
siii2.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
siii2.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
Assertion siilem2 ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 siii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 siii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
3 siii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 siii.9 ⊢ 𝑈 ∈ CPreHilOLD
5 siii.a ⊢ 𝐴 ∈ 𝑋
6 siii.b ⊢ 𝐵 ∈ 𝑋
7 siii2.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
8 siii2.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
9 oveq1 ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
10 9 eqeq2d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ↔ ( 𝐵 𝑃 𝐴 ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
11 9 oveq2d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 𝐴 𝑃 𝐵 ) · ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
12 11 fveq2d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) )
13 12 breq1d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ↔ ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )
14 10 13 imbi12d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) ↔ ( ( 𝐵 𝑃 𝐴 ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) ) )
15 eleq1 ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 𝐶 ∈ ℂ ↔ if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ ) )
16 oveq1 ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) )
17 16 eleq1d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ↔ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ) )
18 16 breq2d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ↔ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
19 15 17 18 3anbi123d ⊢ ( 𝐶 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ ∧ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
20 eleq1 ⊢ ( 0 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 0 ∈ ℂ ↔ if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ ) )
21 oveq1 ⊢ ( 0 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 0 · ( 𝐴 𝑃 𝐵 ) ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) )
22 21 eleq1d ⊢ ( 0 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 0 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ↔ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ) )
23 21 breq2d ⊢ ( 0 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( 0 ≤ ( 0 · ( 𝐴 𝑃 𝐵 ) ) ↔ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ) )
24 20 22 23 3anbi123d ⊢ ( 0 = if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) → ( ( 0 ∈ ℂ ∧ ( 0 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 0 · ( 𝐴 𝑃 𝐵 ) ) ) ↔ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ ∧ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ) ) )
25 0cn ⊢ 0 ∈ ℂ
26 4 phnvi ⊢ 𝑈 ∈ NrmCVec
27 1 3 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
28 26 5 6 27 mp3an ⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
29 28 mul02i ⊢ ( 0 · ( 𝐴 𝑃 𝐵 ) ) = 0
30 0re ⊢ 0 ∈ ℝ
31 29 30 eqeltri ⊢ ( 0 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ
32 0le0 ⊢ 0 ≤ 0
33 32 29 breqtrri ⊢ 0 ≤ ( 0 · ( 𝐴 𝑃 𝐵 ) )
34 25 31 33 3pm3.2i ⊢ ( 0 ∈ ℂ ∧ ( 0 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 0 · ( 𝐴 𝑃 𝐵 ) ) )
35 19 24 34 elimhyp ⊢ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ ∧ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) )
36 35 simp1i ⊢ if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) ∈ ℂ
37 35 simp2i ⊢ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ
38 35 simp3i ⊢ 0 ≤ ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( 𝐴 𝑃 𝐵 ) )
39 1 2 3 4 5 6 7 8 36 37 38 siilem1 ⊢ ( ( 𝐵 𝑃 𝐴 ) = ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( if ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) , 𝐶 , 0 ) · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
40 14 39 dedth ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) → ( ( 𝐵 𝑃 𝐴 ) = ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) → ( √ ‘ ( ( 𝐴 𝑃 𝐵 ) · ( 𝐶 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ) )