This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-plq

Description: Define addition 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.3 of Gleason p. 117. (Contributed by NM, 24-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-plq	$⊢ +_{𝑸} = {(/_{𝑸} \circ +_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplq	$class +_{𝑸}$
1		cerq	$class /_{𝑸}$
2		cplpq	$class +_{𝑝𝑸}$
3	1 2	ccom	$class (/_{𝑸} \circ +_{𝑝𝑸})$
4		cnq	$class 𝑸$
5	4 4	cxp	$class (𝑸 \times 𝑸)$
6	3 5	cres	$class ({(/_{𝑸} \circ +_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸)$
7	0 6	wceq	$wff +_{𝑸} = {(/_{𝑸} \circ +_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸$