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 AAS

Proof

Step Hyp Ref Expression
1 ocval AA=x|yAxihy=0
2 ssrab2 x|yAxihy=0
3 1 2 eqsstrdi AA
4 ssel AyAy
5 hi01 y0ihy=0
6 4 5 syl6 AyA0ihy=0
7 6 ralrimiv AyA0ihy=0
8 ax-hv0cl 0
9 7 8 jctil A0yA0ihy=0
10 ocel A0A0yA0ihy=0
11 9 10 mpbird A0A
12 3 11 jca AA0A
13 ssel2 AzAz
14 ax-his2 xyzx+yihz=xihz+yihz
15 14 3expa xyzx+yihz=xihz+yihz
16 oveq12 xihz=0yihz=0xihz+yihz=0+0
17 00id 0+0=0
18 16 17 eqtrdi xihz=0yihz=0xihz+yihz=0
19 15 18 sylan9eq xyzxihz=0yihz=0x+yihz=0
20 19 ex xyzxihz=0yihz=0x+yihz=0
21 20 ancoms zxyxihz=0yihz=0x+yihz=0
22 13 21 sylan AzAxyxihz=0yihz=0x+yihz=0
23 22 an32s AxyzAxihz=0yihz=0x+yihz=0
24 23 ralimdva AxyzAxihz=0yihz=0zAx+yihz=0
25 24 imdistanda AxyzAxihz=0yihz=0xyzAx+yihz=0
26 hvaddcl xyx+y
27 26 anim1i xyzAx+yihz=0x+yzAx+yihz=0
28 25 27 syl6 AxyzAxihz=0yihz=0x+yzAx+yihz=0
29 ocel AxAxzAxihz=0
30 ocel AyAyzAyihz=0
31 29 30 anbi12d AxAyAxzAxihz=0yzAyihz=0
32 an4 xzAxihz=0yzAyihz=0xyzAxihz=0zAyihz=0
33 r19.26 zAxihz=0yihz=0zAxihz=0zAyihz=0
34 33 anbi2i xyzAxihz=0yihz=0xyzAxihz=0zAyihz=0
35 32 34 bitr4i xzAxihz=0yzAyihz=0xyzAxihz=0yihz=0
36 31 35 bitrdi AxAyAxyzAxihz=0yihz=0
37 ocel Ax+yAx+yzAx+yihz=0
38 28 36 37 3imtr4d AxAyAx+yA
39 38 ralrimivv AxAyAx+yA
40 mul01 xx0=0
41 oveq2 yihz=0xyihz=x0
42 41 eqeq1d yihz=0xyihz=0x0=0
43 40 42 syl5ibrcom xyihz=0xyihz=0
44 43 ad2antrl zxyyihz=0xyihz=0
45 ax-his3 xyzxyihz=xyihz
46 45 eqeq1d xyzxyihz=0xyihz=0
47 46 3expa xyzxyihz=0xyihz=0
48 47 ancoms zxyxyihz=0xyihz=0
49 44 48 sylibrd zxyyihz=0xyihz=0
50 13 49 sylan AzAxyyihz=0xyihz=0
51 50 an32s AxyzAyihz=0xyihz=0
52 51 ralimdva AxyzAyihz=0zAxyihz=0
53 52 imdistanda AxyzAyihz=0xyzAxyihz=0
54 hvmulcl xyxy
55 54 anim1i xyzAxyihz=0xyzAxyihz=0
56 53 55 syl6 AxyzAyihz=0xyzAxyihz=0
57 30 anbi2d AxyAxyzAyihz=0
58 anass xyzAyihz=0xyzAyihz=0
59 57 58 bitr4di AxyAxyzAyihz=0
60 ocel AxyAxyzAxyihz=0
61 56 59 60 3imtr4d AxyAxyA
62 61 ralrimivv AxyAxyA
63 39 62 jca AxAyAx+yAxyAxyA
64 issh2 ASA0AxAyAx+yAxyAxyA
65 12 63 64 sylanbrc AAS