Metamath Proof Explorer

Theorem clsocv

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)

Ref Expression
Hypotheses clsocv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clsocv.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
clsocv.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion clsocv ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑂 ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 clsocv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clsocv.o ⊢ 𝑂 = ( ocv ‘ 𝑊 )
3 clsocv.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
5 ngptps ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp )
6 4 5 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ TopSp )
7 6 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑊 ∈ TopSp )
8 1 3 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑉 ) )
9 7 8 sylib ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝐽 ∈ ( TopOn ‘ 𝑉 ) )
10 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑉 ) → 𝐽 ∈ Top )
11 9 10 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝐽 ∈ Top )
12 simpr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
13 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑉 ) → 𝑉 = ∪ 𝐽 )
14 9 13 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑉 = ∪ 𝐽 )
15 12 14 sseqtrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ∪ 𝐽 )
16 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
17 16 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
18 11 15 17 syl2anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
19 2 ocv2ss ⊢ ( 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( 𝑂 ‘ 𝑆 ) )
20 18 19 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( 𝑂 ‘ 𝑆 ) )
21 16 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
22 11 15 21 syl2anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
23 22 14 sseqtrrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑉 )
24 23 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑉 )
25 1 2 ocvss ⊢ ( 𝑂 ‘ 𝑆 ) ⊆ 𝑉
26 25 a1i ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑂 ‘ 𝑆 ) ⊆ 𝑉 )
27 26 sselda ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝑥 ∈ 𝑉 )
28 df-ss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑉 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑉 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
29 24 28 sylib ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑉 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
30 29 ineq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑉 ) ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
31 dfrab3 ⊢ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } = ( 𝑉 ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
32 31 ineq2i ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( 𝑉 ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
33 inass ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑉 ) ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( 𝑉 ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
34 32 33 eqtr4i ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑉 ) ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
35 dfrab3 ⊢ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
36 30 34 35 3eqtr4g ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
37 16 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
38 11 15 37 syl2anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
39 38 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
40 fvex ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ V
41 eqid ⊢ ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
42 41 mptiniseg ⊢ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ V → ( ◡ ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
43 40 42 ax-mp ⊢ ( ◡ ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) }
44 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
45 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
46 simpll ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝑊 ∈ ℂPreHil )
47 9 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑉 ) )
48 47 47 27 cnmptc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( 𝑦 ∈ 𝑉 ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
49 47 cnmptid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( 𝑦 ∈ 𝑉 ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
50 3 44 45 46 47 48 49 cnmpt1ip ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
51 44 cnfldhaus ⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
52 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
53 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
54 53 clm0 ⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
55 52 54 syl ⊢ ( 𝑊 ∈ ℂPreHil → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
56 55 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
57 0cn ⊢ 0 ∈ ℂ
58 56 57 eqeltrrdi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ℂ )
59 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
60 59 sncld ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Haus ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ℂ ) → { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
61 51 58 60 sylancr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
62 cnclima ⊢ ( ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ∧ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) → ( ◡ ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
63 50 61 62 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ◡ ( 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
64 43 63 eqeltrrid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) )
65 incld ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ∧ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
66 39 64 65 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ { 𝑦 ∈ 𝑉 ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
67 36 66 eqeltrrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) )
68 18 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
69 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
70 1 45 53 69 2 ocvi ⊢ ( ( 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
71 70 ralrimiva ⊢ ( 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
72 71 adantl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
73 ssrab ⊢ ( 𝑆 ⊆ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ↔ ( 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
74 68 72 73 sylanbrc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝑆 ⊆ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
75 16 clsss2 ⊢ ( ( { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
76 67 74 75 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
77 ssrab2 ⊢ { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 )
78 77 a1i ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
79 76 78 eqssd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
80 rabid2 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ↔ ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
81 79 80 sylib ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
82 1 45 53 69 2 elocv ⊢ ( 𝑥 ∈ ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
83 24 27 81 82 syl3anbrc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ ( 𝑂 ‘ 𝑆 ) ) → 𝑥 ∈ ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
84 20 83 eqelssd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑂 ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑂 ‘ 𝑆 ) )