Theorem recrecnq

Description: Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 29-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	recrecnq	$$⊢A\in 𝑸\to {*}_{𝑸}\left({*}_{𝑸}\left(A\right)\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		2fveq3	$$⊢x=A\to {*}_{𝑸}\left({*}_{𝑸}\left(x\right)\right)={*}_{𝑸}\left({*}_{𝑸}\left(A\right)\right)$$
2		id	$$⊢x=A\to x=A$$
3	1 2	eqeq12d	$$⊢x=A\to \left({*}_{𝑸}\left({*}_{𝑸}\left(x\right)\right)=x\leftrightarrow {*}_{𝑸}\left({*}_{𝑸}\left(A\right)\right)=A\right)$$
4		mulcomnq	$$⊢{*}_{𝑸}\left(x\right){\cdot }_{𝑸}x=x{\cdot }_{𝑸}{*}_{𝑸}\left(x\right)$$
5		recidnq	$$⊢x\in 𝑸\to x{\cdot }_{𝑸}{*}_{𝑸}\left(x\right)=1_{𝑸}$$
6	4 5	syl5eq	$$⊢x\in 𝑸\to {*}_{𝑸}\left(x\right){\cdot }_{𝑸}x=1_{𝑸}$$
7		recclnq	$$⊢x\in 𝑸\to {*}_{𝑸}\left(x\right)\in 𝑸$$
8		recmulnq	$$⊢{*}_{𝑸}\left(x\right)\in 𝑸\to \left({*}_{𝑸}\left({*}_{𝑸}\left(x\right)\right)=x\leftrightarrow {*}_{𝑸}\left(x\right){\cdot }_{𝑸}x=1_{𝑸}\right)$$
9	7 8	syl	$$⊢x\in 𝑸\to \left({*}_{𝑸}\left({*}_{𝑸}\left(x\right)\right)=x\leftrightarrow {*}_{𝑸}\left(x\right){\cdot }_{𝑸}x=1_{𝑸}\right)$$
10	6 9	mpbird	$$⊢x\in 𝑸\to {*}_{𝑸}\left({*}_{𝑸}\left(x\right)\right)=x$$
11	3 10	vtoclga	$$⊢A\in 𝑸\to {*}_{𝑸}\left({*}_{𝑸}\left(A\right)\right)=A$$