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	⊢ ( 𝜑 → 𝑆 ∈ 𝐶 )