Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
2 | | csscld.c |
. . . . 5
⊢ 𝐶 = (CSubSp‘𝑊) |
3 | 1, 2 | cssi 19847 |
. . . 4
⊢ (𝑆 ∈ 𝐶 → 𝑆 = ((ocv‘𝑊)‘((ocv‘𝑊)‘𝑆))) |
4 | 3 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝑆 = ((ocv‘𝑊)‘((ocv‘𝑊)‘𝑆))) |
5 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑊) =
(Base‘𝑊) |
6 | 5, 1 | ocvss 19833 |
. . . . 5
⊢
((ocv‘𝑊)‘𝑆) ⊆ (Base‘𝑊) |
7 | | eqid 2610 |
. . . . . 6
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
8 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
9 | | eqid 2610 |
. . . . . 6
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
10 | 5, 7, 8, 9, 1 | ocvval 19830 |
. . . . 5
⊢
(((ocv‘𝑊)‘𝑆) ⊆ (Base‘𝑊) → ((ocv‘𝑊)‘((ocv‘𝑊)‘𝑆)) = {𝑥 ∈ (Base‘𝑊) ∣ ∀𝑦 ∈ ((ocv‘𝑊)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
11 | 6, 10 | mp1i 13 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → ((ocv‘𝑊)‘((ocv‘𝑊)‘𝑆)) = {𝑥 ∈ (Base‘𝑊) ∣ ∀𝑦 ∈ ((ocv‘𝑊)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
12 | | riinrab 4532 |
. . . 4
⊢
((Base‘𝑊)
∩ ∩ 𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = {𝑥 ∈ (Base‘𝑊) ∣ ∀𝑦 ∈ ((ocv‘𝑊)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} |
13 | 11, 12 | syl6eqr 2662 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → ((ocv‘𝑊)‘((ocv‘𝑊)‘𝑆)) = ((Base‘𝑊) ∩ ∩
𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
14 | | cphnlm 22780 |
. . . . . . . 8
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmMod) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝑊 ∈ NrmMod) |
16 | | nlmngp 22291 |
. . . . . . 7
⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp) |
17 | | ngptps 22216 |
. . . . . . 7
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝑊 ∈ TopSp) |
19 | | csscld.j |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝑊) |
20 | 5, 19 | istps 20551 |
. . . . . 6
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑊))) |
21 | 18, 20 | sylib 207 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝐽 ∈ (TopOn‘(Base‘𝑊))) |
22 | | toponuni 20542 |
. . . . 5
⊢ (𝐽 ∈
(TopOn‘(Base‘𝑊)) → (Base‘𝑊) = ∪ 𝐽) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → (Base‘𝑊) = ∪ 𝐽) |
24 | 23 | ineq1d 3775 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → ((Base‘𝑊) ∩ ∩
𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (∪ 𝐽 ∩
∩ 𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
25 | 4, 13, 24 | 3eqtrd 2648 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝑆 = (∪ 𝐽 ∩ ∩ 𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
26 | | topontop 20541 |
. . . 4
⊢ (𝐽 ∈
(TopOn‘(Base‘𝑊)) → 𝐽 ∈ Top) |
27 | 21, 26 | syl 17 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝐽 ∈ Top) |
28 | 6 | sseli 3564 |
. . . . 5
⊢ (𝑦 ∈ ((ocv‘𝑊)‘𝑆) → 𝑦 ∈ (Base‘𝑊)) |
29 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) ∈ V |
30 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) = (𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) |
31 | 30 | mptiniseg 5546 |
. . . . . . 7
⊢
((0g‘(Scalar‘𝑊)) ∈ V → (◡(𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
32 | 29, 31 | ax-mp 5 |
. . . . . 6
⊢ (◡(𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} |
33 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
34 | | simpll 786 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑊 ∈ ℂPreHil) |
35 | 21 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝐽 ∈ (TopOn‘(Base‘𝑊))) |
36 | 35 | cnmptid 21274 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥 ∈ (Base‘𝑊) ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
37 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑦 ∈ (Base‘𝑊)) |
38 | 35, 35, 37 | cnmptc 21275 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥 ∈ (Base‘𝑊) ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) |
39 | 19, 33, 7, 34, 35, 36, 38 | cnmpt1ip 22854 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
40 | 33 | cnfldhaus 22398 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Haus |
41 | | cphclm 22797 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
ℂMod) |
42 | 8 | clm0 22680 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘(Scalar‘𝑊))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ℂPreHil → 0 =
(0g‘(Scalar‘𝑊))) |
44 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → 0 =
(0g‘(Scalar‘𝑊))) |
45 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
46 | 44, 45 | syl6eqelr 2697 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) →
(0g‘(Scalar‘𝑊)) ∈ ℂ) |
47 | 33 | cnfldtopon 22396 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
48 | 47 | toponunii 20547 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
49 | 48 | sncld 20985 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧
(0g‘(Scalar‘𝑊)) ∈ ℂ) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) |
50 | 40, 46, 49 | sylancr 694 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) |
51 | | cnclima 20882 |
. . . . . . 7
⊢ (((𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn (TopOpen‘ℂfld))
∧ {(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) → (◡(𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
52 | 39, 50, 51 | syl2anc 691 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → (◡(𝑥 ∈ (Base‘𝑊) ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
53 | 32, 52 | syl5eqelr 2693 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ (Base‘𝑊)) → {𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) |
54 | 28, 53 | sylan2 490 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) ∧ 𝑦 ∈ ((ocv‘𝑊)‘𝑆)) → {𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) |
55 | 54 | ralrimiva 2949 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → ∀𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) |
56 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
57 | 56 | riincld 20658 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ∀𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∩
∩ 𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
58 | 27, 55, 57 | syl2anc 691 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → (∪ 𝐽 ∩ ∩ 𝑦 ∈ ((ocv‘𝑊)‘𝑆){𝑥 ∈ (Base‘𝑊) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
59 | 25, 58 | eqeltrd 2688 |
1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ∈ 𝐶) → 𝑆 ∈ (Clsd‘𝐽)) |