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	⊢ ·Q : ( Q × Q ) ⟶ Q

Proof

Step	Hyp	Ref	Expression
1		nqerf	⊢ [Q] : ( N × N ) ⟶ Q
2		mulpqf	⊢ ·pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
3		fco	⊢ ( ( [Q] : ( N × N ) ⟶ Q ∧ ·pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N ) ) → ( [Q] ∘ ·pQ ) : ( ( N × N ) × ( N × N ) ) ⟶ Q )
4	1 2 3	mp2an	⊢ ( [Q] ∘ ·pQ ) : ( ( N × N ) × ( N × N ) ) ⟶ Q
5		elpqn	⊢ ( 𝑥 ∈ Q → 𝑥 ∈ ( N × N ) )
6	5	ssriv	⊢ Q ⊆ ( N × N )
7		xpss12	⊢ ( ( Q ⊆ ( N × N ) ∧ Q ⊆ ( N × N ) ) → ( Q × Q ) ⊆ ( ( N × N ) × ( N × N ) ) )
8	6 6 7	mp2an	⊢ ( Q × Q ) ⊆ ( ( N × N ) × ( N × N ) )
9		fssres	⊢ ( ( ( [Q] ∘ ·pQ ) : ( ( N × N ) × ( N × N ) ) ⟶ Q ∧ ( Q × Q ) ⊆ ( ( N × N ) × ( N × N ) ) ) → ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) : ( Q × Q ) ⟶ Q )
10	4 8 9	mp2an	⊢ ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) : ( Q × Q ) ⟶ Q
11		df-mq	⊢ ·Q = ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) )
12	11	feq1i	⊢ ( ·Q : ( Q × Q ) ⟶ Q ↔ ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) : ( Q × Q ) ⟶ Q )
13	10 12	mpbir	⊢ ·Q : ( Q × Q ) ⟶ Q