Theorem 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	⊢ ( 𝐴 ∈ Q → ( ( *Q ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 ·Q 𝐵 ) = 1Q ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( *Q ‘ 𝐴 ) ∈ V
2	1	a1i	⊢ ( 𝐴 ∈ Q → ( *Q ‘ 𝐴 ) ∈ V )
3		eleq1	⊢ ( ( *Q ‘ 𝐴 ) = 𝐵 → ( ( *Q ‘ 𝐴 ) ∈ V ↔ 𝐵 ∈ V ) )
4	2 3	syl5ibcom	⊢ ( 𝐴 ∈ Q → ( ( *Q ‘ 𝐴 ) = 𝐵 → 𝐵 ∈ V ) )
5		id	⊢ ( ( 𝐴 ·Q 𝐵 ) = 1Q → ( 𝐴 ·Q 𝐵 ) = 1Q )
6		1nq	⊢ 1Q ∈ Q
7	5 6	eqeltrdi	⊢ ( ( 𝐴 ·Q 𝐵 ) = 1Q → ( 𝐴 ·Q 𝐵 ) ∈ Q )
8		mulnqf	⊢ ·Q : ( Q × Q ) ⟶ Q
9	8	fdmi	⊢ dom ·Q = ( Q × Q )
10		0nnq	⊢ ¬ ∅ ∈ Q
11	9 10	ndmovrcl	⊢ ( ( 𝐴 ·Q 𝐵 ) ∈ Q → ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) )
12	7 11	syl	⊢ ( ( 𝐴 ·Q 𝐵 ) = 1Q → ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) )
13		elex	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ V )
14	12 13	simpl2im	⊢ ( ( 𝐴 ·Q 𝐵 ) = 1Q → 𝐵 ∈ V )
15	14	a1i	⊢ ( 𝐴 ∈ Q → ( ( 𝐴 ·Q 𝐵 ) = 1Q → 𝐵 ∈ V ) )
16		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·Q 𝑦 ) = ( 𝐴 ·Q 𝑦 ) )
17	16	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·Q 𝑦 ) = 1Q ↔ ( 𝐴 ·Q 𝑦 ) = 1Q ) )
18		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ·Q 𝑦 ) = ( 𝐴 ·Q 𝐵 ) )
19	18	eqeq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ·Q 𝑦 ) = 1Q ↔ ( 𝐴 ·Q 𝐵 ) = 1Q ) )
20		nqerid	⊢ ( 𝑥 ∈ Q → ( [Q] ‘ 𝑥 ) = 𝑥 )
21		relxp	⊢ Rel ( N × N )
22		elpqn	⊢ ( 𝑥 ∈ Q → 𝑥 ∈ ( N × N ) )
23		1st2nd	⊢ ( ( Rel ( N × N ) ∧ 𝑥 ∈ ( N × N ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
24	21 22 23	sylancr	⊢ ( 𝑥 ∈ Q → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
25	24	fveq2d	⊢ ( 𝑥 ∈ Q → ( [Q] ‘ 𝑥 ) = ( [Q] ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
26	20 25	eqtr3d	⊢ ( 𝑥 ∈ Q → 𝑥 = ( [Q] ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
27	26	oveq1d	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = ( ( [Q] ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) )
28		mulerpq	⊢ ( ( [Q] ‘ ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = ( [Q] ‘ ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) )
29	27 28	eqtrdi	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = ( [Q] ‘ ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) )
30		xp1st	⊢ ( 𝑥 ∈ ( N × N ) → ( 1st ‘ 𝑥 ) ∈ N )
31	22 30	syl	⊢ ( 𝑥 ∈ Q → ( 1st ‘ 𝑥 ) ∈ N )
32		xp2nd	⊢ ( 𝑥 ∈ ( N × N ) → ( 2nd ‘ 𝑥 ) ∈ N )
33	22 32	syl	⊢ ( 𝑥 ∈ Q → ( 2nd ‘ 𝑥 ) ∈ N )
34		mulpipq	⊢ ( ( ( ( 1st ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑥 ) ∈ N ) ∧ ( ( 2nd ‘ 𝑥 ) ∈ N ∧ ( 1st ‘ 𝑥 ) ∈ N ) ) → ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) = ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) ⟩ )
35	31 33 33 31 34	syl22anc	⊢ ( 𝑥 ∈ Q → ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) = ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) ⟩ )
36		mulcompi	⊢ ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) )
37	36	opeq2i	⊢ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 1st ‘ 𝑥 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩
38	35 37	eqtrdi	⊢ ( 𝑥 ∈ Q → ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) = ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ )
39	38	fveq2d	⊢ ( 𝑥 ∈ Q → ( [Q] ‘ ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ·pQ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = ( [Q] ‘ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ) )
40		mulclpi	⊢ ( ( ( 1st ‘ 𝑥 ) ∈ N ∧ ( 2nd ‘ 𝑥 ) ∈ N ) → ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ∈ N )
41	31 33 40	syl2anc	⊢ ( 𝑥 ∈ Q → ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ∈ N )
42		1nqenq	⊢ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ∈ N → 1Q ~Q ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ )
43	41 42	syl	⊢ ( 𝑥 ∈ Q → 1Q ~Q ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ )
44		elpqn	⊢ ( 1Q ∈ Q → 1Q ∈ ( N × N ) )
45	6 44	ax-mp	⊢ 1Q ∈ ( N × N )
46	41 41	opelxpd	⊢ ( 𝑥 ∈ Q → ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ∈ ( N × N ) )
47		nqereq	⊢ ( ( 1Q ∈ ( N × N ) ∧ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ∈ ( N × N ) ) → ( 1Q ~Q ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ↔ ( [Q] ‘ 1Q ) = ( [Q] ‘ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ) ) )
48	45 46 47	sylancr	⊢ ( 𝑥 ∈ Q → ( 1Q ~Q ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ↔ ( [Q] ‘ 1Q ) = ( [Q] ‘ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ) ) )
49	43 48	mpbid	⊢ ( 𝑥 ∈ Q → ( [Q] ‘ 1Q ) = ( [Q] ‘ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ) )
50		nqerid	⊢ ( 1Q ∈ Q → ( [Q] ‘ 1Q ) = 1Q )
51	6 50	ax-mp	⊢ ( [Q] ‘ 1Q ) = 1Q
52	49 51	eqtr3di	⊢ ( 𝑥 ∈ Q → ( [Q] ‘ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) , ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑥 ) ) ⟩ ) = 1Q )
53	29 39 52	3eqtrd	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = 1Q )
54		fvex	⊢ ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ∈ V
55		oveq2	⊢ ( 𝑦 = ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) → ( 𝑥 ·Q 𝑦 ) = ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) )
56	55	eqeq1d	⊢ ( 𝑦 = ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) → ( ( 𝑥 ·Q 𝑦 ) = 1Q ↔ ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = 1Q ) )
57	54 56	spcev	⊢ ( ( 𝑥 ·Q ( [Q] ‘ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ ) ) = 1Q → ∃ 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q )
58	53 57	syl	⊢ ( 𝑥 ∈ Q → ∃ 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q )
59		mulcomnq	⊢ ( 𝑟 ·Q 𝑠 ) = ( 𝑠 ·Q 𝑟 )
60		mulassnq	⊢ ( ( 𝑟 ·Q 𝑠 ) ·Q 𝑡 ) = ( 𝑟 ·Q ( 𝑠 ·Q 𝑡 ) )
61		mulidnq	⊢ ( 𝑟 ∈ Q → ( 𝑟 ·Q 1Q ) = 𝑟 )
62	6 9 10 59 60 61	caovmo	⊢ ∃* 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q
63		df-eu	⊢ ( ∃! 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q ↔ ( ∃ 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q ∧ ∃* 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q ) )
64	58 62 63	sylanblrc	⊢ ( 𝑥 ∈ Q → ∃! 𝑦 ( 𝑥 ·Q 𝑦 ) = 1Q )
65		cnvimass	⊢ ( ◡ ·Q “ { 1Q } ) ⊆ dom ·Q
66		df-rq	⊢ *Q = ( ◡ ·Q “ { 1Q } )
67	9	eqcomi	⊢ ( Q × Q ) = dom ·Q
68	65 66 67	3sstr4i	⊢ *Q ⊆ ( Q × Q )
69		relxp	⊢ Rel ( Q × Q )
70		relss	⊢ ( *Q ⊆ ( Q × Q ) → ( Rel ( Q × Q ) → Rel *Q ) )
71	68 69 70	mp2	⊢ Rel *Q
72	66	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ *Q ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ·Q “ { 1Q } ) )
73		ffn	⊢ ( ·Q : ( Q × Q ) ⟶ Q → ·Q Fn ( Q × Q ) )
74		fniniseg	⊢ ( ·Q Fn ( Q × Q ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ·Q “ { 1Q } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ) ) )
75	8 73 74	mp2b	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ·Q “ { 1Q } ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ) )
76		ancom	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ) ↔ ( ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ) )
77		ancom	⊢ ( ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) ↔ ( ( 𝑥 ·Q 𝑦 ) = 1Q ∧ 𝑥 ∈ Q ) )
78		eleq1	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → ( ( 𝑥 ·Q 𝑦 ) ∈ Q ↔ 1Q ∈ Q ) )
79	6 78	mpbiri	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → ( 𝑥 ·Q 𝑦 ) ∈ Q )
80	9 10	ndmovrcl	⊢ ( ( 𝑥 ·Q 𝑦 ) ∈ Q → ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) )
81	79 80	syl	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) )
82		opelxpi	⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) )
83	81 82	syl	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) )
84	81	simpld	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → 𝑥 ∈ Q )
85	83 84	2thd	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ↔ 𝑥 ∈ Q ) )
86	85	pm5.32i	⊢ ( ( ( 𝑥 ·Q 𝑦 ) = 1Q ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) = 1Q ∧ 𝑥 ∈ Q ) )
87		df-ov	⊢ ( 𝑥 ·Q 𝑦 ) = ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ )
88	87	eqeq1i	⊢ ( ( 𝑥 ·Q 𝑦 ) = 1Q ↔ ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q )
89	88	anbi1i	⊢ ( ( ( 𝑥 ·Q 𝑦 ) = 1Q ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ) ↔ ( ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ) )
90	77 86 89	3bitr2ri	⊢ ( ( ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ) ↔ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) )
91	76 90	bitri	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 1Q ) ↔ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) )
92	72 75 91	3bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ *Q ↔ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) )
93	92	a1i	⊢ ( ⊤ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ *Q ↔ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) ) )
94	71 93	opabbi2dv	⊢ ( ⊤ → *Q = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) } )
95	94	mptru	⊢ *Q = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ Q ∧ ( 𝑥 ·Q 𝑦 ) = 1Q ) }
96	17 19 64 95	fvopab3g	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ V ) → ( ( *Q ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 ·Q 𝐵 ) = 1Q ) )
97	96	ex	⊢ ( 𝐴 ∈ Q → ( 𝐵 ∈ V → ( ( *Q ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 ·Q 𝐵 ) = 1Q ) ) )
98	4 15 97	pm5.21ndd	⊢ ( 𝐴 ∈ Q → ( ( *Q ‘ 𝐴 ) = 𝐵 ↔ ( 𝐴 ·Q 𝐵 ) = 1Q ) )