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

Metamath Proof Explorer

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_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
3		fco	$⊢ (/_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸 \land \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵) \to (/_{𝑸} \circ \cdot_{𝑝𝑸}) : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑸$
4	1 2 3	mp2an	$⊢ (/_{𝑸} \circ \cdot_{𝑝𝑸}) : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑸$
5		elpqn	$⊢ x \in 𝑸 \to x \in (𝑵 \times 𝑵)$
6	5	ssriv	$⊢ 𝑸 \subseteq 𝑵 \times 𝑵$
7		xpss12	$⊢ (𝑸 \subseteq 𝑵 \times 𝑵 \land 𝑸 \subseteq 𝑵 \times 𝑵) \to 𝑸 \times 𝑸 \subseteq (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
8	6 6 7	mp2an	$⊢ 𝑸 \times 𝑸 \subseteq (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
9		fssres	$⊢ ((/_{𝑸} \circ \cdot_{𝑝𝑸}) : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑸 \land 𝑸 \times 𝑸 \subseteq (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)) \to ({(/_{𝑸} \circ \cdot_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸) : 𝑸 \times 𝑸 ⟶ 𝑸$
10	4 8 9	mp2an	$⊢ ({(/_{𝑸} \circ \cdot_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸) : 𝑸 \times 𝑸 ⟶ 𝑸$
11		df-mq	$⊢ \cdot_{𝑸} = {(/_{𝑸} \circ \cdot_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸$
12	11	feq1i	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸 \leftrightarrow ({(/_{𝑸} \circ \cdot_{𝑝𝑸}) ↾}_{(𝑸)} \times 𝑸) : 𝑸 \times 𝑸 ⟶ 𝑸$
13	10 12	mpbir	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$