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