Definition df-mq

Description: Define multiplication on positive fractions. 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-2.4 of Gleason p. 119. (Contributed by NM, 24-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mq	⊢ ·Q = ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmq	⊢ ·Q
1		cerq	⊢ [Q]
2		cmpq	⊢ ·pQ
3	1 2	ccom	⊢ ( [Q] ∘ ·pQ )
4		cnq	⊢ Q
5	4 4	cxp	⊢ ( Q × Q )
6	3 5	cres	⊢ ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) )
7	0 6	wceq	⊢ ·Q = ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) )