Definition df-rq 7353

Description: Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by Jim Kingdon, 20-Sep-2019.)

Assertion

Ref	Expression
df-rq	⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rq

Step	Hyp	Ref	Expression
1		crq 7285	. 2 class *Q
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1352	. . . . 5 class 𝑥
4		cnq 7281	. . . . 5 class Q
5	3, 4	wcel 2148	. . . 4 wff 𝑥 ∈ Q
6		vy	. . . . . 6 setvar 𝑦
7	6	cv 1352	. . . . 5 class 𝑦
8	7, 4	wcel 2148	. . . 4 wff 𝑦 ∈ Q
9		cmq 7284	. . . . . 6 class ·Q
10	3, 7, 9	co 5877	. . . . 5 class (𝑥 ·Q 𝑦)
11		c1q 7282	. . . . 5 class 1Q
12	10, 11	wceq 1353	. . . 4 wff (𝑥 ·Q 𝑦) = 1Q
13	5, 8, 12	w3a 978	. . 3 wff (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)
14	13, 2, 6	copab 4065	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
15	1, 14	wceq 1353	1 wff *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}

This definition is referenced by:  recmulnqg  7392