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	|- X = ( BaseSet ` U )
	sii.6	|- N = ( normCV ` U )
	sii.7	|- P = ( .iOLD ` U )
	sii.9	|- U e. CPreHilOLD
Assertion	sii	|- ( ( A e. X /\ B e. X ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sii.1	|- X = ( BaseSet ` U )
2		sii.6	|- N = ( normCV ` U )
3		sii.7	|- P = ( .iOLD ` U )
4		sii.9	|- U e. CPreHilOLD
5		fvoveq1	|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( abs ` ( A P B ) ) = ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) )
6		fveq2	|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( N ` A ) = ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) )
7	6	oveq1d	|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( N ` A ) x. ( N ` B ) ) = ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) )
8	5 7	breq12d	|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) <-> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) ) )
9		oveq2	|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( if ( A e. X , A , ( 0vec ` U ) ) P B ) = ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) )
10	9	fveq2d	|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) = ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) )
11		fveq2	|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( N ` B ) = ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) )
12	11	oveq2d	|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) = ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) ) )
13	10 12	breq12d	|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P B ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` B ) ) <-> ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) ) ) )
14		eqid	|- ( 0vec ` U ) = ( 0vec ` U )
15	1 14 4	elimph	|- if ( A e. X , A , ( 0vec ` U ) ) e. X
16	1 14 4	elimph	|- if ( B e. X , B , ( 0vec ` U ) ) e. X
17	1 2 3 4 15 16	siii	|- ( abs ` ( if ( A e. X , A , ( 0vec ` U ) ) P if ( B e. X , B , ( 0vec ` U ) ) ) ) <_ ( ( N ` if ( A e. X , A , ( 0vec ` U ) ) ) x. ( N ` if ( B e. X , B , ( 0vec ` U ) ) ) )
18	8 13 17	dedth2h	|- ( ( A e. X /\ B e. X ) -> ( abs ` ( A P B ) ) <_ ( ( N ` A ) x. ( N ` B ) ) )