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 𝐵 ) = 1_Q ) )

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

Metamath Proof Explorer

Theorem recmulnq

Proof