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