Metamath Proof Explorer

Theorem tcphcph

Description: The standard definition of a norm turns any pre-Hilbert space over a subfield of CCfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphcph.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
tcphcph.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
tcphcph.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
tcphcph.2 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
tcphcph.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
tcphcph.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ 𝐾 )
tcphcph.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
Assertion tcphcph ( 𝜑 → 𝐺 ∈ ℂPreHil )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphcph.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 tcphcph.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 tcphcph.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
5 tcphcph.2 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
6 tcphcph.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
7 tcphcph.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ 𝐾 )
8 tcphcph.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
9 1 tcphphl ⊢ ( 𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil )
10 4 9 sylib ⊢ ( 𝜑 → 𝐺 ∈ PreHil )
11 1 2 6 tcphval ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
12 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
13 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
14 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
15 4 14 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
16 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
17 15 16 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
18 1 2 3 4 5 6 tcphcphlem3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 , 𝑥 ) ∈ ℝ )
19 18 8 resqrtcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ ℝ )
20 19 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) : 𝑉 ⟶ ℝ )
21 oveq12 ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 , 𝑥 ) = ( 𝑦 , 𝑦 ) )
22 21 anidms ⊢ ( 𝑥 = 𝑦 → ( 𝑥 , 𝑥 ) = ( 𝑦 , 𝑦 ) )
23 22 fveq2d ⊢ ( 𝑥 = 𝑦 → ( √ ‘ ( 𝑥 , 𝑥 ) ) = ( √ ‘ ( 𝑦 , 𝑦 ) ) )
24 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) )
25 fvex ⊢ ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ V
26 23 24 25 fvmpt3i ⊢ ( 𝑦 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) = ( √ ‘ ( 𝑦 , 𝑦 ) ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) = ( √ ‘ ( 𝑦 , 𝑦 ) ) )
28 27 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) = 0 ↔ ( √ ‘ ( 𝑦 , 𝑦 ) ) = 0 ) )
29 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
30 phllvec ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )
31 4 30 syl ⊢ ( 𝜑 → 𝑊 ∈ LVec )
32 3 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
33 31 32 syl ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
34 29 5 33 cphsubrglem ⊢ ( 𝜑 → ( 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) = ( 𝐾 ∩ ℂ ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) ) )
35 34 simp2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( 𝐾 ∩ ℂ ) )
36 inss2 ⊢ ( 𝐾 ∩ ℂ ) ⊆ ℂ
37 35 36 eqsstrdi ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ⊆ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( Base ‘ 𝐹 ) ⊆ ℂ )
39 3 6 2 29 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑦 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 , 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
40 39 3anidm23 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 , 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
41 4 40 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 , 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
42 38 41 sseldd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 , 𝑦 ) ∈ ℂ )
43 42 sqrtcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( √ ‘ ( 𝑦 , 𝑦 ) ) ∈ ℂ )
44 sqeq0 ⊢ ( ( √ ‘ ( 𝑦 , 𝑦 ) ) ∈ ℂ → ( ( ( √ ‘ ( 𝑦 , 𝑦 ) ) ↑ 2 ) = 0 ↔ ( √ ‘ ( 𝑦 , 𝑦 ) ) = 0 ) )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( √ ‘ ( 𝑦 , 𝑦 ) ) ↑ 2 ) = 0 ↔ ( √ ‘ ( 𝑦 , 𝑦 ) ) = 0 ) )
46 42 sqsqrtd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( √ ‘ ( 𝑦 , 𝑦 ) ) ↑ 2 ) = ( 𝑦 , 𝑦 ) )
47 1 2 3 4 5 phclm ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
48 3 clm0 ⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ 𝐹 ) )
49 47 48 syl ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐹 ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → 0 = ( 0g ‘ 𝐹 ) )
51 46 50 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( √ ‘ ( 𝑦 , 𝑦 ) ) ↑ 2 ) = 0 ↔ ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) ) )
52 45 51 bitr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( √ ‘ ( 𝑦 , 𝑦 ) ) = 0 ↔ ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) ) )
53 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
54 3 6 2 53 13 ipeq0 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) ↔ 𝑦 = ( 0g ‘ 𝑊 ) ) )
55 4 54 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑦 , 𝑦 ) = ( 0g ‘ 𝐹 ) ↔ 𝑦 = ( 0g ‘ 𝑊 ) ) )
56 28 52 55 3bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) = 0 ↔ 𝑦 = ( 0g ‘ 𝑊 ) ) )
57 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil )
58 34 simp1d ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
60 3anass ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) )
61 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
62 61 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
63 62 sqrtcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ℂ )
64 7 63 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( ( √ ‘ 𝑥 ) ∈ 𝐾 ∧ ( √ ‘ 𝑥 ) ∈ ℂ ) )
65 64 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ( √ ‘ 𝑥 ) ∈ 𝐾 ∧ ( √ ‘ 𝑥 ) ∈ ℂ ) ) )
66 35 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↔ 𝑥 ∈ ( 𝐾 ∩ ℂ ) ) )
67 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
68 elin ⊢ ( 𝑥 ∈ ( 𝐾 ∩ ℂ ) ↔ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℂ ) )
69 68 rbaib ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ∈ ( 𝐾 ∩ ℂ ) ↔ 𝑥 ∈ 𝐾 ) )
70 67 69 syl ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( 𝐾 ∩ ℂ ) ↔ 𝑥 ∈ 𝐾 ) )
71 66 70 sylan9bb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↔ 𝑥 ∈ 𝐾 ) )
72 71 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↔ 𝑥 ∈ 𝐾 ) )
73 72 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( 𝑥 ∈ ( Base ‘ 𝐹 ) ↔ 𝑥 ∈ 𝐾 ) ) )
74 73 pm5.32rd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) ) )
75 3anass ⊢ ( ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) )
76 74 75 bitr4di ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) )
77 35 eleq2d ⊢ ( 𝜑 → ( ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ↔ ( √ ‘ 𝑥 ) ∈ ( 𝐾 ∩ ℂ ) ) )
78 elin ⊢ ( ( √ ‘ 𝑥 ) ∈ ( 𝐾 ∩ ℂ ) ↔ ( ( √ ‘ 𝑥 ) ∈ 𝐾 ∧ ( √ ‘ 𝑥 ) ∈ ℂ ) )
79 77 78 bitrdi ⊢ ( 𝜑 → ( ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ↔ ( ( √ ‘ 𝑥 ) ∈ 𝐾 ∧ ( √ ‘ 𝑥 ) ∈ ℂ ) ) )
80 65 76 79 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) )
81 60 80 syl5bi ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) )
82 81 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
83 82 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
84 8 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
85 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ 𝑉 )
86 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
87 1 2 3 57 59 6 83 84 29 12 85 86 tcphcphlem1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( √ ‘ ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) ) ≤ ( ( √ ‘ ( 𝑦 , 𝑦 ) ) + ( √ ‘ ( 𝑧 , 𝑧 ) ) ) )
88 2 12 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
89 88 3expb ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
90 17 89 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
91 oveq12 ⊢ ( ( 𝑥 = ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ∧ 𝑥 = ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑥 , 𝑥 ) = ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) )
92 91 anidms ⊢ ( 𝑥 = ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) → ( 𝑥 , 𝑥 ) = ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) )
93 92 fveq2d ⊢ ( 𝑥 = ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) → ( √ ‘ ( 𝑥 , 𝑥 ) ) = ( √ ‘ ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) ) )
94 93 24 25 fvmpt3i ⊢ ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) = ( √ ‘ ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) ) )
95 90 94 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) = ( √ ‘ ( ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) ) )
96 oveq12 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑧 ) → ( 𝑥 , 𝑥 ) = ( 𝑧 , 𝑧 ) )
97 96 anidms ⊢ ( 𝑥 = 𝑧 → ( 𝑥 , 𝑥 ) = ( 𝑧 , 𝑧 ) )
98 97 fveq2d ⊢ ( 𝑥 = 𝑧 → ( √ ‘ ( 𝑥 , 𝑥 ) ) = ( √ ‘ ( 𝑧 , 𝑧 ) ) )
99 98 24 25 fvmpt3i ⊢ ( 𝑧 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑧 ) = ( √ ‘ ( 𝑧 , 𝑧 ) ) )
100 26 99 oveqan12d ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) + ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑧 ) ) = ( ( √ ‘ ( 𝑦 , 𝑦 ) ) + ( √ ‘ ( 𝑧 , 𝑧 ) ) ) )
101 100 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) + ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑧 ) ) = ( ( √ ‘ ( 𝑦 , 𝑦 ) ) + ( √ ‘ ( 𝑧 , 𝑧 ) ) ) )
102 87 95 101 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ ( 𝑦 ( -g ‘ 𝑊 ) 𝑧 ) ) ≤ ( ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑦 ) + ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑧 ) ) )
103 11 2 12 13 17 20 56 102 tngngpd ⊢ ( 𝜑 → 𝐺 ∈ NrmGrp )
104 phllmod ⊢ ( 𝐺 ∈ PreHil → 𝐺 ∈ LMod )
105 10 104 syl ⊢ ( 𝜑 → 𝐺 ∈ LMod )
106 cnnrg ⊢ ℂfld ∈ NrmRing
107 34 simp3d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) )
108 eqid ⊢ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) = ( ℂfld ↾s ( Base ‘ 𝐹 ) )
109 108 subrgnrg ⊢ ( ( ℂfld ∈ NrmRing ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∈ NrmRing )
110 106 107 109 sylancr ⊢ ( 𝜑 → ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∈ NrmRing )
111 58 110 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ NrmRing )
112 103 105 111 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ LMod ∧ 𝐹 ∈ NrmRing ) )
113 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil )
114 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
115 82 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
116 8 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
117 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
118 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝐹 ) )
119 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
120 1 2 3 113 114 6 115 116 29 117 118 119 tcphcphlem2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( √ ‘ ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) = ( ( abs ‘ 𝑦 ) · ( √ ‘ ( 𝑧 , 𝑧 ) ) ) )
121 2 3 117 29 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
122 121 3expb ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
123 15 122 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
124 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
125 1 124 2 6 tcphnmval ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( √ ‘ ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) )
126 17 123 125 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( √ ‘ ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) , ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) )
127 114 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
128 127 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) = ( ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) ‘ 𝑦 ) )
129 subrgsubg ⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ℂfld ) )
130 107 129 syl ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ℂfld ) )
131 cnfldnm ⊢ abs = ( norm ‘ ℂfld )
132 eqid ⊢ ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) = ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
133 108 131 132 subgnm2 ⊢ ( ( ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
134 130 118 133 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
135 128 134 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
136 1 124 2 6 tcphnmval ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑧 ∈ 𝑉 ) → ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) = ( √ ‘ ( 𝑧 , 𝑧 ) ) )
137 17 119 136 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) = ( √ ‘ ( 𝑧 , 𝑧 ) ) )
138 135 137 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) · ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( abs ‘ 𝑦 ) · ( √ ‘ ( 𝑧 , 𝑧 ) ) ) )
139 120 126 138 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) · ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) ) )
140 139 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ 𝑉 ( ( norm ‘ 𝐺 ) ‘ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) · ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) ) )
141 1 2 tcphbas ⊢ 𝑉 = ( Base ‘ 𝐺 )
142 1 117 tcphvsca ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝐺 )
143 1 3 tcphsca ⊢ 𝐹 = ( Scalar ‘ 𝐺 )
144 eqid ⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
145 141 124 142 143 29 144 isnlm ⊢ ( 𝐺 ∈ NrmMod ↔ ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ 𝑉 ( ( norm ‘ 𝐺 ) ‘ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑦 ) · ( ( norm ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
146 112 140 145 sylanbrc ⊢ ( 𝜑 → 𝐺 ∈ NrmMod )
147 10 146 58 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ PreHil ∧ 𝐺 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
148 elin ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ( 0 [,) +∞ ) ) )
149 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
150 149 anbi2i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ∈ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) )
151 148 150 bitri ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) )
152 151 80 syl5bi ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) → ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) )
153 152 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) )
154 sqrtf ⊢ √ : ℂ ⟶ ℂ
155 ffun ⊢ ( √ : ℂ ⟶ ℂ → Fun √ )
156 154 155 ax-mp ⊢ Fun √
157 inss1 ⊢ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ⊆ ( Base ‘ 𝐹 )
158 157 37 sstrid ⊢ ( 𝜑 → ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ⊆ ℂ )
159 154 fdmi ⊢ dom √ = ℂ
160 158 159 sseqtrrdi ⊢ ( 𝜑 → ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ⊆ dom √ )
161 funimass4 ⊢ ( ( Fun √ ∧ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ⊆ dom √ ) → ( ( √ “ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) )
162 156 160 161 sylancr ⊢ ( 𝜑 → ( ( √ “ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ( √ ‘ 𝑥 ) ∈ ( Base ‘ 𝐹 ) ) )
163 153 162 mpbird ⊢ ( 𝜑 → ( √ “ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ 𝐹 ) )
164 43 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) : 𝑉 ⟶ ℂ )
165 1 2 6 tcphval ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) )
166 cnex ⊢ ℂ ∈ V
167 165 2 166 tngnm ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) : 𝑉 ⟶ ℂ ) → ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) = ( norm ‘ 𝐺 ) )
168 17 164 167 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) = ( norm ‘ 𝐺 ) )
169 168 eqcomd ⊢ ( 𝜑 → ( norm ‘ 𝐺 ) = ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) )
170 1 6 tcphip ⊢ , = ( ·𝑖 ‘ 𝐺 )
171 141 170 124 143 29 iscph ⊢ ( 𝐺 ∈ ℂPreHil ↔ ( ( 𝐺 ∈ PreHil ∧ 𝐺 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) ∧ ( √ “ ( ( Base ‘ 𝐹 ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ 𝐹 ) ∧ ( norm ‘ 𝐺 ) = ( 𝑦 ∈ 𝑉 ↦ ( √ ‘ ( 𝑦 , 𝑦 ) ) ) ) )
172 147 163 169 171 syl3anbrc ⊢ ( 𝜑 → 𝐺 ∈ ℂPreHil )