sii

Description: Obsolete version of ipcau as of 22-Sep-2024. 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 . (Contributed by NM, 12-Jan-2008) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem sii

Proof