Metamath Proof Explorer

Theorem bcs3

Description: Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL . (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bcs3 ⊢A∈ℋ∧B∈ℋ∧normℎ⁡B≤1→A⋅ihB≤normℎ⁡A

Proof

Step Hyp Ref Expression
1 abshicom ⊢A∈ℋ∧B∈ℋ→A⋅ihB=B⋅ihA
2 1 3adant3 ⊢A∈ℋ∧B∈ℋ∧normℎ⁡B≤1→A⋅ihB=B⋅ihA
3 bcs2 ⊢B∈ℋ∧A∈ℋ∧normℎ⁡B≤1→B⋅ihA≤normℎ⁡A
4 3 3com12 ⊢A∈ℋ∧B∈ℋ∧normℎ⁡B≤1→B⋅ihA≤normℎ⁡A
5 2 4 eqbrtrd ⊢A∈ℋ∧B∈ℋ∧normℎ⁡B≤1→A⋅ihB≤normℎ⁡A