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 
|- V = ( Base ` W )
ocvss.o 
|- ._|_ = ( ocv ` W )
ocvlss.l 
|- L = ( LSubSp ` W )
Assertion ocvlss 
|- ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) e. L )

Proof

Step Hyp Ref Expression
1 ocvss.v 
 |-  V = ( Base ` W )
2 ocvss.o 
 |-  ._|_ = ( ocv ` W )
3 ocvlss.l 
 |-  L = ( LSubSp ` W )
4 1 2 ocvss 
 |-  ( ._|_ ` S ) C_ V
5 4 a1i 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) C_ V )
6 simpr 
 |-  ( ( W e. PreHil /\ S C_ V ) -> S C_ V )
7 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
8 7 adantr 
 |-  ( ( W e. PreHil /\ S C_ V ) -> W e. LMod )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 1 9 lmod0vcl 
 |-  ( W e. LMod -> ( 0g ` W ) e. V )
11 8 10 syl 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( 0g ` W ) e. V )
12 simpll 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> W e. PreHil )
13 6 sselda 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> x e. V )
14 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
15 eqid 
 |-  ( .i ` W ) = ( .i ` W )
16 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
17 14 15 1 16 9 ip0l 
 |-  ( ( W e. PreHil /\ x e. V ) -> ( ( 0g ` W ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
18 12 13 17 syl2anc 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ x e. S ) -> ( ( 0g ` W ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
19 18 ralrimiva 
 |-  ( ( W e. PreHil /\ S C_ V ) -> A. x e. S ( ( 0g ` W ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
20 1 15 14 16 2 elocv 
 |-  ( ( 0g ` W ) e. ( ._|_ ` S ) <-> ( S C_ V /\ ( 0g ` W ) e. V /\ A. x e. S ( ( 0g ` W ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
21 6 11 19 20 syl3anbrc 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( 0g ` W ) e. ( ._|_ ` S ) )
22 21 ne0d 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) =/= (/) )
23 6 adantr 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> S C_ V )
24 8 adantr 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> W e. LMod )
25 simpr1 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> r e. ( Base ` ( Scalar ` W ) ) )
26 simpr2 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> y e. ( ._|_ ` S ) )
27 4 26 sselid 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> y e. V )
28 eqid 
 |-  ( .s ` W ) = ( .s ` W )
29 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
30 1 14 28 29 lmodvscl 
 |-  ( ( W e. LMod /\ r e. ( Base ` ( Scalar ` W ) ) /\ y e. V ) -> ( r ( .s ` W ) y ) e. V )
31 24 25 27 30 syl3anc 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> ( r ( .s ` W ) y ) e. V )
32 simpr3 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> z e. ( ._|_ ` S ) )
33 4 32 sselid 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> z e. V )
34 eqid 
 |-  ( +g ` W ) = ( +g ` W )
35 1 34 lmodvacl 
 |-  ( ( W e. LMod /\ ( r ( .s ` W ) y ) e. V /\ z e. V ) -> ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. V )
36 24 31 33 35 syl3anc 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. V )
37 12 adantlr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> W e. PreHil )
38 31 adantr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( r ( .s ` W ) y ) e. V )
39 33 adantr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> z e. V )
40 13 adantlr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> x e. V )
41 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
42 14 15 1 34 41 ipdir 
 |-  ( ( W e. PreHil /\ ( ( r ( .s ` W ) y ) e. V /\ z e. V /\ x e. V ) ) -> ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) ( .i ` W ) x ) = ( ( ( r ( .s ` W ) y ) ( .i ` W ) x ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) x ) ) )
43 37 38 39 40 42 syl13anc 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) ( .i ` W ) x ) = ( ( ( r ( .s ` W ) y ) ( .i ` W ) x ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) x ) ) )
44 25 adantr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> r e. ( Base ` ( Scalar ` W ) ) )
45 27 adantr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> y e. V )
46 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
47 14 15 1 29 28 46 ipass 
 |-  ( ( W e. PreHil /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. V /\ x e. V ) ) -> ( ( r ( .s ` W ) y ) ( .i ` W ) x ) = ( r ( .r ` ( Scalar ` W ) ) ( y ( .i ` W ) x ) ) )
48 37 44 45 40 47 syl13anc 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( r ( .s ` W ) y ) ( .i ` W ) x ) = ( r ( .r ` ( Scalar ` W ) ) ( y ( .i ` W ) x ) ) )
49 1 15 14 16 2 ocvi 
 |-  ( ( y e. ( ._|_ ` S ) /\ x e. S ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
50 26 49 sylan 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( y ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
51 50 oveq2d 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( r ( .r ` ( Scalar ` W ) ) ( y ( .i ` W ) x ) ) = ( r ( .r ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) )
52 24 adantr 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> W e. LMod )
53 14 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
54 52 53 syl 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( Scalar ` W ) e. Ring )
55 29 46 16 ringrz 
 |-  ( ( ( Scalar ` W ) e. Ring /\ r e. ( Base ` ( Scalar ` W ) ) ) -> ( r ( .r ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
56 54 44 55 syl2anc 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( r ( .r ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
57 48 51 56 3eqtrd 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( r ( .s ` W ) y ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
58 1 15 14 16 2 ocvi 
 |-  ( ( z e. ( ._|_ ` S ) /\ x e. S ) -> ( z ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
59 32 58 sylan 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( z ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
60 57 59 oveq12d 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( ( r ( .s ` W ) y ) ( .i ` W ) x ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) x ) ) = ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) )
61 14 lmodfgrp 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Grp )
62 29 16 grpidcl 
 |-  ( ( Scalar ` W ) e. Grp -> ( 0g ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
63 29 41 16 grplid 
 |-  ( ( ( Scalar ` W ) e. Grp /\ ( 0g ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
64 62 63 mpdan 
 |-  ( ( Scalar ` W ) e. Grp -> ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
65 52 61 64 3syl 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` ( Scalar ` W ) ) )
66 43 60 65 3eqtrd 
 |-  ( ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) /\ x e. S ) -> ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
67 66 ralrimiva 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> A. x e. S ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) )
68 1 15 14 16 2 elocv 
 |-  ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. ( ._|_ ` S ) <-> ( S C_ V /\ ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. V /\ A. x e. S ( ( ( r ( .s ` W ) y ) ( +g ` W ) z ) ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
69 23 36 67 68 syl3anbrc 
 |-  ( ( ( W e. PreHil /\ S C_ V ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ y e. ( ._|_ ` S ) /\ z e. ( ._|_ ` S ) ) ) -> ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. ( ._|_ ` S ) )
70 69 ralrimivvva 
 |-  ( ( W e. PreHil /\ S C_ V ) -> A. r e. ( Base ` ( Scalar ` W ) ) A. y e. ( ._|_ ` S ) A. z e. ( ._|_ ` S ) ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. ( ._|_ ` S ) )
71 14 29 1 34 28 3 islss 
 |-  ( ( ._|_ ` S ) e. L <-> ( ( ._|_ ` S ) C_ V /\ ( ._|_ ` S ) =/= (/) /\ A. r e. ( Base ` ( Scalar ` W ) ) A. y e. ( ._|_ ` S ) A. z e. ( ._|_ ` S ) ( ( r ( .s ` W ) y ) ( +g ` W ) z ) e. ( ._|_ ` S ) ) )
72 5 22 70 71 syl3anbrc 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( ._|_ ` S ) e. L )