Theorem hhph

Description: The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hhph	⊢ 𝑈 ∈ CPreHilOLD

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3	2	hhnv	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
4		normpar	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
5		hvsubval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
6	5	fveq2d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) )
7	6	oveq1d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) = ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) )
8	7	oveq2d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) )
9		hvaddcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
10		normcl	⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℝ )
11	9 10	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℝ )
12	11	recnd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ℂ )
13	12	sqcld	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ∈ ℂ )
14		hvsubcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 −ℎ 𝑦 ) ∈ ℋ )
15		normcl	⊢ ( ( 𝑥 −ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℝ )
16	15	recnd	⊢ ( ( 𝑥 −ℎ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℂ )
17	14 16	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ∈ ℂ )
18	17	sqcld	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ∈ ℂ )
19	13 18	addcomd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) )
20	8 19	eqtr3d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( 𝑥 −ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) ) )
21		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
22	21	recnd	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℂ )
23	22	sqcld	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
24		normcl	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
25	24	recnd	⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℂ )
26	25	sqcld	⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ )
27		2cn	⊢ 2 ∈ ℂ
28		adddi	⊢ ( ( 2 ∈ ℂ ∧ ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ∧ ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
29	27 28	mp3an1	⊢ ( ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ∧ ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
30	23 26 29	syl2an	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) = ( ( 2 · ( ( normℎ ‘ 𝑥 ) ↑ 2 ) ) + ( 2 · ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
31	4 20 30	3eqtr4d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) )
32	31	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) )
33		hilablo	⊢ +ℎ ∈ AbelOp
34	33	elexi	⊢ +ℎ ∈ V
35		hvmulex	⊢ ·ℎ ∈ V
36		normf	⊢ normℎ : ℋ ⟶ ℝ
37		ax-hilex	⊢ ℋ ∈ V
38		fex	⊢ ( ( normℎ : ℋ ⟶ ℝ ∧ ℋ ∈ V ) → normℎ ∈ V )
39	36 37 38	mp2an	⊢ normℎ ∈ V
40	1	eleq1i	⊢ ( 𝑈 ∈ CPreHilOLD ↔ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ CPreHilOLD )
41		ablogrpo	⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp )
42	33 41	ax-mp	⊢ +ℎ ∈ GrpOp
43		ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
44	43	fdmi	⊢ dom +ℎ = ( ℋ × ℋ )
45	42 44	grporn	⊢ ℋ = ran +ℎ
46	45	isphg	⊢ ( ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) → ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
47	40 46	bitrid	⊢ ( ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) → ( 𝑈 ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) ) )
48	34 35 39 47	mp3an	⊢ ( 𝑈 ∈ CPreHilOLD ↔ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ↑ 2 ) + ( ( normℎ ‘ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( normℎ ‘ 𝑥 ) ↑ 2 ) + ( ( normℎ ‘ 𝑦 ) ↑ 2 ) ) ) ) )
49	3 32 48	mpbir2an	⊢ 𝑈 ∈ CPreHilOLD