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	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{1}_{𝑸}=A$$

Proof

Step	Hyp	Ref	Expression
1		1nq	$$⊢1_{𝑸}\in 𝑸$$
2		mulpqnq	$$⊢\left(A\in 𝑸\wedge 1_{𝑸}\in 𝑸\right)\to A{\cdot }_{𝑸}{1}_{𝑸}={/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
3	1 2	mpan2	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{1}_{𝑸}={/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)$$
4		relxp	$$⊢\mathrm{Rel}\left(𝑵\times 𝑵\right)$$
5		elpqn	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$
6		1st2nd	$$⊢\left(\mathrm{Rel}\left(𝑵\times 𝑵\right)\wedge A\in \left(𝑵\times 𝑵\right)\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
7	4 5 6	sylancr	$$⊢A\in 𝑸\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
8		df-1nq	$$⊢1_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$
9	8	a1i	$$⊢A\in 𝑸\to 1_{𝑸}=⟨1_{𝑜},1_{𝑜}⟩$$
10	7 9	oveq12d	$$⊢A\in 𝑸\to A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩{\cdot }_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩$$
11		xp1st	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(A\right)\in 𝑵$$
12	5 11	syl	$$⊢A\in 𝑸\to 1^{st}\left(A\right)\in 𝑵$$
13		xp2nd	$$⊢A\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left(A\right)\in 𝑵$$
14	5 13	syl	$$⊢A\in 𝑸\to 2^{nd}\left(A\right)\in 𝑵$$
15		1pi	$$⊢1_{𝑜}\in 𝑵$$
16	15	a1i	$$⊢A\in 𝑸\to 1_{𝑜}\in 𝑵$$
17		mulpipq	$$⊢\left(\left(1^{st}\left(A\right)\in 𝑵\wedge 2^{nd}\left(A\right)\in 𝑵\right)\wedge \left(1_{𝑜}\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\right)\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩{\cdot }_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩=⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜},2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}⟩$$
18	12 14 16 16 17	syl22anc	$$⊢A\in 𝑸\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩{\cdot }_{\mathrm{𝑝𝑸}}⟨1_{𝑜},1_{𝑜}⟩=⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜},2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}⟩$$
19		mulidpi	$$⊢1^{st}\left(A\right)\in 𝑵\to 1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right)$$
20	11 19	syl	$$⊢A\in \left(𝑵\times 𝑵\right)\to 1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=1^{st}\left(A\right)$$
21		mulidpi	$$⊢2^{nd}\left(A\right)\in 𝑵\to 2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=2^{nd}\left(A\right)$$
22	13 21	syl	$$⊢A\in \left(𝑵\times 𝑵\right)\to 2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}=2^{nd}\left(A\right)$$
23	20 22	opeq12d	$$⊢A\in \left(𝑵\times 𝑵\right)\to ⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜},2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}⟩=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
24	5 23	syl	$$⊢A\in 𝑸\to ⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}_{𝑜},2^{nd}\left(A\right){\cdot }_{𝑵}{1}_{𝑜}⟩=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
25	10 18 24	3eqtrd	$$⊢A\in 𝑸\to A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
26	25 7	eqtr4d	$$⊢A\in 𝑸\to A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}=A$$
27	26	fveq2d	$$⊢A\in 𝑸\to {/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}{1}_{𝑸}\right)={/}_{𝑸}\left(A\right)$$
28		nqerid	$$⊢A\in 𝑸\to {/}_{𝑸}\left(A\right)=A$$
29	3 27 28	3eqtrd	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{1}_{𝑸}=A$$