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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
cphsscph.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion cphsscph ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂPreHil )

Proof

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