![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulidnq | Structured version Visualization version GIF version |
Description: Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
mulidnq | ⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nq 10146 | . . 3 ⊢ 1Q ∈ Q | |
2 | mulpqnq 10159 | . . 3 ⊢ ((𝐴 ∈ Q ∧ 1Q ∈ Q) → (𝐴 ·Q 1Q) = ([Q]‘(𝐴 ·pQ 1Q))) | |
3 | 1, 2 | mpan2 679 | . 2 ⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = ([Q]‘(𝐴 ·pQ 1Q))) |
4 | relxp 5421 | . . . . . . 7 ⊢ Rel (N × N) | |
5 | elpqn 10143 | . . . . . . 7 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) | |
6 | 1st2nd 7548 | . . . . . . 7 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | |
7 | 4, 5, 6 | sylancr 579 | . . . . . 6 ⊢ (𝐴 ∈ Q → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
8 | df-1nq 10134 | . . . . . . 7 ⊢ 1Q = 〈1o, 1o〉 | |
9 | 8 | a1i 11 | . . . . . 6 ⊢ (𝐴 ∈ Q → 1Q = 〈1o, 1o〉) |
10 | 7, 9 | oveq12d 6992 | . . . . 5 ⊢ (𝐴 ∈ Q → (𝐴 ·pQ 1Q) = (〈(1st ‘𝐴), (2nd ‘𝐴)〉 ·pQ 〈1o, 1o〉)) |
11 | xp1st 7531 | . . . . . . 7 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N) | |
12 | 5, 11 | syl 17 | . . . . . 6 ⊢ (𝐴 ∈ Q → (1st ‘𝐴) ∈ N) |
13 | xp2nd 7532 | . . . . . . 7 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N) | |
14 | 5, 13 | syl 17 | . . . . . 6 ⊢ (𝐴 ∈ Q → (2nd ‘𝐴) ∈ N) |
15 | 1pi 10101 | . . . . . . 7 ⊢ 1o ∈ N | |
16 | 15 | a1i 11 | . . . . . 6 ⊢ (𝐴 ∈ Q → 1o ∈ N) |
17 | mulpipq 10158 | . . . . . 6 ⊢ ((((1st ‘𝐴) ∈ N ∧ (2nd ‘𝐴) ∈ N) ∧ (1o ∈ N ∧ 1o ∈ N)) → (〈(1st ‘𝐴), (2nd ‘𝐴)〉 ·pQ 〈1o, 1o〉) = 〈((1st ‘𝐴) ·N 1o), ((2nd ‘𝐴) ·N 1o)〉) | |
18 | 12, 14, 16, 16, 17 | syl22anc 827 | . . . . 5 ⊢ (𝐴 ∈ Q → (〈(1st ‘𝐴), (2nd ‘𝐴)〉 ·pQ 〈1o, 1o〉) = 〈((1st ‘𝐴) ·N 1o), ((2nd ‘𝐴) ·N 1o)〉) |
19 | mulidpi 10104 | . . . . . . . 8 ⊢ ((1st ‘𝐴) ∈ N → ((1st ‘𝐴) ·N 1o) = (1st ‘𝐴)) | |
20 | 11, 19 | syl 17 | . . . . . . 7 ⊢ (𝐴 ∈ (N × N) → ((1st ‘𝐴) ·N 1o) = (1st ‘𝐴)) |
21 | mulidpi 10104 | . . . . . . . 8 ⊢ ((2nd ‘𝐴) ∈ N → ((2nd ‘𝐴) ·N 1o) = (2nd ‘𝐴)) | |
22 | 13, 21 | syl 17 | . . . . . . 7 ⊢ (𝐴 ∈ (N × N) → ((2nd ‘𝐴) ·N 1o) = (2nd ‘𝐴)) |
23 | 20, 22 | opeq12d 4681 | . . . . . 6 ⊢ (𝐴 ∈ (N × N) → 〈((1st ‘𝐴) ·N 1o), ((2nd ‘𝐴) ·N 1o)〉 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
24 | 5, 23 | syl 17 | . . . . 5 ⊢ (𝐴 ∈ Q → 〈((1st ‘𝐴) ·N 1o), ((2nd ‘𝐴) ·N 1o)〉 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
25 | 10, 18, 24 | 3eqtrd 2811 | . . . 4 ⊢ (𝐴 ∈ Q → (𝐴 ·pQ 1Q) = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
26 | 25, 7 | eqtr4d 2810 | . . 3 ⊢ (𝐴 ∈ Q → (𝐴 ·pQ 1Q) = 𝐴) |
27 | 26 | fveq2d 6500 | . 2 ⊢ (𝐴 ∈ Q → ([Q]‘(𝐴 ·pQ 1Q)) = ([Q]‘𝐴)) |
28 | nqerid 10151 | . 2 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴) | |
29 | 3, 27, 28 | 3eqtrd 2811 | 1 ⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∈ wcel 2051 〈cop 4441 × cxp 5401 Rel wrel 5408 ‘cfv 6185 (class class class)co 6974 1st c1st 7497 2nd c2nd 7498 1oc1o 7896 Ncnpi 10062 ·N cmi 10064 ·pQ cmpq 10067 Qcnq 10070 1Qc1q 10071 [Q]cerq 10072 ·Q cmq 10074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-1st 7499 df-2nd 7500 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-oadd 7907 df-omul 7908 df-er 8087 df-ni 10090 df-mi 10092 df-lti 10093 df-mpq 10127 df-enq 10129 df-nq 10130 df-erq 10131 df-mq 10133 df-1nq 10134 |
This theorem is referenced by: recmulnq 10182 ltaddnq 10192 halfnq 10194 ltrnq 10197 addclprlem1 10234 addclprlem2 10235 mulclprlem 10237 1idpr 10247 prlem934 10251 prlem936 10265 reclem3pr 10267 |
Copyright terms: Public domain | W3C validator |