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

Definition df-phl 18248
Description: Define class all generalized pre-Hilbert (inner product) spaces. (Contributed by NM, 22-Sep-2011.)
Assertion
Ref Expression
df-phl
Distinct variable group:   , , , , ,

Detailed syntax breakdown of Definition df-phl
StepHypRef Expression
1 cphl 18246 . 2
2 vf . . . . . . . . 9
32cv 1369 . . . . . . . 8
4 csr 17105 . . . . . . . 8
53, 4wcel 1758 . . . . . . 7
6 vy . . . . . . . . . . 11
7 vv . . . . . . . . . . . 12
87cv 1369 . . . . . . . . . . 11
96cv 1369 . . . . . . . . . . . 12
10 vx . . . . . . . . . . . . 13
1110cv 1369 . . . . . . . . . . . 12
12 vh . . . . . . . . . . . . 13
1312cv 1369 . . . . . . . . . . . 12
149, 11, 13co 6222 . . . . . . . . . . 11
156, 8, 14cmpt 4467 . . . . . . . . . 10
16 vg . . . . . . . . . . . 12
1716cv 1369 . . . . . . . . . . 11
18 crglmod 17426 . . . . . . . . . . . 12
193, 18cfv 5537 . . . . . . . . . . 11
20 clmhm 17276 . . . . . . . . . . 11
2117, 19, 20co 6222 . . . . . . . . . 10
2215, 21wcel 1758 . . . . . . . . 9
2311, 11, 13co 6222 . . . . . . . . . . 11
24 c0g 14537 . . . . . . . . . . . 12
253, 24cfv 5537 . . . . . . . . . . 11
2623, 25wceq 1370 . . . . . . . . . 10
2717, 24cfv 5537 . . . . . . . . . . 11
2811, 27wceq 1370 . . . . . . . . . 10
2926, 28wi 4 . . . . . . . . 9
3011, 9, 13co 6222 . . . . . . . . . . . 12
31 cstv 14399 . . . . . . . . . . . . 13
323, 31cfv 5537 . . . . . . . . . . . 12
3330, 32cfv 5537 . . . . . . . . . . 11
3433, 14wceq 1370 . . . . . . . . . 10
3534, 6, 8wral 2800 . . . . . . . . 9
3622, 29, 35w3a 965 . . . . . . . 8
3736, 10, 8wral 2800 . . . . . . 7
385, 37wa 369 . . . . . 6
39 csca 14400 . . . . . . 7
4017, 39cfv 5537 . . . . . 6
4138, 2, 40wsbc 3297 . . . . 5
42 cip 14402 . . . . . 6
4317, 42cfv 5537 . . . . 5
4441, 12, 43wsbc 3297 . . . 4
45 cbs 14332 . . . . 5
4617, 45cfv 5537 . . . 4
4744, 7, 46wsbc 3297 . . 3
48 clvec 17359 . . 3
4947, 16, 48crab 2804 . 2
501, 49wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  isphl  18250
  Copyright terms: Public domain W3C validator