Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-docaN | Structured version Visualization version Unicode version |
Description: Define subspace orthocomplement for partial 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, 6-Dec-2013.) |
Ref | Expression |
---|---|
df-docaN |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cocaN 36408 | . 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 | . . . . . . 7 |
10 | cltrn 35387 | . . . . . . . 8 | |
11 | 5, 10 | cfv 5888 | . . . . . . 7 |
12 | 9, 11 | cfv 5888 | . . . . . 6 |
13 | 12 | cpw 4158 | . . . . 5 |
14 | 8 | cv 1482 | . . . . . . . . . . . . 13 |
15 | vz | . . . . . . . . . . . . . 14 | |
16 | 15 | cv 1482 | . . . . . . . . . . . . 13 |
17 | 14, 16 | wss 3574 | . . . . . . . . . . . 12 |
18 | cdia 36317 | . . . . . . . . . . . . . . 15 | |
19 | 5, 18 | cfv 5888 | . . . . . . . . . . . . . 14 |
20 | 9, 19 | cfv 5888 | . . . . . . . . . . . . 13 |
21 | 20 | crn 5115 | . . . . . . . . . . . 12 |
22 | 17, 15, 21 | crab 2916 | . . . . . . . . . . 11 |
23 | 22 | cint 4475 | . . . . . . . . . 10 |
24 | 20 | ccnv 5113 | . . . . . . . . . 10 |
25 | 23, 24 | cfv 5888 | . . . . . . . . 9 |
26 | coc 15949 | . . . . . . . . . 10 | |
27 | 5, 26 | cfv 5888 | . . . . . . . . 9 |
28 | 25, 27 | cfv 5888 | . . . . . . . 8 |
29 | 9, 27 | cfv 5888 | . . . . . . . 8 |
30 | cjn 16944 | . . . . . . . . 9 | |
31 | 5, 30 | cfv 5888 | . . . . . . . 8 |
32 | 28, 29, 31 | co 6650 | . . . . . . 7 |
33 | cmee 16945 | . . . . . . . 8 | |
34 | 5, 33 | cfv 5888 | . . . . . . 7 |
35 | 32, 9, 34 | co 6650 | . . . . . 6 |
36 | 35, 20 | cfv 5888 | . . . . 5 |
37 | 8, 13, 36 | cmpt 4729 | . . . 4 |
38 | 4, 7, 37 | cmpt 4729 | . . 3 |
39 | 2, 3, 38 | cmpt 4729 | . 2 |
40 | 1, 39 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: docaffvalN 36410 |
Copyright terms: Public domain | W3C validator |