| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cphngp 25208 | . . . . . . . 8
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
NrmGrp) | 
| 2 |  | ngptps 24616 | . . . . . . . 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 22941 | . . . . . 6
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑉)) | 
| 8 | 4, 7 | sylib 218 | . . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝐽 ∈ (TopOn‘𝑉)) | 
| 9 |  | topontop 22920 | . . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝐽 ∈ Top) | 
| 10 | 8, 9 | syl 17 | . . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝐽 ∈ Top) | 
| 11 |  | simpr 484 | . . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) | 
| 12 |  | toponuni 22921 | . . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝑉 = ∪ 𝐽) | 
| 13 | 8, 12 | syl 17 | . . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑉 = ∪ 𝐽) | 
| 14 | 11, 13 | sseqtrd 4019 | . . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ ∪ 𝐽) | 
| 15 |  | eqid 2736 | . . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 16 | 15 | sscls 23065 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ⊆
((cls‘𝐽)‘𝑆)) | 
| 17 | 10, 14, 16 | syl2anc 584 | . . 3
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) | 
| 18 |  | clsocv.o | . . . 4
⊢ 𝑂 = (ocv‘𝑊) | 
| 19 | 18 | ocv2ss 21692 | . . 3
⊢ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆)) | 
| 20 | 17, 19 | syl 17 | . 2
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆)) | 
| 21 | 15 | clsss3 23068 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) | 
| 22 | 10, 14, 21 | syl2anc 584 | . . . . 5
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) | 
| 23 | 22, 13 | sseqtrrd 4020 | . . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉) | 
| 24 | 23 | adantr 480 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉) | 
| 25 | 5, 18 | ocvss 21689 | . . . . 5
⊢ (𝑂‘𝑆) ⊆ 𝑉 | 
| 26 | 25 | a1i 11 | . . . 4
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘𝑆) ⊆ 𝑉) | 
| 27 | 26 | sselda 3982 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ 𝑉) | 
| 28 |  | dfss2 3968 | . . . . . . . . . 10
⊢
(((cls‘𝐽)‘𝑆) ⊆ 𝑉 ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆)) | 
| 29 | 24, 28 | sylib 218 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆)) | 
| 30 | 29 | ineq1d 4218 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) | 
| 31 |  | dfrab3 4318 | . . . . . . . . . 10
⊢ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 32 | 31 | ineq2i 4216 | . . . . . . . . 9
⊢
(((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) | 
| 33 |  | inass 4227 | . . . . . . . . 9
⊢
((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})) | 
| 34 | 32, 33 | eqtr4i 2767 | . . . . . . . 8
⊢
(((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 35 |  | dfrab3 4318 | . . . . . . . 8
⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 36 | 30, 34, 35 | 3eqtr4g 2801 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 37 | 15 | clscld 23056 | . . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | 
| 38 | 10, 14, 37 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | 
| 39 | 38 | adantr 480 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | 
| 40 |  | fvex 6918 | . . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑊)) ∈ V | 
| 41 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) = (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) | 
| 42 | 41 | mptiniseg 6258 | . . . . . . . . . 10
⊢
((0g‘(Scalar‘𝑊)) ∈ V → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 43 | 40, 42 | ax-mp 5 | . . . . . . . . 9
⊢ (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} | 
| 44 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 45 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) | 
| 46 |  | simpll 766 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑊 ∈ ℂPreHil) | 
| 47 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝐽 ∈ (TopOn‘𝑉)) | 
| 48 | 47, 47, 27 | cnmptc 23671 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | 
| 49 | 47 | cnmptid 23670 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑦) ∈ (𝐽 Cn 𝐽)) | 
| 50 | 6, 44, 45, 46, 47, 48, 49 | cnmpt1ip 25282 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) | 
| 51 | 44 | cnfldhaus 24806 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Haus | 
| 52 |  | cphclm 25224 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
ℂMod) | 
| 53 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 54 | 53 | clm0 25106 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘(Scalar‘𝑊))) | 
| 55 | 52, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ ℂPreHil → 0 =
(0g‘(Scalar‘𝑊))) | 
| 56 | 55 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 0 =
(0g‘(Scalar‘𝑊))) | 
| 57 |  | 0cn 11254 | . . . . . . . . . . . 12
⊢ 0 ∈
ℂ | 
| 58 | 56, 57 | eqeltrrdi 2849 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) →
(0g‘(Scalar‘𝑊)) ∈ ℂ) | 
| 59 |  | unicntop 24807 | . . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 60 | 59 | sncld 23380 | . . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧
(0g‘(Scalar‘𝑊)) ∈ ℂ) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) | 
| 61 | 51, 58, 60 | sylancr 587 | . . . . . . . . . 10
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) →
{(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) | 
| 62 |  | cnclima 23277 | . . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn (TopOpen‘ℂfld))
∧ {(0g‘(Scalar‘𝑊))} ∈
(Clsd‘(TopOpen‘ℂfld))) → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) | 
| 63 | 50, 61, 62 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “
{(0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) | 
| 64 | 43, 63 | eqeltrrid 2845 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) | 
| 65 |  | incld 23052 | . . . . . . . 8
⊢
((((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽) ∧ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) | 
| 66 | 39, 64, 65 | syl2anc 584 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) ∈ (Clsd‘𝐽)) | 
| 67 | 36, 66 | eqeltrrd 2841 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽)) | 
| 68 | 17 | adantr 480 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) | 
| 69 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 70 | 5, 45, 53, 69, 18 | ocvi 21688 | . . . . . . . . 9
⊢ ((𝑥 ∈ (𝑂‘𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) | 
| 71 | 70 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝑥 ∈ (𝑂‘𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) | 
| 72 | 71 | adantl 481 | . . . . . . 7
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) | 
| 73 |  | ssrab 4072 | . . . . . . 7
⊢ (𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) ∧ ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))) | 
| 74 | 68, 72, 73 | sylanbrc 583 | . . . . . 6
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 75 | 15 | clsss2 23081 | . . . . . 6
⊢ (({𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) → ((cls‘𝐽)‘𝑆) ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 76 | 67, 74, 75 | syl2anc 584 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 77 |  | ssrab2 4079 | . . . . . 6
⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆) | 
| 78 | 77 | a1i 11 | . . . . 5
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆)) | 
| 79 | 76, 78 | eqssd 4000 | . . . 4
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) | 
| 80 |  | rabid2 3469 | . . . 4
⊢
(((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) | 
| 81 | 79, 80 | sylib 218 | . . 3
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) | 
| 82 | 5, 45, 53, 69, 18 | elocv 21687 | . . 3
⊢ (𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆)) ↔ (((cls‘𝐽)‘𝑆) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))) | 
| 83 | 24, 27, 81, 82 | syl3anbrc 1343 | . 2
⊢ (((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆))) | 
| 84 | 20, 83 | eqelssd 4004 | 1
⊢ ((𝑊 ∈ ℂPreHil ∧
𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆)) |