Definition df-mp 3883

Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124.

Assertion

Ref	Expression
df-mp	⊢ ·P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}

Distinct variable group(s):   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-mp

Step	Hyp	Ref	Expression
1		cmp 3782	. 2 class ·P
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cnp 3779	. . . . . 6 class P
5	3, 4	wcel 1092	. . . . 5 wff x ∈ P
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ P
9	5, 8	wa 196	. . . 4 wff (x ∈ P ∧ y ∈ P)
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 1089	. . . . . . . . 9 class w
14		vv	. . . . . . . . . . 11 set v
15	14	cv 1089	. . . . . . . . . 10 class v
16		vu	. . . . . . . . . . 11 set u
17	16	cv 1089	. . . . . . . . . 10 class u
18		cmq 3776	. . . . . . . . . 10 class ·Q
19	15, 17, 18	co 3001	. . . . . . . . 9 class (v ·Q u)
20	13, 19	wceq 1091	. . . . . . . 8 wff w = (v ·Q u)
21	20, 16, 7	wrex 1202	. . . . . . 7 wff ∃u ∈ y w = (v ·Q u)
22	21, 14, 3	wrex 1202	. . . . . 6 wff ∃v ∈ x ∃u ∈ y w = (v ·Q u)
23	22, 12	cab 1090	. . . . 5 class {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)}
24	11, 23	wceq 1091	. . . 4 wff z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)}
25	9, 24	wa 196	. . 3 wff ((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})
26	25, 2, 6, 10	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}
27	1, 26	wceq 1091	1 wff ·P = {⟨⟨x, y⟩, z⟩∣((x ∈ P ∧ y ∈ P) ∧ z = {w∣∃v ∈ x ∃u ∈ y w = (v ·Q u)})}

This definition is referenced by:  mpv 3908  dmmp 3910  mulclprlem 3915  mulclpr 3916  mulasspr 3920  distrlem1pr 3921  distrlem2pr 3922  distrlem5pr 3925  1idpr 3927  reclem3pr 3952  reclem4pr 3953

metamath.org