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

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

Detailed syntax breakdown of Definition df-doch
StepHypRef Expression
1 coch 32145 . 2
2 vk . . 3
3 cvv 2956 . . 3
4 vw . . . 4
52cv 1651 . . . . 5
6 clh 30781 . . . . 5
75, 6cfv 5454 . . . 4
8 vx . . . . 5
94cv 1651 . . . . . . . 8
10 cdvh 31876 . . . . . . . . 9
115, 10cfv 5454 . . . . . . . 8
129, 11cfv 5454 . . . . . . 7
13 cbs 13469 . . . . . . 7
1412, 13cfv 5454 . . . . . 6
1514cpw 3799 . . . . 5
168cv 1651 . . . . . . . . . 10
17 vy . . . . . . . . . . . 12
1817cv 1651 . . . . . . . . . . 11
19 cdih 32026 . . . . . . . . . . . . 13
205, 19cfv 5454 . . . . . . . . . . . 12
219, 20cfv 5454 . . . . . . . . . . 11
2218, 21cfv 5454 . . . . . . . . . 10
2316, 22wss 3320 . . . . . . . . 9
245, 13cfv 5454 . . . . . . . . 9
2523, 17, 24crab 2709 . . . . . . . 8
26 cglb 14400 . . . . . . . . 9
275, 26cfv 5454 . . . . . . . 8
2825, 27cfv 5454 . . . . . . 7
29 coc 13537 . . . . . . . 8
305, 29cfv 5454 . . . . . . 7
3128, 30cfv 5454 . . . . . 6
3231, 21cfv 5454 . . . . 5
338, 15, 32cmpt 4266 . . . 4
344, 7, 33cmpt 4266 . . 3
352, 3, 34cmpt 4266 . 2
361, 35wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  dochffval  32147
 Copyright terms: Public domain W3C validator