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