Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-docaN Structured version   Unicode version

Definition df-docaN 35088
 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.)
Assertion
Ref Expression
df-docaN
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-docaN
StepHypRef Expression
1 cocaN 35087 . 2
2 vk . . 3
3 cvv 3076 . . 3
4 vw . . . 4
52cv 1369 . . . . 5
6 clh 33951 . . . . 5
75, 6cfv 5525 . . . 4
8 vx . . . . 5
94cv 1369 . . . . . . 7
10 cltrn 34068 . . . . . . . 8
115, 10cfv 5525 . . . . . . 7
129, 11cfv 5525 . . . . . 6
1312cpw 3967 . . . . 5
148cv 1369 . . . . . . . . . . . . 13
15 vz . . . . . . . . . . . . . 14
1615cv 1369 . . . . . . . . . . . . 13
1714, 16wss 3435 . . . . . . . . . . . 12
18 cdia 34996 . . . . . . . . . . . . . . 15
195, 18cfv 5525 . . . . . . . . . . . . . 14
209, 19cfv 5525 . . . . . . . . . . . . 13
2120crn 4948 . . . . . . . . . . . 12
2217, 15, 21crab 2802 . . . . . . . . . . 11
2322cint 4235 . . . . . . . . . 10
2420ccnv 4946 . . . . . . . . . 10
2523, 24cfv 5525 . . . . . . . . 9
26 coc 14364 . . . . . . . . . 10
275, 26cfv 5525 . . . . . . . . 9
2825, 27cfv 5525 . . . . . . . 8
299, 27cfv 5525 . . . . . . . 8
30 cjn 15232 . . . . . . . . 9
315, 30cfv 5525 . . . . . . . 8
3228, 29, 31co 6199 . . . . . . 7
33 cmee 15233 . . . . . . . 8
345, 33cfv 5525 . . . . . . 7
3532, 9, 34co 6199 . . . . . 6
3635, 20cfv 5525 . . . . 5
378, 13, 36cmpt 4457 . . . 4
384, 7, 37cmpt 4457 . . 3
392, 3, 38cmpt 4457 . 2
401, 39wceq 1370 1
 Colors of variables: wff setvar class This definition is referenced by:  docaffvalN  35089
 Copyright terms: Public domain W3C validator