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

Definition df-phl 17763
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 17761 . 2
2 vf . . . . . . . . 9
32cv 1686 . . . . . . . 8
4 csr 16742 . . . . . . . 8
53, 4wcel 1749 . . . . . . 7
6 vy . . . . . . . . . . 11
7 vv . . . . . . . . . . . 12
87cv 1686 . . . . . . . . . . 11
96cv 1686 . . . . . . . . . . . 12
10 vx . . . . . . . . . . . . 13
1110cv 1686 . . . . . . . . . . . 12
12 vh . . . . . . . . . . . . 13
1312cv 1686 . . . . . . . . . . . 12
149, 11, 13co 6061 . . . . . . . . . . 11
156, 8, 14cmpt 4325 . . . . . . . . . 10
16 vg . . . . . . . . . . . 12
1716cv 1686 . . . . . . . . . . 11
18 crglmod 17059 . . . . . . . . . . . 12
193, 18cfv 5390 . . . . . . . . . . 11
20 clmhm 16909 . . . . . . . . . . 11
2117, 19, 20co 6061 . . . . . . . . . 10
2215, 21wcel 1749 . . . . . . . . 9
2311, 11, 13co 6061 . . . . . . . . . . 11
24 c0g 14318 . . . . . . . . . . . 12
253, 24cfv 5390 . . . . . . . . . . 11
2623, 25wceq 1687 . . . . . . . . . 10
2717, 24cfv 5390 . . . . . . . . . . 11
2811, 27wceq 1687 . . . . . . . . . 10
2926, 28wi 4 . . . . . . . . 9
3011, 9, 13co 6061 . . . . . . . . . . . 12
31 cstv 14180 . . . . . . . . . . . . 13
323, 31cfv 5390 . . . . . . . . . . . 12
3330, 32cfv 5390 . . . . . . . . . . 11
3433, 14wceq 1687 . . . . . . . . . 10
3534, 6, 8wral 2694 . . . . . . . . 9
3622, 29, 35w3a 950 . . . . . . . 8
3736, 10, 8wral 2694 . . . . . . 7
385, 37wa 362 . . . . . 6
39 csca 14181 . . . . . . 7
4017, 39cfv 5390 . . . . . 6
4138, 2, 40wsbc 3164 . . . . 5
42 cip 14183 . . . . . 6
4317, 42cfv 5390 . . . . 5
4441, 12, 43wsbc 3164 . . . 4
45 cbs 14114 . . . . 5
4617, 45cfv 5390 . . . 4
4744, 7, 46wsbc 3164 . . 3
48 clvec 16992 . . 3
4947, 16, 48crab 2698 . 2
501, 49wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  isphl  17765
  Copyright terms: Public domain W3C validator