Metamath Proof Explorer

Theorem 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 ⊢X=BaseSet⁡U
sii.6 ⊢N=normCV⁡U
sii.7 ⊢P=⋅𝑖OLD⁡U
sii.9 ⊢U∈CPreHilOLD
Assertion sii ⊢A∈X∧B∈X→APB≤N⁡A⁢N⁡B

Proof

Step Hyp Ref Expression
1 sii.1 ⊢X=BaseSet⁡U
2 sii.6 ⊢N=normCV⁡U
3 sii.7 ⊢P=⋅𝑖OLD⁡U
4 sii.9 ⊢U∈CPreHilOLD
5 fvoveq1 ⊢A=ifA∈XA0vec⁡U→APB=ifA∈XA0vec⁡UPB
6 fveq2 ⊢A=ifA∈XA0vec⁡U→N⁡A=N⁡ifA∈XA0vec⁡U
7 6 oveq1d ⊢A=ifA∈XA0vec⁡U→N⁡A⁢N⁡B=N⁡ifA∈XA0vec⁡U⁢N⁡B
8 5 7 breq12d ⊢A=ifA∈XA0vec⁡U→APB≤N⁡A⁢N⁡B↔ifA∈XA0vec⁡UPB≤N⁡ifA∈XA0vec⁡U⁢N⁡B
9 oveq2 ⊢B=ifB∈XB0vec⁡U→ifA∈XA0vec⁡UPB=ifA∈XA0vec⁡UPifB∈XB0vec⁡U
10 9 fveq2d ⊢B=ifB∈XB0vec⁡U→ifA∈XA0vec⁡UPB=ifA∈XA0vec⁡UPifB∈XB0vec⁡U
11 fveq2 ⊢B=ifB∈XB0vec⁡U→N⁡B=N⁡ifB∈XB0vec⁡U
12 11 oveq2d ⊢B=ifB∈XB0vec⁡U→N⁡ifA∈XA0vec⁡U⁢N⁡B=N⁡ifA∈XA0vec⁡U⁢N⁡ifB∈XB0vec⁡U
13 10 12 breq12d ⊢B=ifB∈XB0vec⁡U→ifA∈XA0vec⁡UPB≤N⁡ifA∈XA0vec⁡U⁢N⁡B↔ifA∈XA0vec⁡UPifB∈XB0vec⁡U≤N⁡ifA∈XA0vec⁡U⁢N⁡ifB∈XB0vec⁡U
14 eqid ⊢0vec⁡U=0vec⁡U
15 1 14 4 elimph ⊢ifA∈XA0vec⁡U∈X
16 1 14 4 elimph ⊢ifB∈XB0vec⁡U∈X
17 1 2 3 4 15 16 siii ⊢ifA∈XA0vec⁡UPifB∈XB0vec⁡U≤N⁡ifA∈XA0vec⁡U⁢N⁡ifB∈XB0vec⁡U
18 8 13 17 dedth2h ⊢A∈X∧B∈X→APB≤N⁡A⁢N⁡B