Metamath Proof Explorer

Definition df-mr

Description: Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-mr ⊢ ⋅ 𝑹 = x y z | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmr class ⋅ 𝑹
1 vx setvar x
2 vy setvar y
3 vz setvar z
4 1 cv setvar x
5 cnr class 𝑹
6 4 5 wcel wff x ∈ 𝑹
7 2 cv setvar y
8 7 5 wcel wff y ∈ 𝑹
9 6 8 wa wff x ∈ 𝑹 ∧ y ∈ 𝑹
10 vw setvar w
11 vv setvar v
12 vu setvar u
13 vf setvar f
14 10 cv setvar w
15 11 cv setvar v
16 14 15 cop class w v
17 cer class ~ 𝑹
18 16 17 cec class w v ~ 𝑹
19 4 18 wceq wff x = w v ~ 𝑹
20 12 cv setvar u
21 13 cv setvar f
22 20 21 cop class u f
23 22 17 cec class u f ~ 𝑹
24 7 23 wceq wff y = u f ~ 𝑹
25 19 24 wa wff x = w v ~ 𝑹 ∧ y = u f ~ 𝑹
26 3 cv setvar z
27 cmp class ⋅ 𝑷
28 14 20 27 co class w ⋅ 𝑷 u
29 cpp class + 𝑷
30 15 21 27 co class v ⋅ 𝑷 f
31 28 30 29 co class w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f
32 14 21 27 co class w ⋅ 𝑷 f
33 15 20 27 co class v ⋅ 𝑷 u
34 32 33 29 co class w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u
35 31 34 cop class w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u
36 35 17 cec class w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
37 26 36 wceq wff z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
38 25 37 wa wff x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
39 38 13 wex wff ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
40 39 12 wex wff ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
41 40 11 wex wff ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
42 41 10 wex wff ∃ w ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
43 9 42 wa wff x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
44 43 1 2 3 coprab class x y z | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹
45 0 44 wceq wff ⋅ 𝑹 = x y z | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ w ∃ v ∃ u ∃ f x = w v ~ 𝑹 ∧ y = u f ~ 𝑹 ∧ z = w ⋅ 𝑷 u + 𝑷 v ⋅ 𝑷 f w ⋅ 𝑷 f + 𝑷 v ⋅ 𝑷 u ~ 𝑹