Step | Hyp | Ref
| Expression |
1 | | cphngp 22781 |
. . . . . . . 8
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmGrp) |
2 | | ngptps 22216 |
. . . . . . . 8
⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
TopSp) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑊 ∈ TopSp) |
5 | | clsocv.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
6 | | clsocv.j |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝑊) |
7 | 5, 6 | istps 20551 |
. . . . . 6
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑉)) |
8 | 4, 7 | sylib 207 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝐽 ∈ (TopOn‘𝑉)) |
9 | | topontop 20541 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝐽 ∈ Top) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝐽 ∈ Top) |
11 | | simpr 476 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
12 | | toponuni 20542 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝑉 = ∪ 𝐽) |
13 | 8, 12 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑉 = ∪ 𝐽) |
14 | 11, 13 | sseqtrd 3604 |
. . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ ∪ 𝐽) |
15 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
16 | 15 | sscls 20670 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ⊆
((cls‘𝐽)‘𝑆)) |
17 | 10, 14, 16 | syl2anc 691 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
18 | | clsocv.o |
. . . 4
⊢ 𝑂 = (ocv‘𝑊) |
19 | 18 | ocv2ss 19836 |
. . 3
⊢ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆)) |
20 | 17, 19 | syl 17 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆)) |
21 | 15 | clsss3 20673 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
22 | 10, 14, 21 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
23 | 22, 13 | sseqtr4d 3605 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉) |
24 | 23 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉) |
25 | 5, 18 | ocvss 19833 |
. . . . . . 7
⊢ (𝑂‘𝑆) ⊆ 𝑉 |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘𝑆) ⊆ 𝑉) |
27 | 26 | sselda 3568 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ 𝑉) |
28 | | df-ss 3554 |
. . . . . . . . . . . 12
⊢
(((cls‘𝐽)‘𝑆) ⊆ 𝑉 ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆)) |
29 | 24, 28 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆)) |
30 | 29 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
31 | | dfrab3 3861 |
. . . . . . . . . . . 12
⊢ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
32 | 31 | ineq2i 3773 |
. . . . . . . . . . 11
⊢
(((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
33 | | inass 3785 |
. . . . . . . . . . 11
⊢
((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) |
34 | 32, 33 | eqtr4i 2635 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
35 | | dfrab3 3861 |
. . . . . . . . . 10
⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
36 | 30, 34, 35 | 3eqtr4g 2669 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
37 | 15 | clscld 20661 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) |
38 | 10, 14, 37 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) |
40 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑊)) ∈ V |
41 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) = (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) |
42 | 41 | mptiniseg 5546 |
. . . . . . . . . . . 12
⊢
((0g‘(Scalar‘𝑊)) ∈ V → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
43 | 40, 42 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} |
44 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
46 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑊 ∈ ℂPreHil) |
47 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝐽 ∈ (TopOn‘𝑉)) |
48 | 47, 47, 27 | cnmptc 21275 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
49 | 47 | cnmptid 21274 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) |
50 | 6, 44, 45, 46, 47, 48, 49 | cnmpt1ip 22854 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
51 | 44 | cnfldhaus 22398 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈ Haus |
52 | | cphclm 22797 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
ℂMod) |
53 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
54 | 53 | clm0 22680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘(Scalar‘𝑊))) |
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ ℂPreHil → 0 =
(0g‘(Scalar‘𝑊))) |
56 | 55 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 0 =
(0g‘(Scalar‘𝑊))) |
57 | | 0cn 9911 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
58 | 56, 57 | syl6eqelr 2697 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) →
(0g‘(Scalar‘𝑊)) ∈ ℂ) |
59 | 44 | cnfldtopon 22396 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
60 | 59 | toponunii 20547 |
. . . . . . . . . . . . . 14
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
61 | 60 | sncld 20985 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧
(0g‘(Scalar‘𝑊)) ∈ ℂ) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) |
62 | 51, 58, 61 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) |
63 | | cnclima 20882 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn (TopOpen‘ℂfld))
∧ {(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
64 | 50, 62, 63 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
65 | 43, 64 | syl5eqelr 2693 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) |
66 | | incld 20657 |
. . . . . . . . . 10
⊢
((((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽) ∧ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
67 | 39, 65, 66 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) |
68 | 36, 67 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) |
69 | 17 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
70 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
71 | 5, 45, 53, 70, 18 | ocvi 19832 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑂‘𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
72 | 71 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑂‘𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
73 | 72 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
74 | | ssrab 3643 |
. . . . . . . . 9
⊢ (𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) ∧ ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))) |
75 | 69, 73, 74 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
76 | 15 | clsss2 20686 |
. . . . . . . 8
⊢ (({𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) → ((cls‘𝐽)‘𝑆) ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
77 | 68, 75, 76 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
78 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆) |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆)) |
80 | 77, 79 | eqssd 3585 |
. . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) |
81 | | rabid2 3096 |
. . . . . 6
⊢
(((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
82 | 80, 81 | sylib 207 |
. . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
83 | 5, 45, 53, 70, 18 | elocv 19831 |
. . . . 5
⊢ (𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆)) ↔ (((cls‘𝐽)‘𝑆) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))) |
84 | 24, 27, 82, 83 | syl3anbrc 1239 |
. . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆))) |
85 | 84 | ex 449 |
. . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑥 ∈ (𝑂‘𝑆) → 𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆)))) |
86 | 85 | ssrdv 3574 |
. 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘𝑆) ⊆ (𝑂‘((cls‘𝐽)‘𝑆))) |
87 | 20, 86 | eqssd 3585 |
1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆)) |