cncph

Description: The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007) (Revised by Mario Carneiro, 7-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	cncph.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
	Assertion	cncph	$⊢ U \in {CPreHil}_{OLD}$

Proof

Step	Hyp	Ref	Expression
1		cncph.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2		eqid	$⊢ ⟨⟨+ \times⟩, abs⟩ = ⟨⟨+ \times⟩, abs⟩$
3	2	cnnv	$⊢ ⟨⟨+ \times⟩, abs⟩ \in NrmCVec$
4		mulm1	$⊢ y \in ℂ \to -1 y = - y$
5	4	adantl	$⊢ (x \in ℂ \land y \in ℂ) \to -1 y = - y$
6	5	oveq2d	$⊢ (x \in ℂ \land y \in ℂ) \to x + -1 y = x + (- y)$
7		negsub	$⊢ (x \in ℂ \land y \in ℂ) \to x + (- y) = x - y$
8	6 7	eqtrd	$⊢ (x \in ℂ \land y \in ℂ) \to x + -1 y = x - y$
9	8	fveq2d	$⊢ (x \in ℂ \land y \in ℂ) \to \|x + -1 y\| = \|x - y\|$
10	9	oveq1d	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + -1 y\|}^{2} = {\|x - y\|}^{2}$
11	10	oveq2d	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} + {\|x + -1 y\|}^{2} = {\|x + y\|}^{2} + {\|x - y\|}^{2}$
12		sqabsadd	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} = {\|x\|}^{2} + {\|y\|}^{2} + 2 ℜ (x \overline{y})$
13		sqabssub	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x - y\|}^{2} = {\|x\|}^{2} + {\|y\|}^{2} - 2 ℜ (x \overline{y})$
14	12 13	oveq12d	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} + {\|x - y\|}^{2} = ({\|x\|}^{2} + {\|y\|}^{2}) + 2 ℜ (x \overline{y}) + ({\|x\|}^{2} + {\|y\|}^{2} - 2 ℜ (x \overline{y}))$
15		abscl	$⊢ x \in ℂ \to \|x\| \in ℝ$
16	15	recnd	$⊢ x \in ℂ \to \|x\| \in ℂ$
17	16	sqcld	$⊢ x \in ℂ \to {\|x\|}^{2} \in ℂ$
18		abscl	$⊢ y \in ℂ \to \|y\| \in ℝ$
19	18	recnd	$⊢ y \in ℂ \to \|y\| \in ℂ$
20	19	sqcld	$⊢ y \in ℂ \to {\|y\|}^{2} \in ℂ$
21		addcl	$⊢ ({\|x\|}^{2} \in ℂ \land {\|y\|}^{2} \in ℂ) \to {\|x\|}^{2} + {\|y\|}^{2} \in ℂ$
22	17 20 21	syl2an	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x\|}^{2} + {\|y\|}^{2} \in ℂ$
23		2cn	$⊢ 2 \in ℂ$
24		cjcl	$⊢ y \in ℂ \to \overline{y} \in ℂ$
25		mulcl	$⊢ (x \in ℂ \land \overline{y} \in ℂ) \to x \overline{y} \in ℂ$
26	24 25	sylan2	$⊢ (x \in ℂ \land y \in ℂ) \to x \overline{y} \in ℂ$
27		recl	$⊢ x \overline{y} \in ℂ \to ℜ (x \overline{y}) \in ℝ$
28	27	recnd	$⊢ x \overline{y} \in ℂ \to ℜ (x \overline{y}) \in ℂ$
29	26 28	syl	$⊢ (x \in ℂ \land y \in ℂ) \to ℜ (x \overline{y}) \in ℂ$
30		mulcl	$⊢ (2 \in ℂ \land ℜ (x \overline{y}) \in ℂ) \to 2 ℜ (x \overline{y}) \in ℂ$
31	23 29 30	sylancr	$⊢ (x \in ℂ \land y \in ℂ) \to 2 ℜ (x \overline{y}) \in ℂ$
32	22 31 22	ppncand	$⊢ (x \in ℂ \land y \in ℂ) \to ({\|x\|}^{2} + {\|y\|}^{2}) + 2 ℜ (x \overline{y}) + ({\|x\|}^{2} + {\|y\|}^{2} - 2 ℜ (x \overline{y})) = {\|x\|}^{2} + {\|y\|}^{2} + {\|x\|}^{2} + {\|y\|}^{2}$
33	14 32	eqtrd	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} + {\|x - y\|}^{2} = {\|x\|}^{2} + {\|y\|}^{2} + {\|x\|}^{2} + {\|y\|}^{2}$
34		2times	$⊢ {\|x\|}^{2} + {\|y\|}^{2} \in ℂ \to 2 ({\|x\|}^{2} + {\|y\|}^{2}) = {\|x\|}^{2} + {\|y\|}^{2} + {\|x\|}^{2} + {\|y\|}^{2}$
35	34	eqcomd	$⊢ {\|x\|}^{2} + {\|y\|}^{2} \in ℂ \to {\|x\|}^{2} + {\|y\|}^{2} + {\|x\|}^{2} + {\|y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})$
36	22 35	syl	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x\|}^{2} + {\|y\|}^{2} + {\|x\|}^{2} + {\|y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})$
37	33 36	eqtrd	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} + {\|x - y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})$
38	11 37	eqtrd	$⊢ (x \in ℂ \land y \in ℂ) \to {\|x + y\|}^{2} + {\|x + -1 y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})$
39	38	rgen2	$⊢ \forall x \in ℂ \forall y \in ℂ {\|x + y\|}^{2} + {\|x + -1 y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})$
40		addex	$⊢ + \in V$
41		mulex	$⊢ \times \in V$
42		absf	$⊢ abs : ℂ ⟶ ℝ$
43		cnex	$⊢ ℂ \in V$
44		fex	$⊢ (abs : ℂ ⟶ ℝ \land ℂ \in V) \to abs \in V$
45	42 43 44	mp2an	$⊢ abs \in V$
46		cnaddabloOLD	$⊢ + \in AbelOp$
47		ablogrpo	$⊢ + \in AbelOp \to + \in GrpOp$
48	46 47	ax-mp	$⊢ + \in GrpOp$
49		ax-addf	$⊢ + : ℂ \times ℂ ⟶ ℂ$
50	49	fdmi	$⊢ dom + = ℂ \times ℂ$
51	48 50	grporn	$⊢ ℂ = ran +$
52	51	isphg	$⊢ (+ \in V \land \times \in V \land abs \in V) \to (⟨⟨+ \times⟩, abs⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨+ \times⟩, abs⟩ \in NrmCVec \land \forall x \in ℂ \forall y \in ℂ {\|x + y\|}^{2} + {\|x + -1 y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2})))$
53	40 41 45 52	mp3an	$⊢ ⟨⟨+ \times⟩, abs⟩ \in {CPreHil}_{OLD} \leftrightarrow (⟨⟨+ \times⟩, abs⟩ \in NrmCVec \land \forall x \in ℂ \forall y \in ℂ {\|x + y\|}^{2} + {\|x + -1 y\|}^{2} = 2 ({\|x\|}^{2} + {\|y\|}^{2}))$
54	3 39 53	mpbir2an	$⊢ ⟨⟨+ \times⟩, abs⟩ \in {CPreHil}_{OLD}$
55	1 54	eqeltri	$⊢ U \in {CPreHil}_{OLD}$

Metamath Proof Explorer

Theorem cncph

Proof