Theorem clsocv 24486

Description: The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.)

Hypotheses

Ref	Expression
clsocv.v	⊢ 𝑉 = (Base‘𝑊)
clsocv.o	⊢ 𝑂 = (ocv‘𝑊)
clsocv.j	⊢ 𝐽 = (TopOpen‘𝑊)

Assertion

Ref	Expression
clsocv	⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆))

Proof of Theorem clsocv

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cphngp 24409	. . . . . . . 8 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
2		ngptps 23830	. . . . . . . 8 ⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ TopSp)
4	3	adantr 481	. . . . . 6 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝑊 ∈ TopSp)
5		clsocv.v	. . . . . . 7 ⊢ 𝑉 = (Base‘𝑊)
6		clsocv.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘𝑊)
7	5, 6	istps 22155	. . . . . 6 ⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑉))
8	4, 7	sylib 217	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝐽 ∈ (TopOn‘𝑉))
9		topontop 22134	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝐽 ∈ Top)
10	8, 9	syl 17	. . . 4 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝐽 ∈ Top)
11		simpr 485	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉)
12		toponuni 22135	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑉) → 𝑉 = ∪ 𝐽)
13	8, 12	syl 17	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝑉 = ∪ 𝐽)
14	11, 13	sseqtrd 3971	. . . 4 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ ∪ 𝐽)
15		eqid 2737	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
16	15	sscls 22279	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
17	10, 14, 16	syl2anc 584	. . 3 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
18		clsocv.o	. . . 4 ⊢ 𝑂 = (ocv‘𝑊)
19	18	ocv2ss 20950	. . 3 ⊢ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆))
20	17, 19	syl 17	. 2 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) ⊆ (𝑂‘𝑆))
21	15	clsss3 22282	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
22	10, 14, 21	syl2anc 584	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽)
23	22, 13	sseqtrrd 3972	. . . 4 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉)
24	23	adantr 481	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ⊆ 𝑉)
25	5, 18	ocvss 20947	. . . . 5 ⊢ (𝑂‘𝑆) ⊆ 𝑉
26	25	a1i 11	. . . 4 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘𝑆) ⊆ 𝑉)
27	26	sselda 3931	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ 𝑉)
28		df-ss 3914	. . . . . . . . . 10 ⊢ (((cls‘𝐽)‘𝑆) ⊆ 𝑉 ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆))
29	24, 28	sylib 217	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ 𝑉) = ((cls‘𝐽)‘𝑆))
30	29	ineq1d 4156	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}))
31		dfrab3 4254	. . . . . . . . . 10 ⊢ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
32	31	ineq2i 4154	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}))
33		inass 4164	. . . . . . . . 9 ⊢ ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = (((cls‘𝐽)‘𝑆) ∩ (𝑉 ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}))
34	32, 33	eqtr4i 2768	. . . . . . . 8 ⊢ (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = ((((cls‘𝐽)‘𝑆) ∩ 𝑉) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
35		dfrab3 4254	. . . . . . . 8 ⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} = (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
36	30, 34, 35	3eqtr4g 2802	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (((cls‘𝐽)‘𝑆) ∩ {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
37	15	clscld 22270	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
38	10, 14, 37	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
39	38	adantr 481	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
40		fvex 6824	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘𝑊)) ∈ V
41		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) = (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦))
42	41	mptiniseg 6164	. . . . . . . . . 10 ⊢ ((0g‘(Scalar‘𝑊)) ∈ V → (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “ {(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
43	40, 42	ax-mp 5	. . . . . . . . 9 ⊢ (◡(𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) “ {(0g‘(Scalar‘𝑊))}) = {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))}
44		eqid 2737	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
45		eqid 2737	. . . . . . . . . . 11 ⊢ (·𝑖‘𝑊) = (·𝑖‘𝑊)
46		simpll 764	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑊 ∈ ℂPreHil)
47	8	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝐽 ∈ (TopOn‘𝑉))
48	47, 47, 27	cnmptc 22885	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑥) ∈ (𝐽 Cn 𝐽))
49	47	cnmptid 22884	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ 𝑦) ∈ (𝐽 Cn 𝐽))
50	6, 44, 45, 46, 47, 48, 49	cnmpt1ip 24483	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (𝑦 ∈ 𝑉 ↦ (𝑥(·𝑖‘𝑊)𝑦)) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
51	44	cnfldhaus 24020	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂfld) ∈ Haus
52		cphclm 24425	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
53		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
54	53	clm0 24307	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘(Scalar‘𝑊)))
55	52, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ ℂPreHil → 0 = (0g‘(Scalar‘𝑊)))
56	55	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 0 = (0g‘(Scalar‘𝑊)))
57		0cn 11040	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
58	56, 57	eqeltrrdi 2847	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → (0g‘(Scalar‘𝑊)) ∈ ℂ)
59		unicntop 24021	. . . . . . . . . . . 12 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
60	59	sncld 22594	. . . . . . . . . . 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 22491	. . . . . . . . . 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 2843	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ 𝑉 ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽))
65		incld 22266	. . . . . . . 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 2839	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ∈ (Clsd‘𝐽))
68	17	adantr 481	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
69		eqid 2737	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
70	5, 45, 53, 69, 18	ocvi 20946	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝑂‘𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
71	70	ralrimiva 3140	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑂‘𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
72	71	adantl 482	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
73		ssrab 4017	. . . . . . 7 ⊢ (𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ (𝑆 ⊆ ((cls‘𝐽)‘𝑆) ∧ ∀𝑦 ∈ 𝑆 (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
74	68, 72, 73	sylanbrc 583	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑆 ⊆ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
75	15	clsss2 22295	. . . . . 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 4024	. . . . . 6 ⊢ {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆)
78	77	a1i 11	. . . . 5 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ⊆ ((cls‘𝐽)‘𝑆))
79	76, 78	eqssd 3948	. . . 4 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))})
80		rabid2 3432	. . . 4 ⊢ (((cls‘𝐽)‘𝑆) = {𝑦 ∈ ((cls‘𝐽)‘𝑆) ∣ (𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))} ↔ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
81	79, 80	sylib 217	. . 3 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
82	5, 45, 53, 69, 18	elocv 20945	. . 3 ⊢ (𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆)) ↔ (((cls‘𝐽)‘𝑆) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
83	24, 27, 81, 82	syl3anbrc 1342	. 2 ⊢ (((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ (𝑂‘𝑆)) → 𝑥 ∈ (𝑂‘((cls‘𝐽)‘𝑆)))
84	20, 83	eqelssd 3952	1 ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  {cab 2714  ∀wral 3062  {crab 3404  Vcvv 3441   ∩ cin 3896   ⊆ wss 3897  {csn 4571  ∪ cuni 4850   ↦ cmpt 5170  ^◡ccnv 5606   “ cima 5610  ‘cfv 6465  (class class class)co 7315  ℂcc 10942  0cc0 10944  Basecbs 16982  Scalarcsca 17035  ·_𝑖cip 17037  TopOpenctopn 17202  0_gc0g 17220  ℂ_fldccnfld 20669  ocvcocv 20937  Topctop 22114  TopOnctopon 22131  TopSpctps 22153  Clsdccld 22239  clsccl 22241   Cn ccn 22447  Hauscha 22531  NrmGrpcngp 23805  ℂModcclm 24297  ℂPreHilccph 24402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022  ax-addf 11023  ax-mulf 11024

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-tpos 8089  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-2o 8345  df-er 8546  df-map 8665  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-fi 9240  df-sup 9271  df-inf 9272  df-oi 9339  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-z 12393  df-dec 12511  df-uz 12656  df-q 12762  df-rp 12804  df-xneg 12921  df-xadd 12922  df-xmul 12923  df-ico 13158  df-icc 13159  df-fz 13313  df-fzo 13456  df-seq 13795  df-exp 13856  df-hash 14118  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-rest 17203  df-topn 17204  df-0g 17222  df-gsum 17223  df-topgen 17224  df-pt 17225  df-prds 17228  df-xrs 17283  df-qtop 17288  df-imas 17289  df-xps 17291  df-mre 17365  df-mrc 17366  df-acs 17368  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-mhm 18500  df-submnd 18501  df-grp 18649  df-minusg 18650  df-sbg 18651  df-mulg 18770  df-subg 18821  df-ghm 18901  df-cntz 18992  df-cmn 19456  df-abl 19457  df-mgp 19789  df-ur 19806  df-ring 19853  df-cring 19854  df-oppr 19930  df-dvdsr 19951  df-unit 19952  df-invr 19982  df-dvr 19993  df-rnghom 20027  df-drng 20065  df-subrg 20094  df-staf 20177  df-srng 20178  df-lmod 20197  df-lmhm 20356  df-lvec 20437  df-sra 20506  df-rgmod 20507  df-psmet 20661  df-xmet 20662  df-met 20663  df-bl 20664  df-mopn 20665  df-cnfld 20670  df-phl 20903  df-ipf 20904  df-ocv 20940  df-top 22115  df-topon 22132  df-topsp 22154  df-bases 22168  df-cld 22242  df-cls 22244  df-cn 22450  df-cnp 22451  df-t1 22537  df-haus 22538  df-tx 22785  df-hmeo 22978  df-xms 23545  df-ms 23546  df-tms 23547  df-nm 23810  df-ngp 23811  df-tng 23812  df-nlm 23814  df-clm 24298  df-cph 24404  df-tcph 24405

This theorem is referenced by: (None)