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	⊢ ( 𝐴 ∈ Q → ( *Q ‘ ( *Q ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑥 = 𝐴 → ( *Q ‘ ( *Q ‘ 𝑥 ) ) = ( *Q ‘ ( *Q ‘ 𝐴 ) ) )
2		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
3	1 2	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( *Q ‘ ( *Q ‘ 𝑥 ) ) = 𝑥 ↔ ( *Q ‘ ( *Q ‘ 𝐴 ) ) = 𝐴 ) )
4		mulcomnq	⊢ ( ( *Q ‘ 𝑥 ) ·Q 𝑥 ) = ( 𝑥 ·Q ( *Q ‘ 𝑥 ) )
5		recidnq	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) = 1Q )
6	4 5	syl5eq	⊢ ( 𝑥 ∈ Q → ( ( *Q ‘ 𝑥 ) ·Q 𝑥 ) = 1Q )
7		recclnq	⊢ ( 𝑥 ∈ Q → ( *Q ‘ 𝑥 ) ∈ Q )
8		recmulnq	⊢ ( ( *Q ‘ 𝑥 ) ∈ Q → ( ( *Q ‘ ( *Q ‘ 𝑥 ) ) = 𝑥 ↔ ( ( *Q ‘ 𝑥 ) ·Q 𝑥 ) = 1Q ) )
9	7 8	syl	⊢ ( 𝑥 ∈ Q → ( ( *Q ‘ ( *Q ‘ 𝑥 ) ) = 𝑥 ↔ ( ( *Q ‘ 𝑥 ) ·Q 𝑥 ) = 1Q ) )
10	6 9	mpbird	⊢ ( 𝑥 ∈ Q → ( *Q ‘ ( *Q ‘ 𝑥 ) ) = 𝑥 )
11	3 10	vtoclga	⊢ ( 𝐴 ∈ Q → ( *Q ‘ ( *Q ‘ 𝐴 ) ) = 𝐴 )