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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( normℎ ‘ 𝐵 ) ≤ 1 ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( normℎ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		abshicom	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) = ( abs ‘ ( 𝐵 ·ih 𝐴 ) ) )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( normℎ ‘ 𝐵 ) ≤ 1 ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) = ( abs ‘ ( 𝐵 ·ih 𝐴 ) ) )
3		bcs2	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ∧ ( normℎ ‘ 𝐵 ) ≤ 1 ) → ( abs ‘ ( 𝐵 ·ih 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) )
4	3	3com12	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( normℎ ‘ 𝐵 ) ≤ 1 ) → ( abs ‘ ( 𝐵 ·ih 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 ) )
5	2 4	eqbrtrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( normℎ ‘ 𝐵 ) ≤ 1 ) → ( abs ‘ ( 𝐴 ·ih 𝐵 ) ) ≤ ( normℎ ‘ 𝐴 ) )