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 ·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