Metamath Proof Explorer

Theorem ocsh

Description: The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocsh 
|- ( A C_ ~H -> ( _|_ ` A ) e. SH )

Proof

Step Hyp Ref Expression
1 ocval 
 |-  ( A C_ ~H -> ( _|_ ` A ) = { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
2 ssrab2 
 |-  { x e. ~H | A. y e. A ( x .ih y ) = 0 } C_ ~H
3 1 2 eqsstrdi 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
4 ssel 
 |-  ( A C_ ~H -> ( y e. A -> y e. ~H ) )
5 hi01 
 |-  ( y e. ~H -> ( 0h .ih y ) = 0 )
6 4 5 syl6 
 |-  ( A C_ ~H -> ( y e. A -> ( 0h .ih y ) = 0 ) )
7 6 ralrimiv 
 |-  ( A C_ ~H -> A. y e. A ( 0h .ih y ) = 0 )
8 ax-hv0cl 
 |-  0h e. ~H
9 7 8 jctil 
 |-  ( A C_ ~H -> ( 0h e. ~H /\ A. y e. A ( 0h .ih y ) = 0 ) )
10 ocel 
 |-  ( A C_ ~H -> ( 0h e. ( _|_ ` A ) <-> ( 0h e. ~H /\ A. y e. A ( 0h .ih y ) = 0 ) ) )
11 9 10 mpbird 
 |-  ( A C_ ~H -> 0h e. ( _|_ ` A ) )
12 3 11 jca 
 |-  ( A C_ ~H -> ( ( _|_ ` A ) C_ ~H /\ 0h e. ( _|_ ` A ) ) )
13 ssel2 
 |-  ( ( A C_ ~H /\ z e. A ) -> z e. ~H )
14 ax-his2 
 |-  ( ( x e. ~H /\ y e. ~H /\ z e. ~H ) -> ( ( x +h y ) .ih z ) = ( ( x .ih z ) + ( y .ih z ) ) )
15 14 3expa 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( x +h y ) .ih z ) = ( ( x .ih z ) + ( y .ih z ) ) )
16 oveq12 
 |-  ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x .ih z ) + ( y .ih z ) ) = ( 0 + 0 ) )
17 00id 
 |-  ( 0 + 0 ) = 0
18 16 17 eqtrdi 
 |-  ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x .ih z ) + ( y .ih z ) ) = 0 )
19 15 18 sylan9eq 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) /\ ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) -> ( ( x +h y ) .ih z ) = 0 )
20 19 ex 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ z e. ~H ) -> ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x +h y ) .ih z ) = 0 ) )
21 20 ancoms 
 |-  ( ( z e. ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x +h y ) .ih z ) = 0 ) )
22 13 21 sylan 
 |-  ( ( ( A C_ ~H /\ z e. A ) /\ ( x e. ~H /\ y e. ~H ) ) -> ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x +h y ) .ih z ) = 0 ) )
23 22 an32s 
 |-  ( ( ( A C_ ~H /\ ( x e. ~H /\ y e. ~H ) ) /\ z e. A ) -> ( ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> ( ( x +h y ) .ih z ) = 0 ) )
24 23 ralimdva 
 |-  ( ( A C_ ~H /\ ( x e. ~H /\ y e. ~H ) ) -> ( A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) -> A. z e. A ( ( x +h y ) .ih z ) = 0 ) )
25 24 imdistanda 
 |-  ( A C_ ~H -> ( ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) -> ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x +h y ) .ih z ) = 0 ) ) )
26 hvaddcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H )
27 26 anim1i 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x +h y ) .ih z ) = 0 ) -> ( ( x +h y ) e. ~H /\ A. z e. A ( ( x +h y ) .ih z ) = 0 ) )
28 25 27 syl6 
 |-  ( A C_ ~H -> ( ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) -> ( ( x +h y ) e. ~H /\ A. z e. A ( ( x +h y ) .ih z ) = 0 ) ) )
29 ocel 
 |-  ( A C_ ~H -> ( x e. ( _|_ ` A ) <-> ( x e. ~H /\ A. z e. A ( x .ih z ) = 0 ) ) )
30 ocel 
 |-  ( A C_ ~H -> ( y e. ( _|_ ` A ) <-> ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) )
31 29 30 anbi12d 
 |-  ( A C_ ~H -> ( ( x e. ( _|_ ` A ) /\ y e. ( _|_ ` A ) ) <-> ( ( x e. ~H /\ A. z e. A ( x .ih z ) = 0 ) /\ ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) ) )
32 an4 
 |-  ( ( ( x e. ~H /\ A. z e. A ( x .ih z ) = 0 ) /\ ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) <-> ( ( x e. ~H /\ y e. ~H ) /\ ( A. z e. A ( x .ih z ) = 0 /\ A. z e. A ( y .ih z ) = 0 ) ) )
33 r19.26 
 |-  ( A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) <-> ( A. z e. A ( x .ih z ) = 0 /\ A. z e. A ( y .ih z ) = 0 ) )
34 33 anbi2i 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) <-> ( ( x e. ~H /\ y e. ~H ) /\ ( A. z e. A ( x .ih z ) = 0 /\ A. z e. A ( y .ih z ) = 0 ) ) )
35 32 34 bitr4i 
 |-  ( ( ( x e. ~H /\ A. z e. A ( x .ih z ) = 0 ) /\ ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) <-> ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) )
36 31 35 bitrdi 
 |-  ( A C_ ~H -> ( ( x e. ( _|_ ` A ) /\ y e. ( _|_ ` A ) ) <-> ( ( x e. ~H /\ y e. ~H ) /\ A. z e. A ( ( x .ih z ) = 0 /\ ( y .ih z ) = 0 ) ) ) )
37 ocel 
 |-  ( A C_ ~H -> ( ( x +h y ) e. ( _|_ ` A ) <-> ( ( x +h y ) e. ~H /\ A. z e. A ( ( x +h y ) .ih z ) = 0 ) ) )
38 28 36 37 3imtr4d 
 |-  ( A C_ ~H -> ( ( x e. ( _|_ ` A ) /\ y e. ( _|_ ` A ) ) -> ( x +h y ) e. ( _|_ ` A ) ) )
39 38 ralrimivv 
 |-  ( A C_ ~H -> A. x e. ( _|_ ` A ) A. y e. ( _|_ ` A ) ( x +h y ) e. ( _|_ ` A ) )
40 mul01 
 |-  ( x e. CC -> ( x x. 0 ) = 0 )
41 oveq2 
 |-  ( ( y .ih z ) = 0 -> ( x x. ( y .ih z ) ) = ( x x. 0 ) )
42 41 eqeq1d 
 |-  ( ( y .ih z ) = 0 -> ( ( x x. ( y .ih z ) ) = 0 <-> ( x x. 0 ) = 0 ) )
43 40 42 syl5ibrcom 
 |-  ( x e. CC -> ( ( y .ih z ) = 0 -> ( x x. ( y .ih z ) ) = 0 ) )
44 43 ad2antrl 
 |-  ( ( z e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( y .ih z ) = 0 -> ( x x. ( y .ih z ) ) = 0 ) )
45 ax-his3 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( ( x .h y ) .ih z ) = ( x x. ( y .ih z ) ) )
46 45 eqeq1d 
 |-  ( ( x e. CC /\ y e. ~H /\ z e. ~H ) -> ( ( ( x .h y ) .ih z ) = 0 <-> ( x x. ( y .ih z ) ) = 0 ) )
47 46 3expa 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ z e. ~H ) -> ( ( ( x .h y ) .ih z ) = 0 <-> ( x x. ( y .ih z ) ) = 0 ) )
48 47 ancoms 
 |-  ( ( z e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( ( x .h y ) .ih z ) = 0 <-> ( x x. ( y .ih z ) ) = 0 ) )
49 44 48 sylibrd 
 |-  ( ( z e. ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( ( y .ih z ) = 0 -> ( ( x .h y ) .ih z ) = 0 ) )
50 13 49 sylan 
 |-  ( ( ( A C_ ~H /\ z e. A ) /\ ( x e. CC /\ y e. ~H ) ) -> ( ( y .ih z ) = 0 -> ( ( x .h y ) .ih z ) = 0 ) )
51 50 an32s 
 |-  ( ( ( A C_ ~H /\ ( x e. CC /\ y e. ~H ) ) /\ z e. A ) -> ( ( y .ih z ) = 0 -> ( ( x .h y ) .ih z ) = 0 ) )
52 51 ralimdva 
 |-  ( ( A C_ ~H /\ ( x e. CC /\ y e. ~H ) ) -> ( A. z e. A ( y .ih z ) = 0 -> A. z e. A ( ( x .h y ) .ih z ) = 0 ) )
53 52 imdistanda 
 |-  ( A C_ ~H -> ( ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( y .ih z ) = 0 ) -> ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( ( x .h y ) .ih z ) = 0 ) ) )
54 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
55 54 anim1i 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( ( x .h y ) .ih z ) = 0 ) -> ( ( x .h y ) e. ~H /\ A. z e. A ( ( x .h y ) .ih z ) = 0 ) )
56 53 55 syl6 
 |-  ( A C_ ~H -> ( ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( y .ih z ) = 0 ) -> ( ( x .h y ) e. ~H /\ A. z e. A ( ( x .h y ) .ih z ) = 0 ) ) )
57 30 anbi2d 
 |-  ( A C_ ~H -> ( ( x e. CC /\ y e. ( _|_ ` A ) ) <-> ( x e. CC /\ ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) ) )
58 anass 
 |-  ( ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( y .ih z ) = 0 ) <-> ( x e. CC /\ ( y e. ~H /\ A. z e. A ( y .ih z ) = 0 ) ) )
59 57 58 bitr4di 
 |-  ( A C_ ~H -> ( ( x e. CC /\ y e. ( _|_ ` A ) ) <-> ( ( x e. CC /\ y e. ~H ) /\ A. z e. A ( y .ih z ) = 0 ) ) )
60 ocel 
 |-  ( A C_ ~H -> ( ( x .h y ) e. ( _|_ ` A ) <-> ( ( x .h y ) e. ~H /\ A. z e. A ( ( x .h y ) .ih z ) = 0 ) ) )
61 56 59 60 3imtr4d 
 |-  ( A C_ ~H -> ( ( x e. CC /\ y e. ( _|_ ` A ) ) -> ( x .h y ) e. ( _|_ ` A ) ) )
62 61 ralrimivv 
 |-  ( A C_ ~H -> A. x e. CC A. y e. ( _|_ ` A ) ( x .h y ) e. ( _|_ ` A ) )
63 39 62 jca 
 |-  ( A C_ ~H -> ( A. x e. ( _|_ ` A ) A. y e. ( _|_ ` A ) ( x +h y ) e. ( _|_ ` A ) /\ A. x e. CC A. y e. ( _|_ ` A ) ( x .h y ) e. ( _|_ ` A ) ) )
64 issh2 
 |-  ( ( _|_ ` A ) e. SH <-> ( ( ( _|_ ` A ) C_ ~H /\ 0h e. ( _|_ ` A ) ) /\ ( A. x e. ( _|_ ` A ) A. y e. ( _|_ ` A ) ( x +h y ) e. ( _|_ ` A ) /\ A. x e. CC A. y e. ( _|_ ` A ) ( x .h y ) e. ( _|_ ` A ) ) ) )
65 12 63 64 sylanbrc 
 |-  ( A C_ ~H -> ( _|_ ` A ) e. SH )