Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-doch | Structured version Visualization version Unicode version |
Description: Define subspace orthocomplement for vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.) |
Ref | Expression |
---|---|
df-doch |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coch 36636 | . 2 | |
2 | vk | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vw | . . . 4 | |
5 | 2 | cv 1482 | . . . . 5 |
6 | clh 35270 | . . . . 5 | |
7 | 5, 6 | cfv 5888 | . . . 4 |
8 | vx | . . . . 5 | |
9 | 4 | cv 1482 | . . . . . . . 8 |
10 | cdvh 36367 | . . . . . . . . 9 | |
11 | 5, 10 | cfv 5888 | . . . . . . . 8 |
12 | 9, 11 | cfv 5888 | . . . . . . 7 |
13 | cbs 15857 | . . . . . . 7 | |
14 | 12, 13 | cfv 5888 | . . . . . 6 |
15 | 14 | cpw 4158 | . . . . 5 |
16 | 8 | cv 1482 | . . . . . . . . . 10 |
17 | vy | . . . . . . . . . . . 12 | |
18 | 17 | cv 1482 | . . . . . . . . . . 11 |
19 | cdih 36517 | . . . . . . . . . . . . 13 | |
20 | 5, 19 | cfv 5888 | . . . . . . . . . . . 12 |
21 | 9, 20 | cfv 5888 | . . . . . . . . . . 11 |
22 | 18, 21 | cfv 5888 | . . . . . . . . . 10 |
23 | 16, 22 | wss 3574 | . . . . . . . . 9 |
24 | 5, 13 | cfv 5888 | . . . . . . . . 9 |
25 | 23, 17, 24 | crab 2916 | . . . . . . . 8 |
26 | cglb 16943 | . . . . . . . . 9 | |
27 | 5, 26 | cfv 5888 | . . . . . . . 8 |
28 | 25, 27 | cfv 5888 | . . . . . . 7 |
29 | coc 15949 | . . . . . . . 8 | |
30 | 5, 29 | cfv 5888 | . . . . . . 7 |
31 | 28, 30 | cfv 5888 | . . . . . 6 |
32 | 31, 21 | cfv 5888 | . . . . 5 |
33 | 8, 15, 32 | cmpt 4729 | . . . 4 |
34 | 4, 7, 33 | cmpt 4729 | . . 3 |
35 | 2, 3, 34 | cmpt 4729 | . 2 |
36 | 1, 35 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: dochffval 36638 |
Copyright terms: Public domain | W3C validator |