Theorem mulnqf

Description: Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	mulnqf	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸$$

Proof

Step	Hyp	Ref	Expression
1		nqerf	$$⊢{/}_{𝑸}:𝑵\times 𝑵⟶𝑸$$
2		mulpqf	$$⊢{\cdot }_{\mathrm{𝑝𝑸}}:\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑵\times 𝑵$$
3		fco	$$⊢\left({/}_{𝑸}:𝑵\times 𝑵⟶𝑸\wedge {\cdot }_{\mathrm{𝑝𝑸}}:\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑵\times 𝑵\right)\to \left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right):\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑸$$
4	1 2 3	mp2an	$$⊢\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right):\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑸$$
5		elpqn	$$⊢x\in 𝑸\to x\in \left(𝑵\times 𝑵\right)$$
6	5	ssriv	$$⊢𝑸\subseteq 𝑵\times 𝑵$$
7		xpss12	$$⊢\left(𝑸\subseteq 𝑵\times 𝑵\wedge 𝑸\subseteq 𝑵\times 𝑵\right)\to 𝑸\times 𝑸\subseteq \left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)$$
8	6 6 7	mp2an	$$⊢𝑸\times 𝑸\subseteq \left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)$$
9		fssres	$$⊢\left(\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right):\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑸\wedge 𝑸\times 𝑸\subseteq \left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)\to \left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right):𝑸\times 𝑸⟶𝑸$$
10	4 8 9	mp2an	$$⊢\left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right):𝑸\times 𝑸⟶𝑸$$
11		df-mq	$$⊢{\cdot }_{𝑸}={\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)}\times 𝑸$$
12	11	feq1i	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸\leftrightarrow \left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right):𝑸\times 𝑸⟶𝑸$$
13	10 12	mpbir	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸$$