Metamath Proof Explorer

Theorem rrxcph

Description: Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses rrxval.r ⊢H=msup
rrxbase.b ⊢B=BaseH
Assertion rrxcph ⊢I∈V→H∈CPreHil

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢H=msup
2 rrxbase.b ⊢B=BaseH
3 1 rrxval ⊢I∈V→H=toCPreHil⁡ℝfldfreeLModI
4 eqid ⊢toCPreHil⁡ℝfldfreeLModI=toCPreHil⁡ℝfldfreeLModI
5 eqid ⊢BaseℝfldfreeLModI=BaseℝfldfreeLModI
6 eqid ⊢Scalar⁡ℝfldfreeLModI=Scalar⁡ℝfldfreeLModI
7 eqid ⊢ℝfldfreeLModI=ℝfldfreeLModI
8 rebase ⊢ℝ=Baseℝfld
9 remulr ⊢×=⋅ℝfld
10 eqid ⊢⋅𝑖⁡ℝfldfreeLModI=⋅𝑖⁡ℝfldfreeLModI
11 eqid ⊢0ℝfldfreeLModI=0ℝfldfreeLModI
12 re0g ⊢0=0ℝfld
13 refldcj ⊢*=*ℝfld
14 refld ⊢ℝfld∈Field
15 14 a1i ⊢I∈V→ℝfld∈Field
16 fconstmpt ⊢I×0=x∈I⟼0
17 7 8 5 frlmbasf ⊢I∈V∧f∈BaseℝfldfreeLModI→f:I⟶ℝ
18 17 ffnd ⊢I∈V∧f∈BaseℝfldfreeLModI→fFnI
19 18 3adant3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→fFnI
20 simpl ⊢I∈V∧f∈BaseℝfldfreeLModI→I∈V
21 14 a1i ⊢I∈V∧f∈BaseℝfldfreeLModI→ℝfld∈Field
22 simpr ⊢I∈V∧f∈BaseℝfldfreeLModI→f∈BaseℝfldfreeLModI
23 7 8 9 5 10 frlmipval ⊢I∈V∧ℝfld∈Field∧f∈BaseℝfldfreeLModI∧f∈BaseℝfldfreeLModI→f⋅𝑖⁡ℝfldfreeLModIf=∑ℝfldf×ff
24 20 21 22 22 23 syl22anc ⊢I∈V∧f∈BaseℝfldfreeLModI→f⋅𝑖⁡ℝfldfreeLModIf=∑ℝfldf×ff
25 inidm ⊢I∩I=I
26 eqidd ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈I→f⁡x=f⁡x
27 18 18 20 20 25 26 26 offval ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ff=x∈I⟼f⁡x⁢f⁡x
28 17 ffvelcdmda ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈I→f⁡x∈ℝ
29 28 28 remulcld ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈I→f⁡x⁢f⁡x∈ℝ
30 27 29 fmpt3d ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ff:I⟶ℝ
31 ovexd ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ff∈V
32 30 ffund ⊢I∈V∧f∈BaseℝfldfreeLModI→Fun⁡f×ff
33 7 12 5 frlmbasfsupp ⊢I∈V∧f∈BaseℝfldfreeLModI→finSupp0⁡f
34 0red ⊢I∈V∧f∈BaseℝfldfreeLModI→0∈ℝ
35 simpr ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈ℝ→x∈ℝ
36 35 recnd ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈ℝ→x∈ℂ
37 36 mul02d ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈ℝ→0⋅x=0
38 20 34 17 17 37 suppofss1d ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ffsupp0⊆fsupp0
39 fsuppsssupp ⊢f×ff∈V∧Fun⁡f×ff∧finSupp0⁡f∧f×ffsupp0⊆fsupp0→finSupp0⁡f×ff
40 31 32 33 38 39 syl22anc ⊢I∈V∧f∈BaseℝfldfreeLModI→finSupp0⁡f×ff
41 regsumsupp ⊢f×ff:I⟶ℝ∧finSupp0⁡f×ff∧I∈V→∑ℝfldf×ff=∑x∈f×ffsupp0f×ff⁡x
42 30 40 20 41 syl3anc ⊢I∈V∧f∈BaseℝfldfreeLModI→∑ℝfldf×ff=∑x∈f×ffsupp0f×ff⁡x
43 suppssdm ⊢fsupp0⊆dom⁡f
44 43 17 fssdm ⊢I∈V∧f∈BaseℝfldfreeLModI→fsupp0⊆I
45 38 44 sstrd ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ffsupp0⊆I
46 45 sselda ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈supp0⁡f×ff→x∈I
47 18 18 20 20 25 26 26 ofval ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈I→f×ff⁡x=f⁡x⁢f⁡x
48 46 47 syldan ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈supp0⁡f×ff→f×ff⁡x=f⁡x⁢f⁡x
49 48 sumeq2dv ⊢I∈V∧f∈BaseℝfldfreeLModI→∑x∈f×ffsupp0f×ff⁡x=∑x∈f×ffsupp0f⁡x⁢f⁡x
50 42 49 eqtrd ⊢I∈V∧f∈BaseℝfldfreeLModI→∑ℝfldf×ff=∑x∈f×ffsupp0f⁡x⁢f⁡x
51 24 50 eqtrd ⊢I∈V∧f∈BaseℝfldfreeLModI→f⋅𝑖⁡ℝfldfreeLModIf=∑x∈f×ffsupp0f⁡x⁢f⁡x
52 51 3adant3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→f⋅𝑖⁡ℝfldfreeLModIf=∑x∈f×ffsupp0f⁡x⁢f⁡x
53 simp3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→f⋅𝑖⁡ℝfldfreeLModIf=0
54 52 53 eqtr3d ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→∑x∈f×ffsupp0f⁡x⁢f⁡x=0
55 33 fsuppimpd ⊢I∈V∧f∈BaseℝfldfreeLModI→fsupp0∈Fin
56 55 38 ssfid ⊢I∈V∧f∈BaseℝfldfreeLModI→f×ffsupp0∈Fin
57 46 29 syldan ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈supp0⁡f×ff→f⁡x⁢f⁡x∈ℝ
58 28 msqge0d ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈I→0≤f⁡x⁢f⁡x
59 46 58 syldan ⊢I∈V∧f∈BaseℝfldfreeLModI∧x∈supp0⁡f×ff→0≤f⁡x⁢f⁡x
60 56 57 59 fsum00 ⊢I∈V∧f∈BaseℝfldfreeLModI→∑x∈f×ffsupp0f⁡x⁢f⁡x=0↔∀x∈supp0⁡f×fff⁡x⁢f⁡x=0
61 60 3adant3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→∑x∈f×ffsupp0f⁡x⁢f⁡x=0↔∀x∈supp0⁡f×fff⁡x⁢f⁡x=0
62 54 61 mpbid ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→∀x∈supp0⁡f×fff⁡x⁢f⁡x=0
63 62 r19.21bi ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈supp0⁡f×ff→f⁡x⁢f⁡x=0
64 63 adantlr ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈supp0⁡f×ff→f⁡x⁢f⁡x=0
65 28 3adantl3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f⁡x∈ℝ
66 65 recnd ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f⁡x∈ℂ
67 66 66 mul0ord ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f⁡x⁢f⁡x=0↔f⁡x=0∨f⁡x=0
68 67 adantr ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈supp0⁡f×ff→f⁡x⁢f⁡x=0↔f⁡x=0∨f⁡x=0
69 64 68 mpbid ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈supp0⁡f×ff→f⁡x=0∨f⁡x=0
70 oridm ⊢f⁡x=0∨f⁡x=0↔f⁡x=0
71 69 70 sylib ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈supp0⁡f×ff→f⁡x=0
72 30 3adant3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→f×ff:I⟶ℝ
73 72 adantr ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ff:I⟶ℝ
74 ssidd ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ffsupp0⊆f×ffsupp0
75 simpl1 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→I∈V
76 0red ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→0∈ℝ
77 73 74 75 76 suppssr ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈I∖supp0⁡f×ff→f×ff⁡x=0
78 47 3adantl3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ff⁡x=f⁡x⁢f⁡x
79 78 eqeq1d ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ff⁡x=0↔f⁡x⁢f⁡x=0
80 79 67 bitrd ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ff⁡x=0↔f⁡x=0∨f⁡x=0
81 80 70 bitrdi ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f×ff⁡x=0↔f⁡x=0
82 81 biimpa ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧f×ff⁡x=0→f⁡x=0
83 77 82 syldan ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I∧x∈I∖supp0⁡f×ff→f⁡x=0
84 undif ⊢f×ffsupp0⊆I↔supp0⁡f×ff∪I∖supp0⁡f×ff=I
85 45 84 sylib ⊢I∈V∧f∈BaseℝfldfreeLModI→supp0⁡f×ff∪I∖supp0⁡f×ff=I
86 85 eleq2d ⊢I∈V∧f∈BaseℝfldfreeLModI→x∈supp0⁡f×ff∪I∖supp0⁡f×ff↔x∈I
87 86 3adant3 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→x∈supp0⁡f×ff∪I∖supp0⁡f×ff↔x∈I
88 87 biimpar ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→x∈supp0⁡f×ff∪I∖supp0⁡f×ff
89 elun ⊢x∈supp0⁡f×ff∪I∖supp0⁡f×ff↔x∈supp0⁡f×ff∨x∈I∖supp0⁡f×ff
90 88 89 sylib ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→x∈supp0⁡f×ff∨x∈I∖supp0⁡f×ff
91 71 83 90 mpjaodan ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0∧x∈I→f⁡x=0
92 91 ralrimiva ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→∀x∈If⁡x=0
93 fconstfv ⊢f:I⟶0↔fFnI∧∀x∈If⁡x=0
94 c0ex ⊢0∈V
95 94 fconst2 ⊢f:I⟶0↔f=I×0
96 93 95 sylbb1 ⊢fFnI∧∀x∈If⁡x=0→f=I×0
97 19 92 96 syl2anc ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→f=I×0
98 isfld ⊢ℝfld∈Field↔ℝfld∈DivRing∧ℝfld∈CRing
99 14 98 mpbi ⊢ℝfld∈DivRing∧ℝfld∈CRing
100 99 simpli ⊢ℝfld∈DivRing
101 drngring ⊢ℝfld∈DivRing→ℝfld∈Ring
102 100 101 ax-mp ⊢ℝfld∈Ring
103 7 12 frlm0 ⊢ℝfld∈Ring∧I∈V→I×0=0ℝfldfreeLModI
104 102 103 mpan ⊢I∈V→I×0=0ℝfldfreeLModI
105 104 16 eqtr3di ⊢I∈V→0ℝfldfreeLModI=x∈I⟼0
106 105 3ad2ant1 ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→0ℝfldfreeLModI=x∈I⟼0
107 16 97 106 3eqtr4a ⊢I∈V∧f∈BaseℝfldfreeLModI∧f⋅𝑖⁡ℝfldfreeLModIf=0→f=0ℝfldfreeLModI
108 cjre ⊢x∈ℝ→x‾=x
109 108 adantl ⊢I∈V∧x∈ℝ→x‾=x
110 id ⊢I∈V→I∈V
111 7 8 9 5 10 11 12 13 15 107 109 110 frlmphl ⊢I∈V→ℝfldfreeLModI∈PreHil
112 7 frlmsca ⊢ℝfld∈Field∧I∈V→ℝfld=Scalar⁡ℝfldfreeLModI
113 14 112 mpan ⊢I∈V→ℝfld=Scalar⁡ℝfldfreeLModI
114 df-refld ⊢ℝfld=ℂfld↾𝑠ℝ
115 113 114 eqtr3di ⊢I∈V→Scalar⁡ℝfldfreeLModI=ℂfld↾𝑠ℝ
116 simpr1 ⊢I∈V∧f∈ℝ∧f∈ℝ∧0≤f→f∈ℝ
117 simpr3 ⊢I∈V∧f∈ℝ∧f∈ℝ∧0≤f→0≤f
118 116 117 resqrtcld ⊢I∈V∧f∈ℝ∧f∈ℝ∧0≤f→f∈ℝ
119 56 57 59 fsumge0 ⊢I∈V∧f∈BaseℝfldfreeLModI→0≤∑x∈f×ffsupp0f⁡x⁢f⁡x
120 119 50 breqtrrd ⊢I∈V∧f∈BaseℝfldfreeLModI→0≤∑ℝfldf×ff
121 120 24 breqtrrd ⊢I∈V∧f∈BaseℝfldfreeLModI→0≤f⋅𝑖⁡ℝfldfreeLModIf
122 4 5 6 111 115 10 118 121 tcphcph ⊢I∈V→toCPreHil⁡ℝfldfreeLModI∈CPreHil
123 3 122 eqeltrd ⊢I∈V→H∈CPreHil