Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cphsscph Structured version   Visualization version   GIF version

Theorem cphsscph 23342
 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.)
Hypotheses
Ref Expression
cphsscph.x 𝑋 = (𝑊s 𝑈)
cphsscph.s 𝑆 = (LSubSp‘𝑊)
Assertion
Ref Expression
cphsscph ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑋 ∈ ℂPreHil)

Proof of Theorem cphsscph
Dummy variables 𝑏 𝑞 𝑥 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cphphl 23263 . . . . . 6 (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
21anim1i 608 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑊 ∈ PreHil ∧ 𝑈𝑆))
3 cphsscph.x . . . . . 6 𝑋 = (𝑊s 𝑈)
4 cphsscph.s . . . . . 6 𝑆 = (LSubSp‘𝑊)
53, 4phlssphl 20293 . . . . 5 ((𝑊 ∈ PreHil ∧ 𝑈𝑆) → 𝑋 ∈ PreHil)
62, 5syl 17 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑋 ∈ PreHil)
7 cphnvc 23268 . . . . . . 7 (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmVec)
8 nvcnlm 22793 . . . . . . 7 (𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod)
97, 8syl 17 . . . . . 6 (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
109anim1i 608 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑊 ∈ NrmMod ∧ 𝑈𝑆))
113, 4lssnlm 22798 . . . . 5 ((𝑊 ∈ NrmMod ∧ 𝑈𝑆) → 𝑋 ∈ NrmMod)
1210, 11syl 17 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑋 ∈ NrmMod)
13 eqid 2765 . . . . . . 7 (Scalar‘𝑊) = (Scalar‘𝑊)
14 eqid 2765 . . . . . . 7 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
1513, 14cphsca 23271 . . . . . 6 (𝑊 ∈ ℂPreHil → (Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊))))
1615adantr 472 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊))))
173, 13resssca 16317 . . . . . . 7 (𝑈𝑆 → (Scalar‘𝑊) = (Scalar‘𝑋))
1817fveq2d 6383 . . . . . . . 8 (𝑈𝑆 → (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑋)))
1918oveq2d 6862 . . . . . . 7 (𝑈𝑆 → (ℂflds (Base‘(Scalar‘𝑊))) = (ℂflds (Base‘(Scalar‘𝑋))))
2017, 19eqeq12d 2780 . . . . . 6 (𝑈𝑆 → ((Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊))) ↔ (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋)))))
2120adantl 473 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((Scalar‘𝑊) = (ℂflds (Base‘(Scalar‘𝑊))) ↔ (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋)))))
2216, 21mpbid 223 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋))))
236, 12, 223jca 1158 . . 3 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑋 ∈ PreHil ∧ 𝑋 ∈ NrmMod ∧ (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋)))))
24 funmpt 6108 . . . . . . . . 9 Fun (𝑥 ∈ ℂ ↦ (𝑐 ∈ ℂ ((𝑐↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑐) ∧ (i · 𝑐) ∉ ℝ+)))
25 df-sqrt 14274 . . . . . . . . . 10 √ = (𝑥 ∈ ℂ ↦ (𝑐 ∈ ℂ ((𝑐↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑐) ∧ (i · 𝑐) ∉ ℝ+)))
2625funeqi 6091 . . . . . . . . 9 (Fun √ ↔ Fun (𝑥 ∈ ℂ ↦ (𝑐 ∈ ℂ ((𝑐↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑐) ∧ (i · 𝑐) ∉ ℝ+))))
2724, 26mpbir 222 . . . . . . . 8 Fun √
28 fvelima 6441 . . . . . . . . 9 ((Fun √ ∧ 𝑥 ∈ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)))) → ∃𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥)
2928ex 401 . . . . . . . 8 (Fun √ → (𝑥 ∈ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) → ∃𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥))
3027, 29ax-mp 5 . . . . . . 7 (𝑥 ∈ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) → ∃𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥)
31 simpl 474 . . . . . . . . . . . . 13 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑊 ∈ ℂPreHil)
3231adantl 473 . . . . . . . . . . . 12 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → 𝑊 ∈ ℂPreHil)
33 elinel1 3963 . . . . . . . . . . . . . . 15 (𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈ (Base‘(Scalar‘𝑊)))
3433adantr 472 . . . . . . . . . . . . . 14 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → 𝑞 ∈ (Base‘(Scalar‘𝑊)))
35 elinel2 3964 . . . . . . . . . . . . . . . 16 (𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈ (0[,)+∞))
36 elrege0 12487 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ (0[,)+∞) ↔ (𝑞 ∈ ℝ ∧ 0 ≤ 𝑞))
37 simpl 474 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℝ ∧ 0 ≤ 𝑞) → 𝑞 ∈ ℝ)
3836, 37sylbi 208 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (0[,)+∞) → 𝑞 ∈ ℝ)
3935, 38syl 17 . . . . . . . . . . . . . . 15 (𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈ ℝ)
4039adantr 472 . . . . . . . . . . . . . 14 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → 𝑞 ∈ ℝ)
41 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℝ ∧ 0 ≤ 𝑞) → 0 ≤ 𝑞)
4236, 41sylbi 208 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (0[,)+∞) → 0 ≤ 𝑞)
4335, 42syl 17 . . . . . . . . . . . . . . 15 (𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 0 ≤ 𝑞)
4443adantr 472 . . . . . . . . . . . . . 14 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → 0 ≤ 𝑞)
4534, 40, 443jca 1158 . . . . . . . . . . . . 13 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞))
4645adantr 472 . . . . . . . . . . . 12 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞))
4732, 46jca 507 . . . . . . . . . . 11 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → (𝑊 ∈ ℂPreHil ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞)))
4813, 14cphsqrtcl 23276 . . . . . . . . . . 11 ((𝑊 ∈ ℂPreHil ∧ (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞)) → (√‘𝑞) ∈ (Base‘(Scalar‘𝑊)))
4947, 48syl 17 . . . . . . . . . 10 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → (√‘𝑞) ∈ (Base‘(Scalar‘𝑊)))
50 eleq1 2832 . . . . . . . . . . . 12 ((√‘𝑞) = 𝑥 → ((√‘𝑞) ∈ (Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5150adantl 473 . . . . . . . . . . 11 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → ((√‘𝑞) ∈ (Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5251adantr 472 . . . . . . . . . 10 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → ((√‘𝑞) ∈ (Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5349, 52mpbid 223 . . . . . . . . 9 (((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈𝑆)) → 𝑥 ∈ (Base‘(Scalar‘𝑊)))
5453ex 401 . . . . . . . 8 ((𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧ (√‘𝑞) = 𝑥) → ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5554rexlimiva 3175 . . . . . . 7 (∃𝑞 ∈ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥 → ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5630, 55syl 17 . . . . . 6 (𝑥 ∈ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) → ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5756com12 32 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑥 ∈ (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) → 𝑥 ∈ (Base‘(Scalar‘𝑊))))
5857ssrdv 3769 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)))
5918ineq1d 3977 . . . . . . 7 (𝑈𝑆 → ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) = ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞)))
6059imaeq2d 5650 . . . . . 6 (𝑈𝑆 → (√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) = (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))))
6160, 18sseq12d 3796 . . . . 5 (𝑈𝑆 → ((√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ↔ (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑋))))
6261adantl 473 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑊)) ↔ (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑋))))
6358, 62mpbid 223 . . 3 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑋)))
64 cphlmod 23266 . . . . . . 7 (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
6564anim1i 608 . . . . . 6 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑊 ∈ LMod ∧ 𝑈𝑆))
664lsssubg 19243 . . . . . 6 ((𝑊 ∈ LMod ∧ 𝑈𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
6765, 66syl 17 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
68 eqid 2765 . . . . . 6 (norm‘𝑊) = (norm‘𝑊)
69 eqid 2765 . . . . . 6 (norm‘𝑋) = (norm‘𝑋)
703, 68, 69subgnm 22730 . . . . 5 (𝑈 ∈ (SubGrp‘𝑊) → (norm‘𝑋) = ((norm‘𝑊) ↾ 𝑈))
7167, 70syl 17 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (norm‘𝑋) = ((norm‘𝑊) ↾ 𝑈))
72 eqid 2765 . . . . . . . . . . 11 (Base‘𝑊) = (Base‘𝑊)
73 eqid 2765 . . . . . . . . . . 11 (·𝑖𝑊) = (·𝑖𝑊)
7472, 73, 68cphnmfval 23284 . . . . . . . . . 10 (𝑊 ∈ ℂPreHil → (norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑊)𝑏))))
7574adantr 472 . . . . . . . . 9 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑊)𝑏))))
76 eqid 2765 . . . . . . . . . . . . . . 15 (·𝑖𝑋) = (·𝑖𝑋)
773, 73, 76ssipeq 20290 . . . . . . . . . . . . . 14 (𝑈𝑆 → (·𝑖𝑋) = (·𝑖𝑊))
7877eqcomd 2771 . . . . . . . . . . . . 13 (𝑈𝑆 → (·𝑖𝑊) = (·𝑖𝑋))
7978adantl 473 . . . . . . . . . . . 12 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (·𝑖𝑊) = (·𝑖𝑋))
8079oveqd 6863 . . . . . . . . . . 11 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑏(·𝑖𝑊)𝑏) = (𝑏(·𝑖𝑋)𝑏))
8180fveq2d 6383 . . . . . . . . . 10 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (√‘(𝑏(·𝑖𝑊)𝑏)) = (√‘(𝑏(·𝑖𝑋)𝑏)))
8281mpteq2dv 4906 . . . . . . . . 9 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑊)𝑏))) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))))
8375, 82eqtrd 2799 . . . . . . . 8 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))))
8483reseq1d 5566 . . . . . . 7 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((norm‘𝑊) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ 𝑈))
8572, 4lssss 19220 . . . . . . . . . 10 (𝑈𝑆𝑈 ⊆ (Base‘𝑊))
8685adantl 473 . . . . . . . . 9 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑈 ⊆ (Base‘𝑊))
87 dfss 3749 . . . . . . . . 9 (𝑈 ⊆ (Base‘𝑊) ↔ 𝑈 = (𝑈 ∩ (Base‘𝑊)))
8886, 87sylib 209 . . . . . . . 8 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑈 = (𝑈 ∩ (Base‘𝑊)))
8988reseq2d 5567 . . . . . . 7 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (𝑈 ∩ (Base‘𝑊))))
9084, 89eqtrd 2799 . . . . . 6 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((norm‘𝑊) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (𝑈 ∩ (Base‘𝑊))))
91 simpr 477 . . . . . . . 8 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑈𝑆)
923, 72ressbas 16216 . . . . . . . 8 (𝑈𝑆 → (𝑈 ∩ (Base‘𝑊)) = (Base‘𝑋))
9391, 92syl 17 . . . . . . 7 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (𝑈 ∩ (Base‘𝑊)) = (Base‘𝑋))
9493reseq2d 5567 . . . . . 6 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (𝑈 ∩ (Base‘𝑊))) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (Base‘𝑋)))
9590, 94eqtrd 2799 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((norm‘𝑊) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (Base‘𝑋)))
963, 72ressbasss 16218 . . . . . . 7 (Base‘𝑋) ⊆ (Base‘𝑊)
9796a1i 11 . . . . . 6 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (Base‘𝑋) ⊆ (Base‘𝑊))
9897resmptd 5631 . . . . 5 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))) ↾ (Base‘𝑋)) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))))
9995, 98eqtrd 2799 . . . 4 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((norm‘𝑊) ↾ 𝑈) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))))
10071, 99eqtrd 2799 . . 3 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → (norm‘𝑋) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖𝑋)𝑏))))
10123, 63, 1003jca 1158 . 2 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → ((𝑋 ∈ PreHil ∧ 𝑋 ∈ NrmMod ∧ (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋)))) ∧ (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑋)) ∧ (norm‘𝑋) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖𝑋)𝑏)))))
102 eqid 2765 . . 3 (Base‘𝑋) = (Base‘𝑋)
103 eqid 2765 . . 3 (Scalar‘𝑋) = (Scalar‘𝑋)
104 eqid 2765 . . 3 (Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋))
105102, 76, 69, 103, 104iscph 23262 . 2 (𝑋 ∈ ℂPreHil ↔ ((𝑋 ∈ PreHil ∧ 𝑋 ∈ NrmMod ∧ (Scalar‘𝑋) = (ℂflds (Base‘(Scalar‘𝑋)))) ∧ (√ “ ((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆ (Base‘(Scalar‘𝑋)) ∧ (norm‘𝑋) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖𝑋)𝑏)))))
106101, 105sylibr 225 1 ((𝑊 ∈ ℂPreHil ∧ 𝑈𝑆) → 𝑋 ∈ ℂPreHil)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155   ∉ wnel 3040  ∃wrex 3056   ∩ cin 3733   ⊆ wss 3734   class class class wbr 4811   ↦ cmpt 4890   ↾ cres 5281   “ cima 5282  Fun wfun 6064  ‘cfv 6070  ℩crio 6806  (class class class)co 6846  ℂcc 10191  ℝcr 10192  0cc0 10193  ici 10195   · cmul 10198  +∞cpnf 10329   ≤ cle 10333  2c2 11331  ℝ+crp 12033  [,)cico 12384  ↑cexp 13072  ℜcre 14136  √csqrt 14272  Basecbs 16144   ↾s cress 16145  Scalarcsca 16231  ·𝑖cip 16233  SubGrpcsubg 17866  LModclmod 19146  LSubSpclss 19215  ℂfldccnfld 20033  PreHilcphl 20258  normcnm 22674  NrmModcnlm 22678  NrmVeccnvc 22679  ℂPreHilccph 23258 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271 This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-er 7951  df-map 8066  df-en 8165  df-dom 8166  df-sdom 8167  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ico 12388  df-seq 13014  df-exp 13073  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ds 16250  df-rest 16363  df-topn 16364  df-0g 16382  df-topgen 16384  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-grp 17706  df-minusg 17707  df-sbg 17708  df-subg 17869  df-ghm 17936  df-mgp 18771  df-ur 18783  df-ring 18830  df-subrg 19061  df-lmod 19148  df-lss 19216  df-lsp 19258  df-lmhm 19308  df-lvec 19389  df-sra 19460  df-rgmod 19461  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-phl 20260  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-xms 22418  df-ms 22419  df-nm 22680  df-ngp 22681  df-nlm 22684  df-nvc 22685  df-cph 23260 This theorem is referenced by:  cphssphl  23462  cmslsschl  23468  chlcsschl  23469
 Copyright terms: Public domain W3C validator