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 ( 𝐴 ∈ Q → ( 𝐴 ·Q 1Q ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 1nq ⊢ 1Q ∈ Q
2 mulpqnq ⊢ ( ( 𝐴 ∈ Q ∧ 1Q ∈ Q ) → ( 𝐴 ·Q 1Q ) = ( [Q] ‘ ( 𝐴 ·pQ 1Q ) ) )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ Q → ( 𝐴 ·Q 1Q ) = ( [Q] ‘ ( 𝐴 ·pQ 1Q ) ) )
4 relxp ⊢ Rel ( N × N )
5 elpqn ⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
6 1st2nd ⊢ ( ( Rel ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
7 4 5 6 sylancr ⊢ ( 𝐴 ∈ Q → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
8 df-1nq ⊢ 1Q = ⟨ 1o , 1o ⟩
9 8 a1i ⊢ ( 𝐴 ∈ Q → 1Q = ⟨ 1o , 1o ⟩ )
10 7 9 oveq12d ⊢ ( 𝐴 ∈ Q → ( 𝐴 ·pQ 1Q ) = ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ·pQ ⟨ 1o , 1o ⟩ ) )
11 xp1st ⊢ ( 𝐴 ∈ ( N × N ) → ( 1st ‘ 𝐴 ) ∈ N )
12 5 11 syl ⊢ ( 𝐴 ∈ Q → ( 1st ‘ 𝐴 ) ∈ N )
13 xp2nd ⊢ ( 𝐴 ∈ ( N × N ) → ( 2nd ‘ 𝐴 ) ∈ N )
14 5 13 syl ⊢ ( 𝐴 ∈ Q → ( 2nd ‘ 𝐴 ) ∈ N )
15 1pi ⊢ 1o ∈ N
16 15 a1i ⊢ ( 𝐴 ∈ Q → 1o ∈ N )
17 mulpipq ⊢ ( ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐴 ) ∈ N ) ∧ ( 1o ∈ N ∧ 1o ∈ N ) ) → ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ·pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N 1o ) , ( ( 2nd ‘ 𝐴 ) ·N 1o ) ⟩ )
18 12 14 16 16 17 syl22anc ⊢ ( 𝐴 ∈ Q → ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ·pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N 1o ) , ( ( 2nd ‘ 𝐴 ) ·N 1o ) ⟩ )
19 mulidpi ⊢ ( ( 1st ‘ 𝐴 ) ∈ N → ( ( 1st ‘ 𝐴 ) ·N 1o ) = ( 1st ‘ 𝐴 ) )
20 11 19 syl ⊢ ( 𝐴 ∈ ( N × N ) → ( ( 1st ‘ 𝐴 ) ·N 1o ) = ( 1st ‘ 𝐴 ) )
21 mulidpi ⊢ ( ( 2nd ‘ 𝐴 ) ∈ N → ( ( 2nd ‘ 𝐴 ) ·N 1o ) = ( 2nd ‘ 𝐴 ) )
22 13 21 syl ⊢ ( 𝐴 ∈ ( N × N ) → ( ( 2nd ‘ 𝐴 ) ·N 1o ) = ( 2nd ‘ 𝐴 ) )
23 20 22 opeq12d ⊢ ( 𝐴 ∈ ( N × N ) → ⟨ ( ( 1st ‘ 𝐴 ) ·N 1o ) , ( ( 2nd ‘ 𝐴 ) ·N 1o ) ⟩ = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
24 5 23 syl ⊢ ( 𝐴 ∈ Q → ⟨ ( ( 1st ‘ 𝐴 ) ·N 1o ) , ( ( 2nd ‘ 𝐴 ) ·N 1o ) ⟩ = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
25 10 18 24 3eqtrd ⊢ ( 𝐴 ∈ Q → ( 𝐴 ·pQ 1Q ) = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
26 25 7 eqtr4d ⊢ ( 𝐴 ∈ Q → ( 𝐴 ·pQ 1Q ) = 𝐴 )
27 26 fveq2d ⊢ ( 𝐴 ∈ Q → ( [Q] ‘ ( 𝐴 ·pQ 1Q ) ) = ( [Q] ‘ 𝐴 ) )
28 nqerid ⊢ ( 𝐴 ∈ Q → ( [Q] ‘ 𝐴 ) = 𝐴 )
29 3 27 28 3eqtrd ⊢ ( 𝐴 ∈ Q → ( 𝐴 ·Q 1Q ) = 𝐴 )