Metamath Proof Explorer

Theorem lsmcss

Description: A subset of a pre-Hilbert space whose double orthocomplement has a projection decomposition is a closed subspace. This is the core of the proof that a topologically closed subspace is algebraically closed in a Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses lsmcss.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
lsmcss.j ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmcss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
lsmcss.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmcss.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
lsmcss.2 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
lsmcss.3 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( 𝑆 ⊕ ( ⊥ ‘ 𝑆 ) ) )
Assertion lsmcss ( 𝜑 → 𝑆 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 lsmcss.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
2 lsmcss.j ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 lsmcss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
4 lsmcss.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lsmcss.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
6 lsmcss.2 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
7 lsmcss.3 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ ( 𝑆 ⊕ ( ⊥ ‘ 𝑆 ) ) )
8 7 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ ( 𝑆 ⊕ ( ⊥ ‘ 𝑆 ) ) ) )
9 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
10 5 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 2 3 ocvss ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
12 11 a1i ⊢ ( 𝜑 → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
13 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
14 2 13 4 lsmelvalx ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ) → ( 𝑥 ∈ ( 𝑆 ⊕ ( ⊥ ‘ 𝑆 ) ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
15 10 6 12 14 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ⊕ ( ⊥ ‘ 𝑆 ) ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
16 8 15 sylibd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ PreHil )
18 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑆 ⊆ 𝑉 )
19 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝑆 )
20 18 19 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝑉 )
21 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ ( ⊥ ‘ 𝑆 ) )
22 11 21 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ 𝑉 )
23 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
24 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
25 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
26 23 24 2 13 25 ipdir ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) )
27 17 20 22 22 26 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) )
28 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
29 2 24 23 28 3 ocvi ⊢ ( ( 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
30 21 19 29 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
31 23 24 2 28 iporthcom ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
32 17 22 20 31 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
33 30 32 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
34 33 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) )
35 17 9 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ LMod )
36 23 lmodfgrp ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
37 35 36 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
38 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
39 23 24 2 38 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
40 17 22 22 39 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
41 38 25 28 grplid ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) )
42 37 40 41 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) ) = ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) )
43 27 34 42 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) )
44 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
45 2 24 23 28 3 ocvi ⊢ ( ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
46 44 21 45 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
47 43 46 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
48 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
49 23 24 2 28 48 ipeq0 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑧 = ( 0g ‘ 𝑊 ) ) )
50 17 22 49 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑧 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑧 = ( 0g ‘ 𝑊 ) ) )
51 47 50 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 = ( 0g ‘ 𝑊 ) )
52 51 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
53 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
54 10 53 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ Grp )
56 2 13 48 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑦 ∈ 𝑉 ) → ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑦 )
57 55 20 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑦 )
58 52 57 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = 𝑦 )
59 58 19 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑆 )
60 59 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑆 ) )
61 eleq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
62 eleq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑥 ∈ 𝑆 ↔ ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑆 ) )
63 61 62 imbi12d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑆 ) ↔ ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑆 ) ) )
64 60 63 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑆 ) ) )
65 64 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑆 ∃ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑆 ) ) )
66 16 65 syld ⊢ ( 𝜑 → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑆 ) ) )
67 66 pm2.43d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑆 ) )
68 67 ssrdv ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 )
69 2 1 3 iscss2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )
70 5 6 69 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )
71 68 70 mpbird ⊢ ( 𝜑 → 𝑆 ∈ 𝐶 )