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 ) = 𝐴 )