# 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 ) ) )`
` |-  ( ( 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 syl6bb
` |-  ( 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 ) )`
` |-  ( ( 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 syl6bbr
` |-  ( 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 )`