Step | Hyp | Ref
| Expression |
1 | | ocvss.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | | ocvss.o |
. . . 4
⊢ ⊥ =
(ocv‘𝑊) |
3 | 1, 2 | ocvss 20486 |
. . 3
⊢ ( ⊥
‘𝑆) ⊆ 𝑉 |
4 | 3 | a1i 11 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ⊆ 𝑉) |
5 | | simpr 488 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
6 | | phllmod 20446 |
. . . . . 6
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑊 ∈ LMod) |
8 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) |
9 | 1, 8 | lmod0vcl 19782 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ 𝑉) |
10 | 7, 9 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ 𝑉) |
11 | | simpll 767 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ PreHil) |
12 | 5 | sselda 3877 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) |
13 | | eqid 2738 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
15 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
16 | 13, 14, 1, 15, 8 | ip0l 20452 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
17 | 11, 12, 16 | syl2anc 587 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
18 | 17 | ralrimiva 3096 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
19 | 1, 14, 13, 15, 2 | elocv 20484 |
. . . 4
⊢
((0g‘𝑊) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ (0g‘𝑊) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
20 | 5, 10, 18, 19 | syl3anbrc 1344 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ ( ⊥ ‘𝑆)) |
21 | 20 | ne0d 4224 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ≠ ∅) |
22 | 5 | adantr 484 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑆 ⊆ 𝑉) |
23 | 7 | adantr 484 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑊 ∈ LMod) |
24 | | simpr1 1195 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
25 | | simpr2 1196 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ ( ⊥ ‘𝑆)) |
26 | 3, 25 | sseldi 3875 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ 𝑉) |
27 | | eqid 2738 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
28 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
29 | 1, 13, 27, 28 | lmodvscl 19770 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
30 | 23, 24, 26, 29 | syl3anc 1372 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
31 | | simpr3 1197 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ ( ⊥ ‘𝑆)) |
32 | 3, 31 | sseldi 3875 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ 𝑉) |
33 | | eqid 2738 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
34 | 1, 33 | lmodvacl 19767 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
35 | 23, 30, 32, 34 | syl3anc 1372 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
36 | 11 | adantlr 715 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ PreHil) |
37 | 30 | adantr 484 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
38 | 32 | adantr 484 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑧 ∈ 𝑉) |
39 | 12 | adantlr 715 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) |
40 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
41 | 13, 14, 1, 33, 40 | ipdir 20455 |
. . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ ((𝑟(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) |
42 | 36, 37, 38, 39, 41 | syl13anc 1373 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) |
43 | 24 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
44 | 26 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑦 ∈ 𝑉) |
45 | | eqid 2738 |
. . . . . . . . . 10
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
46 | 13, 14, 1, 28, 27, 45 | ipass 20461 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ (𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥))) |
47 | 36, 43, 44, 39, 46 | syl13anc 1373 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥))) |
48 | 1, 14, 13, 15, 2 | ocvi 20485 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
49 | 25, 48 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
50 | 49 | oveq2d 7186 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
51 | 23 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ LMod) |
52 | 13 | lmodring 19761 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (Scalar‘𝑊) ∈ Ring) |
54 | 28, 45, 15 | ringrz 19460 |
. . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
55 | 53, 43, 54 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
56 | 47, 50, 55 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
57 | 1, 14, 13, 15, 2 | ocvi 20485 |
. . . . . . . 8
⊢ ((𝑧 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
58 | 31, 57 | sylan 583 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
59 | 56, 58 | oveq12d 7188 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥)) = ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
60 | 13 | lmodfgrp 19762 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
61 | 28, 15 | grpidcl 18249 |
. . . . . . . 8
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
62 | 28, 40, 15 | grplid 18251 |
. . . . . . . 8
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
63 | 61, 62 | mpdan 687 |
. . . . . . 7
⊢
((Scalar‘𝑊)
∈ Grp → ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
64 | 51, 60, 63 | 3syl 18 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
65 | 42, 59, 64 | 3eqtrd 2777 |
. . . . 5
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
66 | 65 | ralrimiva 3096 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
67 | 1, 14, 13, 15, 2 | elocv 20484 |
. . . 4
⊢ (((𝑟(
·𝑠 ‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
68 | 22, 35, 66, 67 | syl3anbrc 1344 |
. . 3
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) |
69 | 68 | ralrimivvva 3104 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) |
70 | | ocvlss.l |
. . 3
⊢ 𝐿 = (LSubSp‘𝑊) |
71 | 13, 28, 1, 33, 27, 70 | islss 19825 |
. 2
⊢ (( ⊥
‘𝑆) ∈ 𝐿 ↔ (( ⊥ ‘𝑆) ⊆ 𝑉 ∧ ( ⊥ ‘𝑆) ≠ ∅ ∧
∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆))) |
72 | 4, 21, 69, 71 | syl3anbrc 1344 |
1
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ∈ 𝐿) |