Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ocv Structured version   Unicode version

Definition df-ocv 19161
 Description: Define orthocomplement of a subspace. (Contributed by NM, 7-Oct-2011.)
Assertion
Ref Expression
df-ocv Scalar
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ocv
StepHypRef Expression
1 cocv 19158 . 2
2 vh . . 3
3 cvv 3087 . . 3
4 vs . . . 4
52cv 1436 . . . . . 6
6 cbs 15084 . . . . . 6
75, 6cfv 5601 . . . . 5
87cpw 3985 . . . 4
9 vx . . . . . . . . 9
109cv 1436 . . . . . . . 8
11 vy . . . . . . . . 9
1211cv 1436 . . . . . . . 8
13 cip 15158 . . . . . . . . 9
145, 13cfv 5601 . . . . . . . 8
1510, 12, 14co 6305 . . . . . . 7
16 csca 15156 . . . . . . . . 9 Scalar
175, 16cfv 5601 . . . . . . . 8 Scalar
18 c0g 15301 . . . . . . . 8
1917, 18cfv 5601 . . . . . . 7 Scalar
2015, 19wceq 1437 . . . . . 6 Scalar
214cv 1436 . . . . . 6
2220, 11, 21wral 2782 . . . . 5 Scalar
2322, 9, 7crab 2786 . . . 4 Scalar
244, 8, 23cmpt 4484 . . 3 Scalar
252, 3, 24cmpt 4484 . 2 Scalar
261, 25wceq 1437 1 Scalar
 Colors of variables: wff setvar class This definition is referenced by:  ocvfval  19164
 Copyright terms: Public domain W3C validator