Metamath Proof Explorer

Theorem sii

Description: Schwarz inequality. Part of Lemma 3-2.1(a) of Kreyszig p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also theorems bcseqi , bcsiALT , bcsiHIL , csbren . This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
sii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
sii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
sii.9 ⊢ 𝑈 ∈ CPreHilOLD
Assertion sii ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sii.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 sii.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
3 sii.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 sii.9 ⊢ 𝑈 ∈ CPreHilOLD
5 fvoveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) = ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐵 ) ) )
6 fveq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝐴 ) = ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) )
7 6 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) = ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ 𝐵 ) ) )
8 5 7 breq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) ↔ ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ 𝐵 ) ) ) )
9 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐵 ) = ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) )
10 9 fveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐵 ) ) = ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) ) )
11 fveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) )
12 11 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ 𝐵 ) ) = ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) ) )
13 10 12 breq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ 𝐵 ) ) ↔ ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) ) ≤ ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) ) ) )
14 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
15 1 14 4 elimph ⊢ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
16 1 14 4 elimph ⊢ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
17 1 2 3 4 15 16 siii ⊢ ( abs ‘ ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) ) ≤ ( ( 𝑁 ‘ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ) · ( 𝑁 ‘ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) )
18 8 13 17 dedth2h ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( abs ‘ ( 𝐴 𝑃 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )