This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑥 ∈ 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 ‘ 𝐴 ) ) = 𝐴 )