Definition df-mp

Description: Define multiplication on positive 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-3.7 of Gleason p. 124. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mp	⊢ ·P = ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmp	⊢ ·P
1		vx	⊢ 𝑥
2		cnp	⊢ P
3		vy	⊢ 𝑦
4		vw	⊢ 𝑤
5		vv	⊢ 𝑣
6	1	cv	⊢ 𝑥
7		vu	⊢ 𝑢
8	3	cv	⊢ 𝑦
9	4	cv	⊢ 𝑤
10	5	cv	⊢ 𝑣
11		cmq	⊢ ·Q
12	7	cv	⊢ 𝑢
13	10 12 11	co	⊢ ( 𝑣 ·Q 𝑢 )
14	9 13	wceq	⊢ 𝑤 = ( 𝑣 ·Q 𝑢 )
15	14 7 8	wrex	⊢ ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 )
16	15 5 6	wrex	⊢ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 )
17	16 4	cab	⊢ { 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) }
18	1 3 2 2 17	cmpo	⊢ ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )
19	0 18	wceq	⊢ ·P = ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )