Metamath Proof Explorer


Theorem mulidnq

Description: Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion mulidnq A𝑸A𝑸1𝑸=A

Proof

Step Hyp Ref Expression
1 1nq 1𝑸𝑸
2 mulpqnq A𝑸1𝑸𝑸A𝑸1𝑸=/𝑸A𝑝𝑸1𝑸
3 1 2 mpan2 A𝑸A𝑸1𝑸=/𝑸A𝑝𝑸1𝑸
4 relxp Rel𝑵×𝑵
5 elpqn A𝑸A𝑵×𝑵
6 1st2nd Rel𝑵×𝑵A𝑵×𝑵A=1stA2ndA
7 4 5 6 sylancr A𝑸A=1stA2ndA
8 df-1nq 1𝑸=1𝑜1𝑜
9 8 a1i A𝑸1𝑸=1𝑜1𝑜
10 7 9 oveq12d A𝑸A𝑝𝑸1𝑸=1stA2ndA𝑝𝑸1𝑜1𝑜
11 xp1st A𝑵×𝑵1stA𝑵
12 5 11 syl A𝑸1stA𝑵
13 xp2nd A𝑵×𝑵2ndA𝑵
14 5 13 syl A𝑸2ndA𝑵
15 1pi 1𝑜𝑵
16 15 a1i A𝑸1𝑜𝑵
17 mulpipq 1stA𝑵2ndA𝑵1𝑜𝑵1𝑜𝑵1stA2ndA𝑝𝑸1𝑜1𝑜=1stA𝑵1𝑜2ndA𝑵1𝑜
18 12 14 16 16 17 syl22anc A𝑸1stA2ndA𝑝𝑸1𝑜1𝑜=1stA𝑵1𝑜2ndA𝑵1𝑜
19 mulidpi 1stA𝑵1stA𝑵1𝑜=1stA
20 11 19 syl A𝑵×𝑵1stA𝑵1𝑜=1stA
21 mulidpi 2ndA𝑵2ndA𝑵1𝑜=2ndA
22 13 21 syl A𝑵×𝑵2ndA𝑵1𝑜=2ndA
23 20 22 opeq12d A𝑵×𝑵1stA𝑵1𝑜2ndA𝑵1𝑜=1stA2ndA
24 5 23 syl A𝑸1stA𝑵1𝑜2ndA𝑵1𝑜=1stA2ndA
25 10 18 24 3eqtrd A𝑸A𝑝𝑸1𝑸=1stA2ndA
26 25 7 eqtr4d A𝑸A𝑝𝑸1𝑸=A
27 26 fveq2d A𝑸/𝑸A𝑝𝑸1𝑸=/𝑸A
28 nqerid A𝑸/𝑸A=A
29 3 27 28 3eqtrd A𝑸A𝑸1𝑸=A