Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . . . 5
⊢ (𝑊 ∈ (PreHil ∩ NrmMod)
↔ (𝑊 ∈ PreHil
∧ 𝑊 ∈
NrmMod)) |
2 | 1 | anbi1i 727 |
. . . 4
⊢ ((𝑊 ∈ (PreHil ∩ NrmMod)
∧ 𝐹 =
(ℂfld ↾s 𝐾)) ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod) ∧ 𝐹 = (ℂfld
↾s 𝐾))) |
3 | | df-3an 1033 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))
↔ ((𝑊 ∈ PreHil
∧ 𝑊 ∈ NrmMod)
∧ 𝐹 =
(ℂfld ↾s 𝐾))) |
4 | 2, 3 | bitr4i 266 |
. . 3
⊢ ((𝑊 ∈ (PreHil ∩ NrmMod)
∧ 𝐹 =
(ℂfld ↾s 𝐾)) ↔ (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))) |
5 | 4 | anbi1i 727 |
. 2
⊢ (((𝑊 ∈ (PreHil ∩ NrmMod)
∧ 𝐹 =
(ℂfld ↾s 𝐾)) ∧ ((√ “ (𝐾 ∩ (0[,)+∞))) ⊆
𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))
∧ ((√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))) |
6 | | fvex 6113 |
. . . . . 6
⊢
(Scalar‘𝑤)
∈ V |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V) |
8 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑓)
∈ V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) ∈ V) |
10 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑓 = (Scalar‘𝑤)) |
11 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑤 = 𝑊) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Scalar‘𝑤) = (Scalar‘𝑊)) |
13 | | iscph.f |
. . . . . . . . . . 11
⊢ 𝐹 = (Scalar‘𝑊) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Scalar‘𝑤) = 𝐹) |
15 | 10, 14 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑓 = 𝐹) |
16 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑘 = (Base‘𝑓)) |
17 | 15 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Base‘𝑓) = (Base‘𝐹)) |
18 | | iscph.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (Base‘𝐹) |
19 | 17, 18 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Base‘𝑓) = 𝐾) |
20 | 16, 19 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑘 = 𝐾) |
21 | 20 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (ℂfld
↾s 𝑘) =
(ℂfld ↾s 𝐾)) |
22 | 15, 21 | eqeq12d 2625 |
. . . . . . . 8
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑓 = (ℂfld ↾s
𝑘) ↔ 𝐹 = (ℂfld
↾s 𝐾))) |
23 | 20 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑘 ∩ (0[,)+∞)) = (𝐾 ∩ (0[,)+∞))) |
24 | 23 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (√ “ (𝑘 ∩ (0[,)+∞))) =
(√ “ (𝐾 ∩
(0[,)+∞)))) |
25 | 24, 20 | sseq12d 3597 |
. . . . . . . 8
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((√ “ (𝑘 ∩ (0[,)+∞))) ⊆
𝑘 ↔ (√ “
(𝐾 ∩ (0[,)+∞)))
⊆ 𝐾)) |
26 | 11 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (norm‘𝑤) = (norm‘𝑊)) |
27 | | iscph.n |
. . . . . . . . . 10
⊢ 𝑁 = (norm‘𝑊) |
28 | 26, 27 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (norm‘𝑤) = 𝑁) |
29 | 11 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Base‘𝑤) = (Base‘𝑊)) |
30 | | iscph.v |
. . . . . . . . . . 11
⊢ 𝑉 = (Base‘𝑊) |
31 | 29, 30 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (Base‘𝑤) = 𝑉) |
32 | 11 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) →
(·𝑖‘𝑤) =
(·𝑖‘𝑊)) |
33 | | iscph.h |
. . . . . . . . . . . . 13
⊢ , =
(·𝑖‘𝑊) |
34 | 32, 33 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) →
(·𝑖‘𝑤) = , ) |
35 | 34 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑥(·𝑖‘𝑤)𝑥) = (𝑥 , 𝑥)) |
36 | 35 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (√‘(𝑥(·𝑖‘𝑤)𝑥)) = (√‘(𝑥 , 𝑥))) |
37 | 31, 36 | mpteq12dv 4663 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))) = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) |
38 | 28, 37 | eqeq12d 2625 |
. . . . . . . 8
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))) ↔ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) |
39 | 22, 25, 38 | 3anbi123d 1391 |
. . . . . . 7
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((𝑓 = (ℂfld ↾s
𝑘) ∧ (√ “
(𝑘 ∩ (0[,)+∞)))
⊆ 𝑘 ∧
(norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))) ↔ (𝐹 = (ℂfld ↾s
𝐾) ∧ (√ “
(𝐾 ∩ (0[,)+∞)))
⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))) |
40 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝐹 = (ℂfld
↾s 𝐾)
∧ (√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ ((√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))) |
41 | 39, 40 | syl6bb 275 |
. . . . . 6
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((𝑓 = (ℂfld ↾s
𝑘) ∧ (√ “
(𝑘 ∩ (0[,)+∞)))
⊆ 𝑘 ∧
(norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))) ↔ (𝐹 = (ℂfld ↾s
𝐾) ∧ ((√ “
(𝐾 ∩ (0[,)+∞)))
⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))))) |
42 | 9, 41 | sbcied 3439 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ([(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ (√ “
(𝑘 ∩ (0[,)+∞)))
⊆ 𝑘 ∧
(norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))) ↔ (𝐹 = (ℂfld ↾s
𝐾) ∧ ((√ “
(𝐾 ∩ (0[,)+∞)))
⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))))) |
43 | 7, 42 | sbcied 3439 |
. . . 4
⊢ (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ (√ “
(𝑘 ∩ (0[,)+∞)))
⊆ 𝑘 ∧
(norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))) ↔ (𝐹 = (ℂfld ↾s
𝐾) ∧ ((√ “
(𝐾 ∩ (0[,)+∞)))
⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))))) |
44 | | df-cph 22776 |
. . . 4
⊢
ℂPreHil = {𝑤
∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ (√ “
(𝑘 ∩ (0[,)+∞)))
⊆ 𝑘 ∧
(norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))} |
45 | 43, 44 | elrab2 3333 |
. . 3
⊢ (𝑊 ∈ ℂPreHil ↔
(𝑊 ∈ (PreHil ∩
NrmMod) ∧ (𝐹 =
(ℂfld ↾s 𝐾) ∧ ((√ “ (𝐾 ∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))))) |
46 | | anass 679 |
. . 3
⊢ (((𝑊 ∈ (PreHil ∩ NrmMod)
∧ 𝐹 =
(ℂfld ↾s 𝐾)) ∧ ((√ “ (𝐾 ∩ (0[,)+∞))) ⊆
𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) ↔ (𝑊 ∈ (PreHil ∩ NrmMod) ∧ (𝐹 = (ℂfld
↾s 𝐾)
∧ ((√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))))) |
47 | 45, 46 | bitr4i 266 |
. 2
⊢ (𝑊 ∈ ℂPreHil ↔
((𝑊 ∈ (PreHil ∩
NrmMod) ∧ 𝐹 =
(ℂfld ↾s 𝐾)) ∧ ((√ “ (𝐾 ∩ (0[,)+∞))) ⊆
𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))) |
48 | | 3anass 1035 |
. 2
⊢ (((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))
∧ (√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))
∧ ((√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))))) |
49 | 5, 47, 48 | 3bitr4i 291 |
1
⊢ (𝑊 ∈ ℂPreHil ↔
((𝑊 ∈ PreHil ∧
𝑊 ∈ NrmMod ∧ 𝐹 = (ℂfld
↾s 𝐾))
∧ (√ “ (𝐾
∩ (0[,)+∞))) ⊆ 𝐾 ∧ 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))) |