| Step | Hyp | Ref
| Expression |
| 1 | | cphphl 25205 |
. . . 4
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
PreHil) |
| 2 | | cphsscph.x |
. . . . 5
⊢ 𝑋 = (𝑊 ↾s 𝑈) |
| 3 | | cphsscph.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
| 4 | 2, 3 | phlssphl 21677 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ PreHil) |
| 5 | 1, 4 | sylan 580 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑋 ∈ PreHil) |
| 6 | | cphnlm 25206 |
. . . 4
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmMod) |
| 7 | 2, 3 | lssnlm 24722 |
. . . 4
⊢ ((𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) |
| 8 | 6, 7 | sylan 580 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑋 ∈ NrmMod) |
| 9 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 11 | 9, 10 | cphsca 25213 |
. . . . 5
⊢ (𝑊 ∈ ℂPreHil →
(Scalar‘𝑊) =
(ℂfld ↾s (Base‘(Scalar‘𝑊)))) |
| 12 | 11 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (Scalar‘𝑊) = (ℂfld
↾s (Base‘(Scalar‘𝑊)))) |
| 13 | 2, 9 | resssca 17387 |
. . . . . 6
⊢ (𝑈 ∈ 𝑆 → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 14 | 13 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑆 → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑋))) |
| 15 | 14 | oveq2d 7447 |
. . . . . 6
⊢ (𝑈 ∈ 𝑆 → (ℂfld
↾s (Base‘(Scalar‘𝑊))) = (ℂfld
↾s (Base‘(Scalar‘𝑋)))) |
| 16 | 13, 15 | eqeq12d 2753 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → ((Scalar‘𝑊) = (ℂfld
↾s (Base‘(Scalar‘𝑊))) ↔ (Scalar‘𝑋) = (ℂfld
↾s (Base‘(Scalar‘𝑋))))) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((Scalar‘𝑊) = (ℂfld
↾s (Base‘(Scalar‘𝑊))) ↔ (Scalar‘𝑋) = (ℂfld
↾s (Base‘(Scalar‘𝑋))))) |
| 18 | 12, 17 | mpbid 232 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (Scalar‘𝑋) = (ℂfld
↾s (Base‘(Scalar‘𝑋)))) |
| 19 | 5, 8, 18 | 3jca 1129 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (𝑋 ∈ PreHil ∧ 𝑋 ∈ NrmMod ∧ (Scalar‘𝑋) = (ℂfld
↾s (Base‘(Scalar‘𝑋))))) |
| 20 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑊 ∈ ℂPreHil) |
| 21 | | elinel1 4201 |
. . . . . . . . . . 11
⊢ (𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈
(Base‘(Scalar‘𝑊))) |
| 22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → 𝑞 ∈ (Base‘(Scalar‘𝑊))) |
| 23 | | elinel2 4202 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈
(0[,)+∞)) |
| 24 | | elrege0 13494 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (0[,)+∞) ↔
(𝑞 ∈ ℝ ∧ 0
≤ 𝑞)) |
| 25 | 24 | simplbi 497 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ (0[,)+∞) →
𝑞 ∈
ℝ) |
| 26 | 23, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 𝑞 ∈
ℝ) |
| 27 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → 𝑞 ∈ ℝ) |
| 28 | 24 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ (0[,)+∞) → 0
≤ 𝑞) |
| 29 | 23, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) → 0 ≤ 𝑞) |
| 30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → 0 ≤ 𝑞) |
| 31 | 22, 27, 30 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → (𝑞 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞)) |
| 32 | 9, 10 | cphsqrtcl 25218 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
(𝑞 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞)) → (√‘𝑞) ∈
(Base‘(Scalar‘𝑊))) |
| 33 | 20, 31, 32 | syl2anr 597 |
. . . . . . . 8
⊢ (((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆)) → (√‘𝑞) ∈ (Base‘(Scalar‘𝑊))) |
| 34 | | eleq1 2829 |
. . . . . . . . . 10
⊢
((√‘𝑞) =
𝑥 →
((√‘𝑞) ∈
(Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊)))) |
| 35 | 34 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → ((√‘𝑞) ∈
(Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊)))) |
| 36 | 35 | adantr 480 |
. . . . . . . 8
⊢ (((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆)) → ((√‘𝑞) ∈ (Base‘(Scalar‘𝑊)) ↔ 𝑥 ∈ (Base‘(Scalar‘𝑊)))) |
| 37 | 33, 36 | mpbid 232 |
. . . . . . 7
⊢ (((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) ∧ (𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
| 38 | 37 | ex 412 |
. . . . . 6
⊢ ((𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) ∧
(√‘𝑞) = 𝑥) → ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆) → 𝑥 ∈ (Base‘(Scalar‘𝑊)))) |
| 39 | 38 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥 → ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆) → 𝑥 ∈ (Base‘(Scalar‘𝑊)))) |
| 40 | | df-sqrt 15274 |
. . . . . . 7
⊢ √ =
(𝑥 ∈ ℂ ↦
(℩𝑐 ∈
ℂ ((𝑐↑2) = 𝑥 ∧ 0 ≤
(ℜ‘𝑐) ∧ (i
· 𝑐) ∉
ℝ+))) |
| 41 | 40 | funmpt2 6605 |
. . . . . 6
⊢ Fun
√ |
| 42 | | fvelima 6974 |
. . . . . 6
⊢ ((Fun
√ ∧ 𝑥 ∈
(√ “ ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)))) →
∃𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥) |
| 43 | 41, 42 | mpan 690 |
. . . . 5
⊢ (𝑥 ∈ (√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) →
∃𝑞 ∈
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))(√‘𝑞) = 𝑥) |
| 44 | 39, 43 | syl11 33 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (𝑥 ∈ (√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) → 𝑥 ∈
(Base‘(Scalar‘𝑊)))) |
| 45 | 44 | ssrdv 3989 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑊))) |
| 46 | 14 | ineq1d 4219 |
. . . . . 6
⊢ (𝑈 ∈ 𝑆 → ((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞)) =
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) |
| 47 | 46 | imaeq2d 6078 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) = (√ “
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞)))) |
| 48 | 47, 14 | sseq12d 4017 |
. . . 4
⊢ (𝑈 ∈ 𝑆 → ((√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑊)) ↔ (√ “
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑋)))) |
| 49 | 48 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((√ “
((Base‘(Scalar‘𝑊)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑊)) ↔ (√ “
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑋)))) |
| 50 | 45, 49 | mpbid 232 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (√ “
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑋))) |
| 51 | | cphlmod 25208 |
. . . . 5
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
LMod) |
| 52 | 3 | lsssubg 20955 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 53 | 51, 52 | sylan 580 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 54 | | eqid 2737 |
. . . . 5
⊢
(norm‘𝑊) =
(norm‘𝑊) |
| 55 | | eqid 2737 |
. . . . 5
⊢
(norm‘𝑋) =
(norm‘𝑋) |
| 56 | 2, 54, 55 | subgnm 24646 |
. . . 4
⊢ (𝑈 ∈ (SubGrp‘𝑊) → (norm‘𝑋) = ((norm‘𝑊) ↾ 𝑈)) |
| 57 | 53, 56 | syl 17 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (norm‘𝑋) = ((norm‘𝑊) ↾ 𝑈)) |
| 58 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 59 | | eqid 2737 |
. . . . . . . 8
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
| 60 | 58, 59, 54 | cphnmfval 25226 |
. . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
(norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑊)𝑏)))) |
| 61 | 60 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑊)𝑏)))) |
| 62 | 2, 59 | ressip 17389 |
. . . . . . . . . 10
⊢ (𝑈 ∈ 𝑆 →
(·𝑖‘𝑊) =
(·𝑖‘𝑋)) |
| 63 | 62 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) →
(·𝑖‘𝑊) =
(·𝑖‘𝑋)) |
| 64 | 63 | oveqd 7448 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (𝑏(·𝑖‘𝑊)𝑏) = (𝑏(·𝑖‘𝑋)𝑏)) |
| 65 | 64 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (√‘(𝑏(·𝑖‘𝑊)𝑏)) = (√‘(𝑏(·𝑖‘𝑋)𝑏))) |
| 66 | 65 | mpteq2dv 5244 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑊)𝑏))) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏)))) |
| 67 | 61, 66 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (norm‘𝑊) = (𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏)))) |
| 68 | 58, 3 | lssss 20934 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ (Base‘𝑊)) |
| 69 | 68 | adantl 481 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑈 ⊆ (Base‘𝑊)) |
| 70 | | dfss 3970 |
. . . . . 6
⊢ (𝑈 ⊆ (Base‘𝑊) ↔ 𝑈 = (𝑈 ∩ (Base‘𝑊))) |
| 71 | 69, 70 | sylib 218 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑈 = (𝑈 ∩ (Base‘𝑊))) |
| 72 | 67, 71 | reseq12d 5998 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((norm‘𝑊) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))) ↾ (𝑈 ∩ (Base‘𝑊)))) |
| 73 | 2, 58 | ressbas 17280 |
. . . . . 6
⊢ (𝑈 ∈ 𝑆 → (𝑈 ∩ (Base‘𝑊)) = (Base‘𝑋)) |
| 74 | 73 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (𝑈 ∩ (Base‘𝑊)) = (Base‘𝑋)) |
| 75 | 74 | reseq2d 5997 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))) ↾ (𝑈 ∩ (Base‘𝑊))) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))) ↾ (Base‘𝑋))) |
| 76 | 72, 75 | eqtrd 2777 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((norm‘𝑊) ↾ 𝑈) = ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))) ↾ (Base‘𝑋))) |
| 77 | 2, 58 | ressbasss 17284 |
. . . . 5
⊢
(Base‘𝑋)
⊆ (Base‘𝑊) |
| 78 | 77 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (Base‘𝑋) ⊆ (Base‘𝑊)) |
| 79 | 78 | resmptd 6058 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → ((𝑏 ∈ (Base‘𝑊) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))) ↾ (Base‘𝑋)) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏)))) |
| 80 | 57, 76, 79 | 3eqtrd 2781 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → (norm‘𝑋) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏)))) |
| 81 | | eqid 2737 |
. . 3
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 82 | | eqid 2737 |
. . 3
⊢
(·𝑖‘𝑋) =
(·𝑖‘𝑋) |
| 83 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝑋) =
(Scalar‘𝑋) |
| 84 | | eqid 2737 |
. . 3
⊢
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋)) |
| 85 | 81, 82, 55, 83, 84 | iscph 25204 |
. 2
⊢ (𝑋 ∈ ℂPreHil ↔
((𝑋 ∈ PreHil ∧
𝑋 ∈ NrmMod ∧
(Scalar‘𝑋) =
(ℂfld ↾s (Base‘(Scalar‘𝑋)))) ∧ (√ “
((Base‘(Scalar‘𝑋)) ∩ (0[,)+∞))) ⊆
(Base‘(Scalar‘𝑋)) ∧ (norm‘𝑋) = (𝑏 ∈ (Base‘𝑋) ↦ (√‘(𝑏(·𝑖‘𝑋)𝑏))))) |
| 86 | 19, 50, 80, 85 | syl3anbrc 1344 |
1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑈 ∈ 𝑆) → 𝑋 ∈ ℂPreHil) |