Metamath Proof Explorer

Theorem bcsiHIL

Description: Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of Beran p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	bcs.1	⊢ 𝐴 ∈ ℋ
		bcs.2	⊢ 𝐵 ∈ ℋ
	Assertion	bcsiHIL	⊢ ( abs ‘ ( 𝐴 ·_ih 𝐵 ) ) ≤ ( ( norm_ℎ ‘ 𝐴 ) · ( norm_ℎ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bcs.1	⊢ 𝐴 ∈ ℋ
2		bcs.2	⊢ 𝐵 ∈ ℋ
3		df-hba	⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩ )
4		eqid	⊢ ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩ = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
5	4	hhnm	⊢ norm_ℎ = ( norm_CV ‘ ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩ )
6	4	hhip	⊢ ·_ih = ( ·_𝑖OLD ‘ ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩ )
7	4	hhph	⊢ ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩ ∈ CPreHil_OLD
8	3 5 6 7 1 2	siii	⊢ ( abs ‘ ( 𝐴 ·_ih 𝐵 ) ) ≤ ( ( norm_ℎ ‘ 𝐴 ) · ( norm_ℎ ‘ 𝐵 ) )