Step | Hyp | Ref
| Expression |
1 | | ocvss.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | | ocvss.o |
. . . 4
⊢ ⊥ =
(ocv‘𝑊) |
3 | 1, 2 | ocvss 20014 |
. . 3
⊢ ( ⊥
‘𝑆) ⊆ 𝑉 |
4 | 3 | a1i 11 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ⊆ 𝑉) |
5 | | simpr 477 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
6 | | phllmod 19975 |
. . . . . 6
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑊 ∈ LMod) |
8 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) |
9 | 1, 8 | lmod0vcl 18892 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ 𝑉) |
10 | 7, 9 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ 𝑉) |
11 | | simpll 790 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ PreHil) |
12 | 5 | sselda 3603 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) |
13 | | eqid 2622 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
14 | | eqid 2622 |
. . . . . . 7
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
15 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
16 | 13, 14, 1, 15, 8 | ip0l 19981 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
17 | 11, 12, 16 | syl2anc 693 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
18 | 17 | ralrimiva 2966 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
19 | 1, 14, 13, 15, 2 | elocv 20012 |
. . . 4
⊢
((0g‘𝑊) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ (0g‘𝑊) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
20 | 5, 10, 18, 19 | syl3anbrc 1246 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ ( ⊥ ‘𝑆)) |
21 | | ne0i 3921 |
. . 3
⊢
((0g‘𝑊) ∈ ( ⊥ ‘𝑆) → ( ⊥ ‘𝑆) ≠ ∅) |
22 | 20, 21 | syl 17 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ≠ ∅) |
23 | 5 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑆 ⊆ 𝑉) |
24 | 7 | adantr 481 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑊 ∈ LMod) |
25 | | simpr1 1067 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
26 | | simpr2 1068 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ ( ⊥ ‘𝑆)) |
27 | 3, 26 | sseldi 3601 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ 𝑉) |
28 | | eqid 2622 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
29 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
30 | 1, 13, 28, 29 | lmodvscl 18880 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
31 | 24, 25, 27, 30 | syl3anc 1326 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
32 | | simpr3 1069 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ ( ⊥ ‘𝑆)) |
33 | 3, 32 | sseldi 3601 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ 𝑉) |
34 | | eqid 2622 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
35 | 1, 34 | lmodvacl 18877 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
36 | 24, 31, 33, 35 | syl3anc 1326 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉) |
37 | 11 | adantlr 751 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ PreHil) |
38 | 31 | adantr 481 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) |
39 | 33 | adantr 481 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑧 ∈ 𝑉) |
40 | 12 | adantlr 751 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) |
41 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
42 | 13, 14, 1, 34, 41 | ipdir 19984 |
. . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ ((𝑟(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) |
43 | 37, 38, 39, 40, 42 | syl13anc 1328 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) |
44 | 25 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
45 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑦 ∈ 𝑉) |
46 | | eqid 2622 |
. . . . . . . . . 10
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
47 | 13, 14, 1, 29, 28, 46 | ipass 19990 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ (𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥))) |
48 | 37, 44, 45, 40, 47 | syl13anc 1328 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥))) |
49 | 1, 14, 13, 15, 2 | ocvi 20013 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
50 | 26, 49 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
51 | 50 | oveq2d 6666 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
52 | 24 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ LMod) |
53 | 13 | lmodring 18871 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (Scalar‘𝑊) ∈ Ring) |
55 | 29, 46, 15 | ringrz 18588 |
. . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
56 | 54, 44, 55 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
57 | 48, 51, 56 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
58 | 1, 14, 13, 15, 2 | ocvi 20013 |
. . . . . . . 8
⊢ ((𝑧 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
59 | 32, 58 | sylan 488 |
. . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
60 | 57, 59 | oveq12d 6668 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥)) = ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
61 | 13 | lmodfgrp 18872 |
. . . . . . 7
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
62 | 29, 15 | grpidcl 17450 |
. . . . . . . 8
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
63 | 29, 41, 15 | grplid 17452 |
. . . . . . . 8
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
64 | 62, 63 | mpdan 702 |
. . . . . . 7
⊢
((Scalar‘𝑊)
∈ Grp → ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
65 | 52, 61, 64 | 3syl 18 |
. . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
66 | 43, 60, 65 | 3eqtrd 2660 |
. . . . 5
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
67 | 66 | ralrimiva 2966 |
. . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) |
68 | 1, 14, 13, 15, 2 | elocv 20012 |
. . . 4
⊢ (((𝑟(
·𝑠 ‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
69 | 23, 36, 67, 68 | syl3anbrc 1246 |
. . 3
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) |
70 | 69 | ralrimivvva 2972 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) |
71 | | ocvlss.l |
. . 3
⊢ 𝐿 = (LSubSp‘𝑊) |
72 | 13, 29, 1, 34, 28, 71 | islss 18935 |
. 2
⊢ (( ⊥
‘𝑆) ∈ 𝐿 ↔ (( ⊥ ‘𝑆) ⊆ 𝑉 ∧ ( ⊥ ‘𝑆) ≠ ∅ ∧
∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆))) |
73 | 4, 22, 70, 72 | syl3anbrc 1246 |
1
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ∈ 𝐿) |