Theorem iscph

Description: A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	iscph.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	iscph.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	iscph.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	iscph.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	iscph.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	iscph	⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscph.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		iscph.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		iscph.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
4		iscph.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		iscph.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		elin	⊢ ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ↔ ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ) )
7	6	anbi1i	⊢ ( ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
8		df-3an	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
9	7 8	bitr4i	⊢ ( ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ↔ ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
10	9	anbi1i	⊢ ( ( ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) )
11		fvexd	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) ∈ V )
12		fvexd	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) ∈ V )
13		simplr	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑓 = ( Scalar ‘ 𝑤 ) )
14		simpll	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑤 = 𝑊 )
15	14	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
16	15 4	eqtr4di	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Scalar ‘ 𝑤 ) = 𝐹 )
17	13 16	eqtrd	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑓 = 𝐹 )
18		simpr	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑘 = ( Base ‘ 𝑓 ) )
19	17	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
20	19 5	eqtr4di	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Base ‘ 𝑓 ) = 𝐾 )
21	18 20	eqtrd	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑘 = 𝐾 )
22	21	oveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ℂfld ↾s 𝑘 ) = ( ℂfld ↾s 𝐾 ) )
23	17 22	eqeq12d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑓 = ( ℂfld ↾s 𝑘 ) ↔ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
24	21	ineq1d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑘 ∩ ( 0 [,) +∞ ) ) = ( 𝐾 ∩ ( 0 [,) +∞ ) ) )
25	24	imaeq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) = ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) )
26	25 21	sseq12d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ↔ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ) )
27	14	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( norm ‘ 𝑤 ) = ( norm ‘ 𝑊 ) )
28	27 3	eqtr4di	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( norm ‘ 𝑤 ) = 𝑁 )
29	14	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
30	29 1	eqtr4di	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( Base ‘ 𝑤 ) = 𝑉 )
31	14	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ·𝑖 ‘ 𝑤 ) = ( ·𝑖 ‘ 𝑊 ) )
32	31 2	eqtr4di	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ·𝑖 ‘ 𝑤 ) = , )
33	32	oveqd	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) = ( 𝑥 , 𝑥 ) )
34	33	fveq2d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) = ( √ ‘ ( 𝑥 , 𝑥 ) ) )
35	30 34	mpteq12dv	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
36	28 35	eqeq12d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ↔ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )
37	23 26 36	3anbi123d	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) )
38		3anass	⊢ ( ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) )
39	37 38	bitrdi	⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ) )
40	12 39	sbcied	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ) )
41	11 40	sbcied	⊢ ( 𝑤 = 𝑊 → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ) )
42		df-cph	⊢ ℂPreHil = { 𝑤 ∈ ( PreHil ∩ NrmMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) }
43	41 42	elrab2	⊢ ( 𝑊 ∈ ℂPreHil ↔ ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ) )
44		anass	⊢ ( ( ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ↔ ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) ) )
45	43 44	bitr4i	⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ ( PreHil ∩ NrmMod ) ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) )
46		3anass	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) ) )
47	10 45 46	3bitr4i	⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )