ipcau

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of Kreyszig p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	ipcau.v	$⊢ V = {Base}_{W}$
	ipcau.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	ipcau.n	$⊢ N = norm (W)$
Assertion	ipcau	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to \|X \underset{˙}{,} Y\| \leq N (X) N (Y)$

Proof

Step	Hyp	Ref	Expression
1		ipcau.v	$⊢ V = {Base}_{W}$
2		ipcau.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		ipcau.n	$⊢ N = norm (W)$
4		eqid	$⊢ toCPreHil (W) = toCPreHil (W)$
5		eqid	$⊢ Scalar (W) = Scalar (W)$
6		simp1	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to W \in CPreHil$
7		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
8	6 7	syl	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to W \in PreHil$
9		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
10	5 9	cphsca	$⊢ W \in CPreHil \to Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)}$
11	6 10	syl	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to Scalar (W) = ℂ_{fld} ↾_{𝑠} {Base}_{Scalar (W)}$
12	5 9	cphsqrtcl	$⊢ (W \in CPreHil \land (x \in {Base}_{Scalar (W)} \land x \in ℝ \land 0 \leq x)) \to \sqrt{x} \in {Base}_{Scalar (W)}$
13	6 12	sylan	$⊢ ((W \in CPreHil \land X \in V \land Y \in V) \land (x \in {Base}_{Scalar (W)} \land x \in ℝ \land 0 \leq x)) \to \sqrt{x} \in {Base}_{Scalar (W)}$
14	1 2	ipge0	$⊢ (W \in CPreHil \land x \in V) \to 0 \leq x \underset{˙}{,} x$
15	6 14	sylan	$⊢ ((W \in CPreHil \land X \in V \land Y \in V) \land x \in V) \to 0 \leq x \underset{˙}{,} x$
16		eqid	$⊢ norm (toCPreHil (W)) = norm (toCPreHil (W))$
17		eqid	$⊢ \frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y} = \frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}$
18		simp2	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to X \in V$
19		simp3	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to Y \in V$
20	4 1 5 8 11 2 13 15 9 16 17 18 19	ipcau2	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to \|X \underset{˙}{,} Y\| \leq norm (toCPreHil (W)) (X) norm (toCPreHil (W)) (Y)$
21	4 3	cphtcphnm	$⊢ W \in CPreHil \to N = norm (toCPreHil (W))$
22	6 21	syl	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to N = norm (toCPreHil (W))$
23	22	fveq1d	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to N (X) = norm (toCPreHil (W)) (X)$
24	22	fveq1d	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to N (Y) = norm (toCPreHil (W)) (Y)$
25	23 24	oveq12d	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to N (X) N (Y) = norm (toCPreHil (W)) (X) norm (toCPreHil (W)) (Y)$
26	20 25	breqtrrd	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to \|X \underset{˙}{,} Y\| \leq N (X) N (Y)$

Metamath Proof Explorer

Theorem ipcau

Proof