![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulnqf | Structured version Visualization version GIF version |
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 |
---|---|
mulnqf | ⊢ ·Q :(Q × Q)⟶Q |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nqerf 10205 | . . . 4 ⊢ [Q]:(N × N)⟶Q | |
2 | mulpqf 10221 | . . . 4 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N) | |
3 | fco 6406 | . . . 4 ⊢ (([Q]:(N × N)⟶Q ∧ ·pQ :((N × N) × (N × N))⟶(N × N)) → ([Q] ∘ ·pQ ):((N × N) × (N × N))⟶Q) | |
4 | 1, 2, 3 | mp2an 688 | . . 3 ⊢ ([Q] ∘ ·pQ ):((N × N) × (N × N))⟶Q |
5 | elpqn 10200 | . . . . 5 ⊢ (𝑥 ∈ Q → 𝑥 ∈ (N × N)) | |
6 | 5 | ssriv 3899 | . . . 4 ⊢ Q ⊆ (N × N) |
7 | xpss12 5465 | . . . 4 ⊢ ((Q ⊆ (N × N) ∧ Q ⊆ (N × N)) → (Q × Q) ⊆ ((N × N) × (N × N))) | |
8 | 6, 6, 7 | mp2an 688 | . . 3 ⊢ (Q × Q) ⊆ ((N × N) × (N × N)) |
9 | fssres 6419 | . . 3 ⊢ ((([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 688 | . 2 ⊢ (([Q] ∘ ·pQ ) ↾ (Q × Q)):(Q × Q)⟶Q |
11 | df-mq 10190 | . . 3 ⊢ ·Q = (([Q] ∘ ·pQ ) ↾ (Q × Q)) | |
12 | 11 | feq1i 6380 | . 2 ⊢ ( ·Q :(Q × Q)⟶Q ↔ (([Q] ∘ ·pQ ) ↾ (Q × Q)):(Q × Q)⟶Q) |
13 | 10, 12 | mpbir 232 | 1 ⊢ ·Q :(Q × Q)⟶Q |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3865 × cxp 5448 ↾ cres 5452 ∘ ccom 5454 ⟶wf 6228 Ncnpi 10119 ·pQ cmpq 10124 Qcnq 10127 [Q]cerq 10129 ·Q cmq 10131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-1st 7552 df-2nd 7553 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-1o 7960 df-oadd 7964 df-omul 7965 df-er 8146 df-ni 10147 df-mi 10149 df-lti 10150 df-mpq 10184 df-enq 10186 df-nq 10187 df-erq 10188 df-mq 10190 df-1nq 10191 |
This theorem is referenced by: mulcomnq 10228 mulerpq 10232 mulassnq 10234 distrnq 10236 recmulnq 10239 recclnq 10241 dmrecnq 10243 ltmnq 10247 prlem936 10322 |
Copyright terms: Public domain | W3C validator |