recmulnq

Description: Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

		Ref	Expression
	Assertion	recmulnq	$⊢ A \in 𝑸 \to (*_{𝑸} (A) = B \leftrightarrow A \cdot_{𝑸} B = 1_{𝑸})$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ *_{𝑸} (A) \in V$
2	1	a1i	$⊢ A \in 𝑸 \to *_{𝑸} (A) \in V$
3		eleq1	$⊢ _{𝑸} (A) = B \to (_{𝑸} (A) \in V \leftrightarrow B \in V)$
4	2 3	syl5ibcom	$⊢ A \in 𝑸 \to (*_{𝑸} (A) = B \to B \in V)$
5		id	$⊢ A \cdot_{𝑸} B = 1_{𝑸} \to A \cdot_{𝑸} B = 1_{𝑸}$
6		1nq	$⊢ 1_{𝑸} \in 𝑸$
7	5 6	eqeltrdi	$⊢ A \cdot_{𝑸} B = 1_{𝑸} \to A \cdot_{𝑸} B \in 𝑸$
8		mulnqf	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
9	8	fdmi	$⊢ dom \cdot_{𝑸} = 𝑸 \times 𝑸$
10		0nnq	$⊢ \neg \emptyset \in 𝑸$
11	9 10	ndmovrcl	$⊢ A \cdot_{𝑸} B \in 𝑸 \to (A \in 𝑸 \land B \in 𝑸)$
12	7 11	syl	$⊢ A \cdot_{𝑸} B = 1_{𝑸} \to (A \in 𝑸 \land B \in 𝑸)$
13		elex	$⊢ B \in 𝑸 \to B \in V$
14	12 13	simpl2im	$⊢ A \cdot_{𝑸} B = 1_{𝑸} \to B \in V$
15	14	a1i	$⊢ A \in 𝑸 \to (A \cdot_{𝑸} B = 1_{𝑸} \to B \in V)$
16		oveq1	$⊢ x = A \to x \cdot_{𝑸} y = A \cdot_{𝑸} y$
17	16	eqeq1d	$⊢ x = A \to (x \cdot_{𝑸} y = 1_{𝑸} \leftrightarrow A \cdot_{𝑸} y = 1_{𝑸})$
18		oveq2	$⊢ y = B \to A \cdot_{𝑸} y = A \cdot_{𝑸} B$
19	18	eqeq1d	$⊢ y = B \to (A \cdot_{𝑸} y = 1_{𝑸} \leftrightarrow A \cdot_{𝑸} B = 1_{𝑸})$
20		nqerid	$⊢ x \in 𝑸 \to /_{𝑸} (x) = x$
21		relxp	$⊢ Rel (𝑵 \times 𝑵)$
22		elpqn	$⊢ x \in 𝑸 \to x \in (𝑵 \times 𝑵)$
23		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land x \in (𝑵 \times 𝑵)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
24	21 22 23	sylancr	$⊢ x \in 𝑸 \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
25	24	fveq2d	$⊢ x \in 𝑸 \to /_{𝑸} (x) = /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩)$
26	20 25	eqtr3d	$⊢ x \in 𝑸 \to x = /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩)$
27	26	oveq1d	$⊢ x \in 𝑸 \to x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩) \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩)$
28		mulerpq	$⊢ /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩) \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩)$
29	27 28	eqtrdi	$⊢ x \in 𝑸 \to x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩)$
30		xp1st	$⊢ x \in (𝑵 \times 𝑵) \to 1^{st} (x) \in 𝑵$
31	22 30	syl	$⊢ x \in 𝑸 \to 1^{st} (x) \in 𝑵$
32		xp2nd	$⊢ x \in (𝑵 \times 𝑵) \to 2^{nd} (x) \in 𝑵$
33	22 32	syl	$⊢ x \in 𝑸 \to 2^{nd} (x) \in 𝑵$
34		mulpipq	$⊢ ((1^{st} (x) \in 𝑵 \land 2^{nd} (x) \in 𝑵) \land (2^{nd} (x) \in 𝑵 \land 1^{st} (x) \in 𝑵)) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩ = ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 2^{nd} (x) \cdot_{𝑵} 1^{st} (x)⟩$
35	31 33 33 31 34	syl22anc	$⊢ x \in 𝑸 \to ⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩ = ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 2^{nd} (x) \cdot_{𝑵} 1^{st} (x)⟩$
36		mulcompi	$⊢ 2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)$
37	36	opeq2i	$⊢ ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 2^{nd} (x) \cdot_{𝑵} 1^{st} (x)⟩ = ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩$
38	35 37	eqtrdi	$⊢ x \in 𝑸 \to ⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩ = ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩$
39	38	fveq2d	$⊢ x \in 𝑸 \to /_{𝑸} (⟨1^{st} (x), 2^{nd} (x)⟩ \cdot_{𝑝𝑸} ⟨2^{nd} (x), 1^{st} (x)⟩) = /_{𝑸} (⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩)$
40		nqerid	$⊢ 1_{𝑸} \in 𝑸 \to /_{𝑸} (1_{𝑸}) = 1_{𝑸}$
41	6 40	ax-mp	$⊢ /_{𝑸} (1_{𝑸}) = 1_{𝑸}$
42		mulclpi	$⊢ (1^{st} (x) \in 𝑵 \land 2^{nd} (x) \in 𝑵) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
43	31 33 42	syl2anc	$⊢ x \in 𝑸 \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
44		1nqenq	$⊢ 1^{st} (x) \cdot_{𝑵} 2^{nd} (x) \in 𝑵 \to 1_{𝑸} ~_{𝑸} ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩$
45	43 44	syl	$⊢ x \in 𝑸 \to 1_{𝑸} ~_{𝑸} ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩$
46		elpqn	$⊢ 1_{𝑸} \in 𝑸 \to 1_{𝑸} \in (𝑵 \times 𝑵)$
47	6 46	ax-mp	$⊢ 1_{𝑸} \in (𝑵 \times 𝑵)$
48	43 43	opelxpd	$⊢ x \in 𝑸 \to ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩ \in (𝑵 \times 𝑵)$
49		nqereq	$⊢ (1_{𝑸} \in (𝑵 \times 𝑵) \land ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩ \in (𝑵 \times 𝑵)) \to (1_{𝑸} ~_{𝑸} ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩ \leftrightarrow /_{𝑸} (1_{𝑸}) = /_{𝑸} (⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩))$
50	47 48 49	sylancr	$⊢ x \in 𝑸 \to (1_{𝑸} ~_{𝑸} ⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩ \leftrightarrow /_{𝑸} (1_{𝑸}) = /_{𝑸} (⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩))$
51	45 50	mpbid	$⊢ x \in 𝑸 \to /_{𝑸} (1_{𝑸}) = /_{𝑸} (⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩)$
52	41 51	syl5reqr	$⊢ x \in 𝑸 \to /_{𝑸} (⟨1^{st} (x) \cdot_{𝑵} 2^{nd} (x), 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)⟩) = 1_{𝑸}$
53	29 39 52	3eqtrd	$⊢ x \in 𝑸 \to x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = 1_{𝑸}$
54		fvex	$⊢ /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) \in V$
55		oveq2	$⊢ y = /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) \to x \cdot_{𝑸} y = x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩)$
56	55	eqeq1d	$⊢ y = /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) \to (x \cdot_{𝑸} y = 1_{𝑸} \leftrightarrow x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = 1_{𝑸})$
57	54 56	spcev	$⊢ x \cdot_{𝑸} /_{𝑸} (⟨2^{nd} (x), 1^{st} (x)⟩) = 1_{𝑸} \to \exists y x \cdot_{𝑸} y = 1_{𝑸}$
58	53 57	syl	$⊢ x \in 𝑸 \to \exists y x \cdot_{𝑸} y = 1_{𝑸}$
59		mulcomnq	$⊢ r \cdot_{𝑸} s = s \cdot_{𝑸} r$
60		mulassnq	$⊢ (r \cdot_{𝑸} s) \cdot_{𝑸} t = r \cdot_{𝑸} (s \cdot_{𝑸} t)$
61		mulidnq	$⊢ r \in 𝑸 \to r \cdot_{𝑸} 1_{𝑸} = r$
62	6 9 10 59 60 61	caovmo	$⊢ \exists^{*} y x \cdot_{𝑸} y = 1_{𝑸}$
63		df-eu	$⊢ \exists! y x \cdot_{𝑸} y = 1_{𝑸} \leftrightarrow (\exists y x \cdot_{𝑸} y = 1_{𝑸} \land \exists^{*} y x \cdot_{𝑸} y = 1_{𝑸})$
64	58 62 63	sylanblrc	$⊢ x \in 𝑸 \to \exists! y x \cdot_{𝑸} y = 1_{𝑸}$
65		cnvimass	$⊢ {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}] \subseteq dom \cdot_{𝑸}$
66		df-rq	$⊢ *_{𝑸} = {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}]$
67	9	eqcomi	$⊢ 𝑸 \times 𝑸 = dom \cdot_{𝑸}$
68	65 66 67	3sstr4i	$⊢ *_{𝑸} \subseteq 𝑸 \times 𝑸$
69		relxp	$⊢ Rel (𝑸 \times 𝑸)$
70		relss	$⊢ _{𝑸} \subseteq 𝑸 \times 𝑸 \to (Rel (𝑸 \times 𝑸) \to Rel _{𝑸})$
71	68 69 70	mp2	$⊢ Rel *_{𝑸}$
72	66	eleq2i	$⊢ ⟨x, y⟩ \in *_{𝑸} \leftrightarrow ⟨x, y⟩ \in {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}]$
73		ffn	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸 \to \cdot_{𝑸} Fn (𝑸 \times 𝑸)$
74		fniniseg	$⊢ \cdot_{𝑸} Fn (𝑸 \times 𝑸) \to (⟨x, y⟩ \in {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}] \leftrightarrow (⟨x, y⟩ \in (𝑸 \times 𝑸) \land \cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸}))$
75	8 73 74	mp2b	$⊢ ⟨x, y⟩ \in {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}] \leftrightarrow (⟨x, y⟩ \in (𝑸 \times 𝑸) \land \cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸})$
76		ancom	$⊢ (⟨x, y⟩ \in (𝑸 \times 𝑸) \land \cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸}) \leftrightarrow (\cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸} \land ⟨x, y⟩ \in (𝑸 \times 𝑸))$
77		ancom	$⊢ (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸}) \leftrightarrow (x \cdot_{𝑸} y = 1_{𝑸} \land x \in 𝑸)$
78		eleq1	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to (x \cdot_{𝑸} y \in 𝑸 \leftrightarrow 1_{𝑸} \in 𝑸)$
79	6 78	mpbiri	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to x \cdot_{𝑸} y \in 𝑸$
80	9 10	ndmovrcl	$⊢ x \cdot_{𝑸} y \in 𝑸 \to (x \in 𝑸 \land y \in 𝑸)$
81	79 80	syl	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to (x \in 𝑸 \land y \in 𝑸)$
82		opelxpi	$⊢ (x \in 𝑸 \land y \in 𝑸) \to ⟨x, y⟩ \in (𝑸 \times 𝑸)$
83	81 82	syl	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to ⟨x, y⟩ \in (𝑸 \times 𝑸)$
84	81	simpld	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to x \in 𝑸$
85	83 84	2thd	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \to (⟨x, y⟩ \in (𝑸 \times 𝑸) \leftrightarrow x \in 𝑸)$
86	85	pm5.32i	$⊢ (x \cdot_{𝑸} y = 1_{𝑸} \land ⟨x, y⟩ \in (𝑸 \times 𝑸)) \leftrightarrow (x \cdot_{𝑸} y = 1_{𝑸} \land x \in 𝑸)$
87		df-ov	$⊢ x \cdot_{𝑸} y = \cdot_{𝑸} (⟨x, y⟩)$
88	87	eqeq1i	$⊢ x \cdot_{𝑸} y = 1_{𝑸} \leftrightarrow \cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸}$
89	88	anbi1i	$⊢ (x \cdot_{𝑸} y = 1_{𝑸} \land ⟨x, y⟩ \in (𝑸 \times 𝑸)) \leftrightarrow (\cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸} \land ⟨x, y⟩ \in (𝑸 \times 𝑸))$
90	77 86 89	3bitr2ri	$⊢ (\cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸} \land ⟨x, y⟩ \in (𝑸 \times 𝑸)) \leftrightarrow (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸})$
91	76 90	bitri	$⊢ (⟨x, y⟩ \in (𝑸 \times 𝑸) \land \cdot_{𝑸} (⟨x, y⟩) = 1_{𝑸}) \leftrightarrow (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸})$
92	72 75 91	3bitri	$⊢ ⟨x, y⟩ \in *_{𝑸} \leftrightarrow (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸})$
93	92	a1i	$⊢ ⊤ \to (⟨x, y⟩ \in *_{𝑸} \leftrightarrow (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸}))$
94	71 93	opabbi2dv	$⊢ ⊤ \to *_{𝑸} = \{⟨x, y⟩ \| (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸})\}$
95	94	mptru	$⊢ *_{𝑸} = \{⟨x, y⟩ \| (x \in 𝑸 \land x \cdot_{𝑸} y = 1_{𝑸})\}$
96	17 19 64 95	fvopab3g	$⊢ (A \in 𝑸 \land B \in V) \to (*_{𝑸} (A) = B \leftrightarrow A \cdot_{𝑸} B = 1_{𝑸})$
97	96	ex	$⊢ A \in 𝑸 \to (B \in V \to (*_{𝑸} (A) = B \leftrightarrow A \cdot_{𝑸} B = 1_{𝑸}))$
98	4 15 97	pm5.21ndd	$⊢ A \in 𝑸 \to (*_{𝑸} (A) = B \leftrightarrow A \cdot_{𝑸} B = 1_{𝑸})$

Metamath Proof Explorer

Theorem recmulnq

Proof