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 )