Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Definition df-plpq 6553
 Description: Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 6758, and is intended to be used only by the construction. This "pre-addition" operation works works directly with ordered pairs of integers. The actual positive fraction addition (df-plq 6557) works with the equivalence classes of these ordered pairs determined by the equivalence relation (df-enq 6555). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117.
Assertion
Ref Expression
df-plpq
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-plpq
StepHypRef Expression
1 cplpq 6494 . 2
2 vx . . . . . . 7
32cv 1585 . . . . . 6
4 cnpi 6490 . . . . . . 7
54, 4cxp 4117 . . . . . 6
63, 5wcel 1588 . . . . 5
7 vy . . . . . . 7
87cv 1585 . . . . . 6
98, 5wcel 1588 . . . . 5
106, 9wa 337 . . . 4
11 vw . . . . . . . . . . . . 13
1211cv 1585 . . . . . . . . . . . 12
13 vv . . . . . . . . . . . . 13
1413cv 1585 . . . . . . . . . . . 12
1512, 14cop 3240 . . . . . . . . . . 11
163, 15wceq 1586 . . . . . . . . . 10
17 vu . . . . . . . . . . . . 13
1817cv 1585 . . . . . . . . . . . 12
19 vf . . . . . . . . . . . . 13
2019cv 1585 . . . . . . . . . . . 12
2118, 20cop 3240 . . . . . . . . . . 11
228, 21wceq 1586 . . . . . . . . . 10
2316, 22wa 337 . . . . . . . . 9
24 vz . . . . . . . . . . 11
2524cv 1585 . . . . . . . . . 10
26 cmi 6492 . . . . . . . . . . . . 13
2712, 20, 26co 4981 . . . . . . . . . . . 12
2814, 18, 26co 4981 . . . . . . . . . . . 12
29 cpli 6491 . . . . . . . . . . . 12
3027, 28, 29co 4981 . . . . . . . . . . 11
3114, 20, 26co 4981 . . . . . . . . . . 11
3230, 31cop 3240 . . . . . . . . . 10
3325, 32wceq 1586 . . . . . . . . 9
3423, 33wa 337 . . . . . . . 8
3534, 19wex 1615 . . . . . . 7
3635, 17wex 1615 . . . . . 6
3736, 13wex 1615 . . . . 5
3837, 11wex 1615 . . . 4
3910, 38wa 337 . . 3
4039, 2, 7, 24copab2 4982 . 2
411, 40wceq 1586 1
 Colors of variables: wff set class This definition is referenced by:  addpipq 6572