Metamath Proof Explorer

Theorem cphsscph

Description: A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008) (Revised by AV, 25-Sep-2022)

Ref Expression
Hypotheses cphsscph.x ⊢X=W↾𝑠U
cphsscph.s ⊢S=LSubSp⁡W
Assertion cphsscph ⊢W∈CPreHil∧U∈S→X∈CPreHil

Proof

Step Hyp Ref Expression
1 cphsscph.x ⊢X=W↾𝑠U
2 cphsscph.s ⊢S=LSubSp⁡W
3 cphphl ⊢W∈CPreHil→W∈PreHil
4 1 2 phlssphl ⊢W∈PreHil∧U∈S→X∈PreHil
5 3 4 sylan ⊢W∈CPreHil∧U∈S→X∈PreHil
6 cphnlm ⊢W∈CPreHil→W∈NrmMod
7 1 2 lssnlm ⊢W∈NrmMod∧U∈S→X∈NrmMod
8 6 7 sylan ⊢W∈CPreHil∧U∈S→X∈NrmMod
9 eqid ⊢Scalar⁡W=Scalar⁡W
10 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
11 9 10 cphsca ⊢W∈CPreHil→Scalar⁡W=ℂfld↾𝑠BaseScalar⁡W
12 11 adantr ⊢W∈CPreHil∧U∈S→Scalar⁡W=ℂfld↾𝑠BaseScalar⁡W
13 1 9 resssca ⊢U∈S→Scalar⁡W=Scalar⁡X
14 13 fveq2d ⊢U∈S→BaseScalar⁡W=BaseScalar⁡X
15 14 oveq2d ⊢U∈S→ℂfld↾𝑠BaseScalar⁡W=ℂfld↾𝑠BaseScalar⁡X
16 13 15 eqeq12d ⊢U∈S→Scalar⁡W=ℂfld↾𝑠BaseScalar⁡W↔Scalar⁡X=ℂfld↾𝑠BaseScalar⁡X
17 16 adantl ⊢W∈CPreHil∧U∈S→Scalar⁡W=ℂfld↾𝑠BaseScalar⁡W↔Scalar⁡X=ℂfld↾𝑠BaseScalar⁡X
18 12 17 mpbid ⊢W∈CPreHil∧U∈S→Scalar⁡X=ℂfld↾𝑠BaseScalar⁡X
19 5 8 18 3jca ⊢W∈CPreHil∧U∈S→X∈PreHil∧X∈NrmMod∧Scalar⁡X=ℂfld↾𝑠BaseScalar⁡X
20 simpl ⊢W∈CPreHil∧U∈S→W∈CPreHil
21 elinel1 ⊢q∈BaseScalar⁡W∩0+∞→q∈BaseScalar⁡W
22 21 adantr ⊢q∈BaseScalar⁡W∩0+∞∧q=x→q∈BaseScalar⁡W
23 elinel2 ⊢q∈BaseScalar⁡W∩0+∞→q∈0+∞
24 elrege0 ⊢q∈0+∞↔q∈ℝ∧0≤q
25 24 simplbi ⊢q∈0+∞→q∈ℝ
26 23 25 syl ⊢q∈BaseScalar⁡W∩0+∞→q∈ℝ
27 26 adantr ⊢q∈BaseScalar⁡W∩0+∞∧q=x→q∈ℝ
28 24 simprbi ⊢q∈0+∞→0≤q
29 23 28 syl ⊢q∈BaseScalar⁡W∩0+∞→0≤q
30 29 adantr ⊢q∈BaseScalar⁡W∩0+∞∧q=x→0≤q
31 22 27 30 3jca ⊢q∈BaseScalar⁡W∩0+∞∧q=x→q∈BaseScalar⁡W∧q∈ℝ∧0≤q
32 9 10 cphsqrtcl ⊢W∈CPreHil∧q∈BaseScalar⁡W∧q∈ℝ∧0≤q→q∈BaseScalar⁡W
33 20 31 32 syl2anr ⊢q∈BaseScalar⁡W∩0+∞∧q=x∧W∈CPreHil∧U∈S→q∈BaseScalar⁡W
34 eleq1 ⊢q=x→q∈BaseScalar⁡W↔x∈BaseScalar⁡W
35 34 adantl ⊢q∈BaseScalar⁡W∩0+∞∧q=x→q∈BaseScalar⁡W↔x∈BaseScalar⁡W
36 35 adantr ⊢q∈BaseScalar⁡W∩0+∞∧q=x∧W∈CPreHil∧U∈S→q∈BaseScalar⁡W↔x∈BaseScalar⁡W
37 33 36 mpbid ⊢q∈BaseScalar⁡W∩0+∞∧q=x∧W∈CPreHil∧U∈S→x∈BaseScalar⁡W
38 37 ex ⊢q∈BaseScalar⁡W∩0+∞∧q=x→W∈CPreHil∧U∈S→x∈BaseScalar⁡W
39 38 rexlimiva ⊢∃q∈BaseScalar⁡W∩0+∞q=x→W∈CPreHil∧U∈S→x∈BaseScalar⁡W
40 df-sqrt ⊢√=x∈ℂ⟼ιc∈ℂ|c2=x∧0≤ℜ⁡c∧i⁢c∉ℝ+
41 40 funmpt2 ⊢Fun⁡√
42 fvelima ⊢Fun⁡√∧x∈√BaseScalar⁡W∩0+∞→∃q∈BaseScalar⁡W∩0+∞q=x
43 41 42 mpan ⊢x∈√BaseScalar⁡W∩0+∞→∃q∈BaseScalar⁡W∩0+∞q=x
44 39 43 syl11 ⊢W∈CPreHil∧U∈S→x∈√BaseScalar⁡W∩0+∞→x∈BaseScalar⁡W
45 44 ssrdv ⊢W∈CPreHil∧U∈S→√BaseScalar⁡W∩0+∞⊆BaseScalar⁡W
46 14 ineq1d ⊢U∈S→BaseScalar⁡W∩0+∞=BaseScalar⁡X∩0+∞
47 46 imaeq2d ⊢U∈S→√BaseScalar⁡W∩0+∞=√BaseScalar⁡X∩0+∞
48 47 14 sseq12d ⊢U∈S→√BaseScalar⁡W∩0+∞⊆BaseScalar⁡W↔√BaseScalar⁡X∩0+∞⊆BaseScalar⁡X
49 48 adantl ⊢W∈CPreHil∧U∈S→√BaseScalar⁡W∩0+∞⊆BaseScalar⁡W↔√BaseScalar⁡X∩0+∞⊆BaseScalar⁡X
50 45 49 mpbid ⊢W∈CPreHil∧U∈S→√BaseScalar⁡X∩0+∞⊆BaseScalar⁡X
51 cphlmod ⊢W∈CPreHil→W∈LMod
52 2 lsssubg ⊢W∈LMod∧U∈S→U∈SubGrp⁡W
53 51 52 sylan ⊢W∈CPreHil∧U∈S→U∈SubGrp⁡W
54 eqid ⊢norm⁡W=norm⁡W
55 eqid ⊢norm⁡X=norm⁡X
56 1 54 55 subgnm ⊢U∈SubGrp⁡W→norm⁡X=norm⁡W↾U
57 53 56 syl ⊢W∈CPreHil∧U∈S→norm⁡X=norm⁡W↾U
58 eqid ⊢BaseW=BaseW
59 eqid ⊢⋅𝑖⁡W=⋅𝑖⁡W
60 58 59 54 cphnmfval ⊢W∈CPreHil→norm⁡W=b∈BaseW⟼b⋅𝑖⁡Wb
61 60 adantr ⊢W∈CPreHil∧U∈S→norm⁡W=b∈BaseW⟼b⋅𝑖⁡Wb
62 1 59 ressip ⊢U∈S→⋅𝑖⁡W=⋅𝑖⁡X
63 62 adantl ⊢W∈CPreHil∧U∈S→⋅𝑖⁡W=⋅𝑖⁡X
64 63 oveqd ⊢W∈CPreHil∧U∈S→b⋅𝑖⁡Wb=b⋅𝑖⁡Xb
65 64 fveq2d ⊢W∈CPreHil∧U∈S→b⋅𝑖⁡Wb=b⋅𝑖⁡Xb
66 65 mpteq2dv ⊢W∈CPreHil∧U∈S→b∈BaseW⟼b⋅𝑖⁡Wb=b∈BaseW⟼b⋅𝑖⁡Xb
67 61 66 eqtrd ⊢W∈CPreHil∧U∈S→norm⁡W=b∈BaseW⟼b⋅𝑖⁡Xb
68 58 2 lssss ⊢U∈S→U⊆BaseW
69 68 adantl ⊢W∈CPreHil∧U∈S→U⊆BaseW
70 dfss ⊢U⊆BaseW↔U=U∩BaseW
71 69 70 sylib ⊢W∈CPreHil∧U∈S→U=U∩BaseW
72 67 71 reseq12d ⊢W∈CPreHil∧U∈S→norm⁡W↾U=b∈BaseW⟼b⋅𝑖⁡Xb↾U∩BaseW
73 1 58 ressbas ⊢U∈S→U∩BaseW=BaseX
74 73 adantl ⊢W∈CPreHil∧U∈S→U∩BaseW=BaseX
75 74 reseq2d ⊢W∈CPreHil∧U∈S→b∈BaseW⟼b⋅𝑖⁡Xb↾U∩BaseW=b∈BaseW⟼b⋅𝑖⁡Xb↾BaseX
76 72 75 eqtrd ⊢W∈CPreHil∧U∈S→norm⁡W↾U=b∈BaseW⟼b⋅𝑖⁡Xb↾BaseX
77 1 58 ressbasss ⊢BaseX⊆BaseW
78 77 a1i ⊢W∈CPreHil∧U∈S→BaseX⊆BaseW
79 78 resmptd ⊢W∈CPreHil∧U∈S→b∈BaseW⟼b⋅𝑖⁡Xb↾BaseX=b∈BaseX⟼b⋅𝑖⁡Xb
80 57 76 79 3eqtrd ⊢W∈CPreHil∧U∈S→norm⁡X=b∈BaseX⟼b⋅𝑖⁡Xb
81 eqid ⊢BaseX=BaseX
82 eqid ⊢⋅𝑖⁡X=⋅𝑖⁡X
83 eqid ⊢Scalar⁡X=Scalar⁡X
84 eqid ⊢BaseScalar⁡X=BaseScalar⁡X
85 81 82 55 83 84 iscph ⊢X∈CPreHil↔X∈PreHil∧X∈NrmMod∧Scalar⁡X=ℂfld↾𝑠BaseScalar⁡X∧√BaseScalar⁡X∩0+∞⊆BaseScalar⁡X∧norm⁡X=b∈BaseX⟼b⋅𝑖⁡Xb
86 19 50 80 85 syl3anbrc ⊢W∈CPreHil∧U∈S→X∈CPreHil