ipcau2

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau . (Contributed by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$⊢ G = toCPreHil (W)$
	tcphcph.v	$⊢ V = {Base}_{W}$
	tcphcph.f	$⊢ F = Scalar (W)$
	tcphcph.1	$⊢ φ \to W \in PreHil$
	tcphcph.2	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} K$
	tcphcph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	tcphcph.3	$⊢ (φ \land (x \in K \land x \in ℝ \land 0 \leq x)) \to \sqrt{x} \in K$
	tcphcph.4	$⊢ (φ \land x \in V) \to 0 \leq x \underset{˙}{,} x$
	tcphcph.k	$⊢ K = {Base}_{F}$
	ipcau2.n	$⊢ N = norm (G)$
	ipcau2.c	$⊢ C = \frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}$
	ipcau2.3	$⊢ φ \to X \in V$
	ipcau2.4	$⊢ φ \to Y \in V$
Assertion	ipcau2	$⊢ φ \to \|X \underset{˙}{,} Y\| \leq N (X) N (Y)$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$⊢ G = toCPreHil (W)$
2		tcphcph.v	$⊢ V = {Base}_{W}$
3		tcphcph.f	$⊢ F = Scalar (W)$
4		tcphcph.1	$⊢ φ \to W \in PreHil$
5		tcphcph.2	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} K$
6		tcphcph.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
7		tcphcph.3	$⊢ (φ \land (x \in K \land x \in ℝ \land 0 \leq x)) \to \sqrt{x} \in K$
8		tcphcph.4	$⊢ (φ \land x \in V) \to 0 \leq x \underset{˙}{,} x$
9		tcphcph.k	$⊢ K = {Base}_{F}$
10		ipcau2.n	$⊢ N = norm (G)$
11		ipcau2.c	$⊢ C = \frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}$
12		ipcau2.3	$⊢ φ \to X \in V$
13		ipcau2.4	$⊢ φ \to Y \in V$
14		oveq2	$⊢ Y = 0_{W} \to X \underset{˙}{,} Y = X \underset{˙}{,} 0_{W}$
15	14	oveq1d	$⊢ Y = 0_{W} \to (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) = (X \underset{˙}{,} 0_{W}) (Y \underset{˙}{,} X)$
16	15	breq1d	$⊢ Y = 0_{W} \to ((X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y) \leftrightarrow (X \underset{˙}{,} 0_{W}) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y))$
17	1 2 3 4 5	phclm	$⊢ φ \to W \in CMod$
18	3 9	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
19	17 18	syl	$⊢ φ \to K \subseteq ℂ$
20	3 6 2 9	ipcl	$⊢ (W \in PreHil \land X \in V \land Y \in V) \to X \underset{˙}{,} Y \in K$
21	4 12 13 20	syl3anc	$⊢ φ \to X \underset{˙}{,} Y \in K$
22	19 21	sseldd	$⊢ φ \to X \underset{˙}{,} Y \in ℂ$
23	22	adantr	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} Y \in ℂ$
24	3 6 2 9	ipcl	$⊢ (W \in PreHil \land Y \in V \land X \in V) \to Y \underset{˙}{,} X \in K$
25	4 13 12 24	syl3anc	$⊢ φ \to Y \underset{˙}{,} X \in K$
26	19 25	sseldd	$⊢ φ \to Y \underset{˙}{,} X \in ℂ$
27	26	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} X \in ℂ$
28	1 2 3 4 5 6	tcphcphlem3	$⊢ (φ \land Y \in V) \to Y \underset{˙}{,} Y \in ℝ$
29	13 28	mpdan	$⊢ φ \to Y \underset{˙}{,} Y \in ℝ$
30	29	recnd	$⊢ φ \to Y \underset{˙}{,} Y \in ℂ$
31	30	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} Y \in ℂ$
32	3	clm0	$⊢ W \in CMod \to 0 = 0_{F}$
33	17 32	syl	$⊢ φ \to 0 = 0_{F}$
34	33	eqeq2d	$⊢ φ \to (Y \underset{˙}{,} Y = 0 \leftrightarrow Y \underset{˙}{,} Y = 0_{F})$
35		eqid	$⊢ 0_{F} = 0_{F}$
36		eqid	$⊢ 0_{W} = 0_{W}$
37	3 6 2 35 36	ipeq0	$⊢ (W \in PreHil \land Y \in V) \to (Y \underset{˙}{,} Y = 0_{F} \leftrightarrow Y = 0_{W})$
38	4 13 37	syl2anc	$⊢ φ \to (Y \underset{˙}{,} Y = 0_{F} \leftrightarrow Y = 0_{W})$
39	34 38	bitrd	$⊢ φ \to (Y \underset{˙}{,} Y = 0 \leftrightarrow Y = 0_{W})$
40	39	necon3bid	$⊢ φ \to (Y \underset{˙}{,} Y \neq 0 \leftrightarrow Y \neq 0_{W})$
41	40	biimpar	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} Y \neq 0$
42	23 27 31 41	divassd	$⊢ (φ \land Y \neq 0_{W}) \to \frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} = (X \underset{˙}{,} Y) (\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y})$
43	11	oveq2i	$⊢ (X \underset{˙}{,} Y) C = (X \underset{˙}{,} Y) (\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y})$
44	42 43	eqtr4di	$⊢ (φ \land Y \neq 0_{W}) \to \frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} = (X \underset{˙}{,} Y) C$
45		oveq12	$⊢ (x = X -_{W} (\overline{C} \cdot_{W} Y) \land x = X -_{W} (\overline{C} \cdot_{W} Y)) \to x \underset{˙}{,} x = (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y))$
46	45	anidms	$⊢ x = X -_{W} (\overline{C} \cdot_{W} Y) \to x \underset{˙}{,} x = (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y))$
47	46	breq2d	$⊢ x = X -_{W} (\overline{C} \cdot_{W} Y) \to (0 \leq x \underset{˙}{,} x \leftrightarrow 0 \leq (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y)))$
48	8	ralrimiva	$⊢ φ \to \forall x \in V 0 \leq x \underset{˙}{,} x$
49	48	adantr	$⊢ (φ \land Y \neq 0_{W}) \to \forall x \in V 0 \leq x \underset{˙}{,} x$
50		phllmod	$⊢ W \in PreHil \to W \in LMod$
51	4 50	syl	$⊢ φ \to W \in LMod$
52	51	adantr	$⊢ (φ \land Y \neq 0_{W}) \to W \in LMod$
53	12	adantr	$⊢ (φ \land Y \neq 0_{W}) \to X \in V$
54	11	fveq2i	$⊢ \overline{C} = \overline{\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}}$
55	27 31 41	cjdivd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}} = \frac{\overline{Y \underset{˙}{,} X}}{\overline{Y \underset{˙}{,} Y}}$
56	54 55	syl5eq	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} = \frac{\overline{Y \underset{˙}{,} X}}{\overline{Y \underset{˙}{,} Y}}$
57	5	fveq2d	$⊢ φ \to _{F} = _{(ℂ_{fld} ↾_{𝑠} K)}$
58	9	fvexi	$⊢ K \in V$
59		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
60		cnfldcj	$⊢ * = *_{ℂ_{fld}}$
61	59 60	ressstarv	$⊢ K \in V \to * = *_{(ℂ_{fld} ↾_{𝑠} K)}$
62	58 61	ax-mp	$⊢ * = *_{(ℂ_{fld} ↾_{𝑠} K)}$
63	57 62	eqtr4di	$⊢ φ \to _{F} = $
64	63	fveq1d	$⊢ φ \to {(X \underset{˙}{,} Y)}^{*_{F}} = \overline{X \underset{˙}{,} Y}$
65		eqid	$⊢ _{F} = _{F}$
66	3 6 2 65	ipcj	$⊢ (W \in PreHil \land X \in V \land Y \in V) \to {(X \underset{˙}{,} Y)}^{*_{F}} = Y \underset{˙}{,} X$
67	4 12 13 66	syl3anc	$⊢ φ \to {(X \underset{˙}{,} Y)}^{*_{F}} = Y \underset{˙}{,} X$
68	64 67	eqtr3d	$⊢ φ \to \overline{X \underset{˙}{,} Y} = Y \underset{˙}{,} X$
69	68	adantr	$⊢ (φ \land Y \neq 0_{W}) \to \overline{X \underset{˙}{,} Y} = Y \underset{˙}{,} X$
70	69	fveq2d	$⊢ (φ \land Y \neq 0_{W}) \to \overline{\overline{X \underset{˙}{,} Y}} = \overline{Y \underset{˙}{,} X}$
71	23	cjcjd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{\overline{X \underset{˙}{,} Y}} = X \underset{˙}{,} Y$
72	70 71	eqtr3d	$⊢ (φ \land Y \neq 0_{W}) \to \overline{Y \underset{˙}{,} X} = X \underset{˙}{,} Y$
73	29	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} Y \in ℝ$
74	73	cjred	$⊢ (φ \land Y \neq 0_{W}) \to \overline{Y \underset{˙}{,} Y} = Y \underset{˙}{,} Y$
75	72 74	oveq12d	$⊢ (φ \land Y \neq 0_{W}) \to \frac{\overline{Y \underset{˙}{,} X}}{\overline{Y \underset{˙}{,} Y}} = \frac{X \underset{˙}{,} Y}{Y \underset{˙}{,} Y}$
76	23 31 41	divrecd	$⊢ (φ \land Y \neq 0_{W}) \to \frac{X \underset{˙}{,} Y}{Y \underset{˙}{,} Y} = (X \underset{˙}{,} Y) (\frac{1}{Y \underset{˙}{,} Y})$
77	56 75 76	3eqtrd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} = (X \underset{˙}{,} Y) (\frac{1}{Y \underset{˙}{,} Y})$
78	17	adantr	$⊢ (φ \land Y \neq 0_{W}) \to W \in CMod$
79	21	adantr	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} Y \in K$
80	3 6 2 9	ipcl	$⊢ (W \in PreHil \land Y \in V \land Y \in V) \to Y \underset{˙}{,} Y \in K$
81	4 13 13 80	syl3anc	$⊢ φ \to Y \underset{˙}{,} Y \in K$
82	81	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} Y \in K$
83	5	adantr	$⊢ (φ \land Y \neq 0_{W}) \to F = ℂ_{fld} ↾_{𝑠} K$
84		phllvec	$⊢ W \in PreHil \to W \in LVec$
85	4 84	syl	$⊢ φ \to W \in LVec$
86	3	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
87	85 86	syl	$⊢ φ \to F \in DivRing$
88	87	adantr	$⊢ (φ \land Y \neq 0_{W}) \to F \in DivRing$
89	9 83 88	cphreccllem	$⊢ ((φ \land Y \neq 0_{W}) \land Y \underset{˙}{,} Y \in K \land Y \underset{˙}{,} Y \neq 0) \to \frac{1}{Y \underset{˙}{,} Y} \in K$
90	82 41 89	mpd3an23	$⊢ (φ \land Y \neq 0_{W}) \to \frac{1}{Y \underset{˙}{,} Y} \in K$
91	3 9	clmmcl	$⊢ (W \in CMod \land X \underset{˙}{,} Y \in K \land \frac{1}{Y \underset{˙}{,} Y} \in K) \to (X \underset{˙}{,} Y) (\frac{1}{Y \underset{˙}{,} Y}) \in K$
92	78 79 90 91	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) (\frac{1}{Y \underset{˙}{,} Y}) \in K$
93	77 92	eqeltrd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} \in K$
94	13	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \in V$
95		eqid	$⊢ \cdot_{W} = \cdot_{W}$
96	2 3 95 9	lmodvscl	$⊢ (W \in LMod \land \overline{C} \in K \land Y \in V) \to \overline{C} \cdot_{W} Y \in V$
97	52 93 94 96	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} \cdot_{W} Y \in V$
98		eqid	$⊢ -_{W} = -_{W}$
99	2 98	lmodvsubcl	$⊢ (W \in LMod \land X \in V \land \overline{C} \cdot_{W} Y \in V) \to X -_{W} (\overline{C} \cdot_{W} Y) \in V$
100	52 53 97 99	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to X -_{W} (\overline{C} \cdot_{W} Y) \in V$
101	47 49 100	rspcdva	$⊢ (φ \land Y \neq 0_{W}) \to 0 \leq (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y))$
102		eqid	$⊢ -_{F} = -_{F}$
103		eqid	$⊢ +_{F} = +_{F}$
104	4	adantr	$⊢ (φ \land Y \neq 0_{W}) \to W \in PreHil$
105	3 6 2 98 102 103 104 53 97 53 97	ip2subdi	$⊢ (φ \land Y \neq 0_{W}) \to (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y)) = ((X \underset{˙}{,} X) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y))) -_{F} ((X \underset{˙}{,} (\overline{C} \cdot_{W} Y)) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} X))$
106	83	fveq2d	$⊢ (φ \land Y \neq 0_{W}) \to +_{F} = +_{(ℂ_{fld} ↾_{𝑠} K)}$
107		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
108	59 107	ressplusg	$⊢ K \in V \to + = +_{(ℂ_{fld} ↾_{𝑠} K)}$
109	58 108	ax-mp	$⊢ + = +_{(ℂ_{fld} ↾_{𝑠} K)}$
110	106 109	eqtr4di	$⊢ (φ \land Y \neq 0_{W}) \to +_{F} = +$
111		eqidd	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} X = X \underset{˙}{,} X$
112		eqid	$⊢ \cdot_{F} = \cdot_{F}$
113	3 6 2 9 95 112	ipass	$⊢ (W \in PreHil \land (\overline{C} \in K \land Y \in V \land \overline{C} \cdot_{W} Y \in V)) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y) = \overline{C} \cdot_{F} (Y \underset{˙}{,} (\overline{C} \cdot_{W} Y))$
114	104 93 94 97 113	syl13anc	$⊢ (φ \land Y \neq 0_{W}) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y) = \overline{C} \cdot_{F} (Y \underset{˙}{,} (\overline{C} \cdot_{W} Y))$
115	83	fveq2d	$⊢ (φ \land Y \neq 0_{W}) \to \cdot_{F} = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
116		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
117	59 116	ressmulr	$⊢ K \in V \to \times = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
118	58 117	ax-mp	$⊢ \times = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
119	115 118	eqtr4di	$⊢ (φ \land Y \neq 0_{W}) \to \cdot_{F} = \times$
120		eqidd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} = \overline{C}$
121	27 31 41	divrecd	$⊢ (φ \land Y \neq 0_{W}) \to \frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y} = (Y \underset{˙}{,} X) (\frac{1}{Y \underset{˙}{,} Y})$
122	11 121	syl5eq	$⊢ (φ \land Y \neq 0_{W}) \to C = (Y \underset{˙}{,} X) (\frac{1}{Y \underset{˙}{,} Y})$
123	25	adantr	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} X \in K$
124	3 9	clmmcl	$⊢ (W \in CMod \land Y \underset{˙}{,} X \in K \land \frac{1}{Y \underset{˙}{,} Y} \in K) \to (Y \underset{˙}{,} X) (\frac{1}{Y \underset{˙}{,} Y}) \in K$
125	78 123 90 124	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} X) (\frac{1}{Y \underset{˙}{,} Y}) \in K$
126	122 125	eqeltrd	$⊢ (φ \land Y \neq 0_{W}) \to C \in K$
127	3 6 2 9 95 112 65	ipassr2	$⊢ (W \in PreHil \land (Y \in V \land Y \in V \land C \in K)) \to (Y \underset{˙}{,} Y) \cdot_{F} C = Y \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y)$
128	104 94 94 126 127	syl13anc	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} Y) \cdot_{F} C = Y \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y)$
129	119	oveqd	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} Y) \cdot_{F} C = (Y \underset{˙}{,} Y) C$
130	11	oveq2i	$⊢ (Y \underset{˙}{,} Y) C = (Y \underset{˙}{,} Y) (\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y})$
131	27 31 41	divcan2d	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} Y) (\frac{Y \underset{˙}{,} X}{Y \underset{˙}{,} Y}) = Y \underset{˙}{,} X$
132	130 131	syl5eq	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} Y) C = Y \underset{˙}{,} X$
133	129 132	eqtrd	$⊢ (φ \land Y \neq 0_{W}) \to (Y \underset{˙}{,} Y) \cdot_{F} C = Y \underset{˙}{,} X$
134	63	adantr	$⊢ (φ \land Y \neq 0_{W}) \to _{F} = $
135	134	fveq1d	$⊢ (φ \land Y \neq 0_{W}) \to C^{*_{F}} = \overline{C}$
136	135	oveq1d	$⊢ (φ \land Y \neq 0_{W}) \to C^{*_{F}} \cdot_{W} Y = \overline{C} \cdot_{W} Y$
137	136	oveq2d	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y) = Y \underset{˙}{,} (\overline{C} \cdot_{W} Y)$
138	128 133 137	3eqtr3rd	$⊢ (φ \land Y \neq 0_{W}) \to Y \underset{˙}{,} (\overline{C} \cdot_{W} Y) = Y \underset{˙}{,} X$
139	119 120 138	oveq123d	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} \cdot_{F} (Y \underset{˙}{,} (\overline{C} \cdot_{W} Y)) = \overline{C} (Y \underset{˙}{,} X)$
140	114 139	eqtrd	$⊢ (φ \land Y \neq 0_{W}) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y) = \overline{C} (Y \underset{˙}{,} X)$
141	110 111 140	oveq123d	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} X) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y)) = (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X)$
142	3 6 2 9 95 112 65	ipassr2	$⊢ (W \in PreHil \land (X \in V \land Y \in V \land C \in K)) \to (X \underset{˙}{,} Y) \cdot_{F} C = X \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y)$
143	104 53 94 126 142	syl13anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) \cdot_{F} C = X \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y)$
144	119	oveqd	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) \cdot_{F} C = (X \underset{˙}{,} Y) C$
145	136	oveq2d	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} (C^{*_{F}} \cdot_{W} Y) = X \underset{˙}{,} (\overline{C} \cdot_{W} Y)$
146	143 144 145	3eqtr3rd	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} (\overline{C} \cdot_{W} Y) = (X \underset{˙}{,} Y) C$
147	3 6 2 9 95 112	ipass	$⊢ (W \in PreHil \land (\overline{C} \in K \land Y \in V \land X \in V)) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} X = \overline{C} \cdot_{F} (Y \underset{˙}{,} X)$
148	104 93 94 53 147	syl13anc	$⊢ (φ \land Y \neq 0_{W}) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} X = \overline{C} \cdot_{F} (Y \underset{˙}{,} X)$
149	119	oveqd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} \cdot_{F} (Y \underset{˙}{,} X) = \overline{C} (Y \underset{˙}{,} X)$
150	148 149	eqtrd	$⊢ (φ \land Y \neq 0_{W}) \to (\overline{C} \cdot_{W} Y) \underset{˙}{,} X = \overline{C} (Y \underset{˙}{,} X)$
151	110 146 150	oveq123d	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} (\overline{C} \cdot_{W} Y)) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} X) = (X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X)$
152	141 151	oveq12d	$⊢ (φ \land Y \neq 0_{W}) \to ((X \underset{˙}{,} X) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} (\overline{C} \cdot_{W} Y))) -_{F} ((X \underset{˙}{,} (\overline{C} \cdot_{W} Y)) +_{F} ((\overline{C} \cdot_{W} Y) \underset{˙}{,} X)) = ((X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X)) -_{F} ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X))$
153	3 6 2 9	ipcl	$⊢ (W \in PreHil \land X \in V \land X \in V) \to X \underset{˙}{,} X \in K$
154	104 53 53 153	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} X \in K$
155	3 9	clmmcl	$⊢ (W \in CMod \land \overline{C} \in K \land Y \underset{˙}{,} X \in K) \to \overline{C} (Y \underset{˙}{,} X) \in K$
156	78 93 123 155	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} (Y \underset{˙}{,} X) \in K$
157	3 9	clmacl	$⊢ (W \in CMod \land X \underset{˙}{,} X \in K \land \overline{C} (Y \underset{˙}{,} X) \in K) \to (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) \in K$
158	78 154 156 157	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) \in K$
159	3 9	clmmcl	$⊢ (W \in CMod \land X \underset{˙}{,} Y \in K \land C \in K) \to (X \underset{˙}{,} Y) C \in K$
160	78 79 126 159	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) C \in K$
161	3 9	clmacl	$⊢ (W \in CMod \land (X \underset{˙}{,} Y) C \in K \land \overline{C} (Y \underset{˙}{,} X) \in K) \to (X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X) \in K$
162	78 160 156 161	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X) \in K$
163	3 9	clmsub	$⊢ (W \in CMod \land (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) \in K \land (X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X) \in K) \to (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) - ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X)) = ((X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X)) -_{F} ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X))$
164	78 158 162 163	syl3anc	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) - ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X)) = ((X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X)) -_{F} ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X))$
165	1 2 3 4 5 6	tcphcphlem3	$⊢ (φ \land X \in V) \to X \underset{˙}{,} X \in ℝ$
166	12 165	mpdan	$⊢ φ \to X \underset{˙}{,} X \in ℝ$
167	166	recnd	$⊢ φ \to X \underset{˙}{,} X \in ℂ$
168	167	adantr	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} X \in ℂ$
169	22	absvalsqd	$⊢ φ \to {\|X \underset{˙}{,} Y\|}^{2} = (X \underset{˙}{,} Y) \overline{X \underset{˙}{,} Y}$
170	68	oveq2d	$⊢ φ \to (X \underset{˙}{,} Y) \overline{X \underset{˙}{,} Y} = (X \underset{˙}{,} Y) (Y \underset{˙}{,} X)$
171	169 170	eqtrd	$⊢ φ \to {\|X \underset{˙}{,} Y\|}^{2} = (X \underset{˙}{,} Y) (Y \underset{˙}{,} X)$
172	22	abscld	$⊢ φ \to \|X \underset{˙}{,} Y\| \in ℝ$
173	172	resqcld	$⊢ φ \to {\|X \underset{˙}{,} Y\|}^{2} \in ℝ$
174	171 173	eqeltrrd	$⊢ φ \to (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \in ℝ$
175	174	adantr	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \in ℝ$
176	175 73 41	redivcld	$⊢ (φ \land Y \neq 0_{W}) \to \frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} \in ℝ$
177	44 176	eqeltrrd	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) C \in ℝ$
178	177	recnd	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) C \in ℂ$
179	78 18	syl	$⊢ (φ \land Y \neq 0_{W}) \to K \subseteq ℂ$
180	179 156	sseldd	$⊢ (φ \land Y \neq 0_{W}) \to \overline{C} (Y \underset{˙}{,} X) \in ℂ$
181	168 178 180	pnpcan2d	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X) - ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X)) = (X \underset{˙}{,} X) - (X \underset{˙}{,} Y) C$
182	164 181	eqtr3d	$⊢ (φ \land Y \neq 0_{W}) \to ((X \underset{˙}{,} X) + \overline{C} (Y \underset{˙}{,} X)) -_{F} ((X \underset{˙}{,} Y) C + \overline{C} (Y \underset{˙}{,} X)) = (X \underset{˙}{,} X) - (X \underset{˙}{,} Y) C$
183	105 152 182	3eqtrd	$⊢ (φ \land Y \neq 0_{W}) \to (X -_{W} (\overline{C} \cdot_{W} Y)) \underset{˙}{,} (X -_{W} (\overline{C} \cdot_{W} Y)) = (X \underset{˙}{,} X) - (X \underset{˙}{,} Y) C$
184	101 183	breqtrd	$⊢ (φ \land Y \neq 0_{W}) \to 0 \leq (X \underset{˙}{,} X) - (X \underset{˙}{,} Y) C$
185	166	adantr	$⊢ (φ \land Y \neq 0_{W}) \to X \underset{˙}{,} X \in ℝ$
186	185 177	subge0d	$⊢ (φ \land Y \neq 0_{W}) \to (0 \leq (X \underset{˙}{,} X) - (X \underset{˙}{,} Y) C \leftrightarrow (X \underset{˙}{,} Y) C \leq X \underset{˙}{,} X)$
187	184 186	mpbid	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) C \leq X \underset{˙}{,} X$
188	44 187	eqbrtrd	$⊢ (φ \land Y \neq 0_{W}) \to \frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} \leq X \underset{˙}{,} X$
189		oveq12	$⊢ (x = Y \land x = Y) \to x \underset{˙}{,} x = Y \underset{˙}{,} Y$
190	189	anidms	$⊢ x = Y \to x \underset{˙}{,} x = Y \underset{˙}{,} Y$
191	190	breq2d	$⊢ x = Y \to (0 \leq x \underset{˙}{,} x \leftrightarrow 0 \leq Y \underset{˙}{,} Y)$
192	191 48 13	rspcdva	$⊢ φ \to 0 \leq Y \underset{˙}{,} Y$
193	192	adantr	$⊢ (φ \land Y \neq 0_{W}) \to 0 \leq Y \underset{˙}{,} Y$
194	73 193 41	ne0gt0d	$⊢ (φ \land Y \neq 0_{W}) \to 0 < Y \underset{˙}{,} Y$
195		ledivmul2	$⊢ ((X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \in ℝ \land X \underset{˙}{,} X \in ℝ \land (Y \underset{˙}{,} Y \in ℝ \land 0 < Y \underset{˙}{,} Y)) \to (\frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} \leq X \underset{˙}{,} X \leftrightarrow (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y))$
196	175 185 73 194 195	syl112anc	$⊢ (φ \land Y \neq 0_{W}) \to (\frac{(X \underset{˙}{,} Y) (Y \underset{˙}{,} X)}{Y \underset{˙}{,} Y} \leq X \underset{˙}{,} X \leftrightarrow (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y))$
197	188 196	mpbid	$⊢ (φ \land Y \neq 0_{W}) \to (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
198	3 6 2 35 36	ip0r	$⊢ (W \in PreHil \land X \in V) \to X \underset{˙}{,} 0_{W} = 0_{F}$
199	4 12 198	syl2anc	$⊢ φ \to X \underset{˙}{,} 0_{W} = 0_{F}$
200	199 33	eqtr4d	$⊢ φ \to X \underset{˙}{,} 0_{W} = 0$
201	200	oveq1d	$⊢ φ \to (X \underset{˙}{,} 0_{W}) (Y \underset{˙}{,} X) = 0 \cdot (Y \underset{˙}{,} X)$
202	26	mul02d	$⊢ φ \to 0 \cdot (Y \underset{˙}{,} X) = 0$
203	201 202	eqtrd	$⊢ φ \to (X \underset{˙}{,} 0_{W}) (Y \underset{˙}{,} X) = 0$
204		oveq12	$⊢ (x = X \land x = X) \to x \underset{˙}{,} x = X \underset{˙}{,} X$
205	204	anidms	$⊢ x = X \to x \underset{˙}{,} x = X \underset{˙}{,} X$
206	205	breq2d	$⊢ x = X \to (0 \leq x \underset{˙}{,} x \leftrightarrow 0 \leq X \underset{˙}{,} X)$
207	206 48 12	rspcdva	$⊢ φ \to 0 \leq X \underset{˙}{,} X$
208	166 29 207 192	mulge0d	$⊢ φ \to 0 \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
209	203 208	eqbrtrd	$⊢ φ \to (X \underset{˙}{,} 0_{W}) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
210	16 197 209	pm2.61ne	$⊢ φ \to (X \underset{˙}{,} Y) (Y \underset{˙}{,} X) \leq (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
211	166 207	resqrtcld	$⊢ φ \to \sqrt{X \underset{˙}{,} X} \in ℝ$
212	211	recnd	$⊢ φ \to \sqrt{X \underset{˙}{,} X} \in ℂ$
213	29 192	resqrtcld	$⊢ φ \to \sqrt{Y \underset{˙}{,} Y} \in ℝ$
214	213	recnd	$⊢ φ \to \sqrt{Y \underset{˙}{,} Y} \in ℂ$
215	212 214	sqmuld	$⊢ φ \to {\sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}}^{2} = {\sqrt{X \underset{˙}{,} X}}^{2} {\sqrt{Y \underset{˙}{,} Y}}^{2}$
216	167	sqsqrtd	$⊢ φ \to {\sqrt{X \underset{˙}{,} X}}^{2} = X \underset{˙}{,} X$
217	30	sqsqrtd	$⊢ φ \to {\sqrt{Y \underset{˙}{,} Y}}^{2} = Y \underset{˙}{,} Y$
218	216 217	oveq12d	$⊢ φ \to {\sqrt{X \underset{˙}{,} X}}^{2} {\sqrt{Y \underset{˙}{,} Y}}^{2} = (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
219	215 218	eqtrd	$⊢ φ \to {\sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}}^{2} = (X \underset{˙}{,} X) (Y \underset{˙}{,} Y)$
220	210 171 219	3brtr4d	$⊢ φ \to {\|X \underset{˙}{,} Y\|}^{2} \leq {\sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}}^{2}$
221	211 213	remulcld	$⊢ φ \to \sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y} \in ℝ$
222	22	absge0d	$⊢ φ \to 0 \leq \|X \underset{˙}{,} Y\|$
223	166 207	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{X \underset{˙}{,} X}$
224	29 192	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{Y \underset{˙}{,} Y}$
225	211 213 223 224	mulge0d	$⊢ φ \to 0 \leq \sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}$
226	172 221 222 225	le2sqd	$⊢ φ \to (\|X \underset{˙}{,} Y\| \leq \sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y} \leftrightarrow {\|X \underset{˙}{,} Y\|}^{2} \leq {\sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}}^{2})$
227	220 226	mpbird	$⊢ φ \to \|X \underset{˙}{,} Y\| \leq \sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}$
228		lmodgrp	$⊢ W \in LMod \to W \in Grp$
229	51 228	syl	$⊢ φ \to W \in Grp$
230	1 10 2 6	tcphnmval	$⊢ (W \in Grp \land X \in V) \to N (X) = \sqrt{X \underset{˙}{,} X}$
231	229 12 230	syl2anc	$⊢ φ \to N (X) = \sqrt{X \underset{˙}{,} X}$
232	1 10 2 6	tcphnmval	$⊢ (W \in Grp \land Y \in V) \to N (Y) = \sqrt{Y \underset{˙}{,} Y}$
233	229 13 232	syl2anc	$⊢ φ \to N (Y) = \sqrt{Y \underset{˙}{,} Y}$
234	231 233	oveq12d	$⊢ φ \to N (X) N (Y) = \sqrt{X \underset{˙}{,} X} \sqrt{Y \underset{˙}{,} Y}$
235	227 234	breqtrrd	$⊢ φ \to \|X \underset{˙}{,} Y\| \leq N (X) N (Y)$

Metamath Proof Explorer

Theorem ipcau2

Proof