Metamath Proof Explorer

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 [,) +∞ ) ) ) ⊆ 𝐾 ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )