| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ocvss.v | . . . 4
⊢ 𝑉 = (Base‘𝑊) | 
| 2 |  | ocvss.o | . . . 4
⊢  ⊥ =
(ocv‘𝑊) | 
| 3 | 1, 2 | ocvss 21689 | . . 3
⊢ ( ⊥
‘𝑆) ⊆ 𝑉 | 
| 4 | 3 | a1i 11 | . 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ⊆ 𝑉) | 
| 5 |  | simpr 484 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) | 
| 6 |  | phllmod 21649 | . . . . . 6
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑊 ∈ LMod) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 9 | 1, 8 | lmod0vcl 20890 | . . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ 𝑉) | 
| 10 | 7, 9 | syl 17 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ 𝑉) | 
| 11 |  | simpll 766 | . . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ PreHil) | 
| 12 | 5 | sselda 3982 | . . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) | 
| 13 |  | eqid 2736 | . . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 14 |  | eqid 2736 | . . . . . . 7
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) | 
| 15 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 16 | 13, 14, 1, 15, 8 | ip0l 21655 | . . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 17 | 11, 12, 16 | syl2anc 584 | . . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ 𝑥 ∈ 𝑆) → ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 18 | 17 | ralrimiva 3145 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 19 | 1, 14, 13, 15, 2 | elocv 21687 | . . . 4
⊢
((0g‘𝑊) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ (0g‘𝑊) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 ((0g‘𝑊)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) | 
| 20 | 5, 10, 18, 19 | syl3anbrc 1343 | . . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑊) ∈ ( ⊥ ‘𝑆)) | 
| 21 | 20 | ne0d 4341 | . 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ≠ ∅) | 
| 22 | 5 | adantr 480 | . . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑆 ⊆ 𝑉) | 
| 23 | 7 | adantr 480 | . . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑊 ∈ LMod) | 
| 24 |  | simpr1 1194 | . . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) | 
| 25 |  | simpr2 1195 | . . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ ( ⊥ ‘𝑆)) | 
| 26 | 3, 25 | sselid 3980 | . . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑦 ∈ 𝑉) | 
| 27 |  | eqid 2736 | . . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 28 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 29 | 1, 13, 27, 28 | lmodvscl 20877 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) | 
| 30 | 23, 24, 26, 29 | syl3anc 1372 | . . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) | 
| 31 |  | simpr3 1196 | . . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ ( ⊥ ‘𝑆)) | 
| 32 | 3, 31 | sselid 3980 | . . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → 𝑧 ∈ 𝑉) | 
| 33 |  | eqid 2736 | . . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 34 | 1, 33 | lmodvacl 20874 | . . . . 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 480 | . . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟( ·𝑠
‘𝑊)𝑦) ∈ 𝑉) | 
| 38 | 32 | adantr 480 | . . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑧 ∈ 𝑉) | 
| 39 | 12 | adantlr 715 | . . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑉) | 
| 40 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) | 
| 41 | 13, 14, 1, 33, 40 | ipdir 21658 | . . . . . . 7
⊢ ((𝑊 ∈ PreHil ∧ ((𝑟(
·𝑠 ‘𝑊)𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) | 
| 42 | 36, 37, 38, 39, 41 | syl13anc 1373 | . . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥))) | 
| 43 | 24 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) | 
| 44 | 26 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑦 ∈ 𝑉) | 
| 45 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) | 
| 46 | 13, 14, 1, 28, 27, 45 | ipass 21664 | . . . . . . . . 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 21688 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 49 | 25, 48 | sylan 580 | . . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑦(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 50 | 49 | oveq2d 7448 | . . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(𝑦(·𝑖‘𝑊)𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) | 
| 51 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ LMod) | 
| 52 | 13 | lmodring 20867 | . . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . 9
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (Scalar‘𝑊) ∈ Ring) | 
| 54 | 28, 45, 15 | ringrz 20292 | . . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 55 | 53, 43, 54 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 56 | 47, 50, 55 | 3eqtrd 2780 | . . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → ((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 57 | 1, 14, 13, 15, 2 | ocvi 21688 | . . . . . . . 8
⊢ ((𝑧 ∈ ( ⊥ ‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 58 | 31, 57 | sylan 580 | . . . . . . 7
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 59 | 56, 58 | oveq12d 7450 | . . . . . 6
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(·𝑖‘𝑊)𝑥)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑥)) = ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) | 
| 60 | 13 | lmodfgrp 20868 | . . . . . . 7
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) | 
| 61 | 28, 15 | grpidcl 18984 | . . . . . . . 8
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) | 
| 62 | 28, 40, 15 | grplid 18986 | . . . . . . . 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 2780 | . . . . 5
⊢ ((((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 66 | 65 | ralrimiva 3145 | . . . 4
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) | 
| 67 | 1, 14, 13, 15, 2 | elocv 21687 | . . . 4
⊢ (((𝑟(
·𝑠 ‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) | 
| 68 | 22, 35, 66, 67 | syl3anbrc 1343 | . . 3
⊢ (((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑦 ∈ ( ⊥ ‘𝑆) ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) | 
| 69 | 68 | ralrimivvva 3204 | . 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆)) | 
| 70 |  | ocvlss.l | . . 3
⊢ 𝐿 = (LSubSp‘𝑊) | 
| 71 | 13, 28, 1, 33, 27, 70 | islss 20933 | . 2
⊢ (( ⊥
‘𝑆) ∈ 𝐿 ↔ (( ⊥ ‘𝑆) ⊆ 𝑉 ∧ ( ⊥ ‘𝑆) ≠ ∅ ∧
∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑦 ∈ ( ⊥ ‘𝑆)∀𝑧 ∈ ( ⊥ ‘𝑆)((𝑟( ·𝑠
‘𝑊)𝑦)(+g‘𝑊)𝑧) ∈ ( ⊥ ‘𝑆))) | 
| 72 | 4, 21, 69, 71 | syl3anbrc 1343 | 1
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ∈ 𝐿) |