Metamath Proof Explorer


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 o. .pQ ) |` ( Q. X. Q. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmq
 |-  .Q
1 cerq
 |-  /Q
2 cmpq
 |-  .pQ
3 1 2 ccom
 |-  ( /Q o. .pQ )
4 cnq
 |-  Q.
5 4 4 cxp
 |-  ( Q. X. Q. )
6 3 5 cres
 |-  ( ( /Q o. .pQ ) |` ( Q. X. Q. ) )
7 0 6 wceq
 |-  .Q = ( ( /Q o. .pQ ) |` ( Q. X. Q. ) )