Metamath Proof Explorer

Theorem ocvlss

Description: The orthocomplement of a subset is a linear subspace of the pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
ocvlss.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion ocvlss ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 ocvss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ocvss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
3 ocvlss.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4 1 2 ocvss ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
5 4 a1i ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
6 simpr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
7 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
8 7 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
9 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
10 1 9 lmod0vcl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
11 8 10 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
12 simpll ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ PreHil )
13 6 sselda ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
14 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
15 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
16 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
17 14 15 1 16 9 ip0l ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ) → ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
18 12 13 17 syl2anc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
19 18 ralrimiva ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
20 1 15 14 16 2 elocv ⊢ ( ( 0g ‘ 𝑊 ) ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
21 6 11 19 20 syl3anbrc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 0g ‘ 𝑊 ) ∈ ( ⊥ ‘ 𝑆 ) )
22 21 ne0d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ≠ ∅ )
23 6 adantr ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑆 ⊆ 𝑉 )
24 8 adantr ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ LMod )
25 simpr1 ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
26 simpr2 ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ ( ⊥ ‘ 𝑆 ) )
27 4 26 sselid ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝑉 )
28 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
29 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
30 1 14 28 29 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
31 24 25 27 30 syl3anc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
32 simpr3 ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ ( ⊥ ‘ 𝑆 ) )
33 4 32 sselid ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ 𝑉 )
34 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
35 1 34 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
36 24 31 33 35 syl3anc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
37 12 adantlr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ PreHil )
38 31 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
39 33 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑧 ∈ 𝑉 )
40 13 adantlr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
41 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
42 14 15 1 34 41 ipdir ⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
43 37 38 39 40 42 syl13anc ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
44 25 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45 27 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑦 ∈ 𝑉 )
46 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
47 14 15 1 29 28 46 ipass ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
48 37 44 45 40 47 syl13anc ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
49 1 15 14 16 2 ocvi ⊢ ( ( 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
50 26 49 sylan ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
51 50 oveq2d ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
52 24 adantr ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ LMod )
53 14 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
54 52 53 syl ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ Ring )
55 29 46 16 ringrz ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Ring ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
56 54 44 55 syl2anc ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
57 48 51 56 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
58 1 15 14 16 2 ocvi ⊢ ( ( 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
59 32 58 sylan ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
60 57 59 oveq12d ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
61 14 lmodfgrp ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
62 29 16 grpidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
63 29 41 16 grplid ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
64 62 63 mpdan ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
65 52 61 64 3syl ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
66 43 60 65 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
67 66 ralrimiva ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
68 1 15 14 16 2 elocv ⊢ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
69 23 36 67 68 syl3anbrc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) )
70 69 ralrimivvva ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∀ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) )
71 14 29 1 34 28 3 islss ⊢ ( ( ⊥ ‘ 𝑆 ) ∈ 𝐿 ↔ ( ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑆 ) ≠ ∅ ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∀ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) ) )
72 5 22 70 71 syl3anbrc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )