![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adddir | Structured version Visualization version GIF version |
Description: Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Ref | Expression |
---|---|
adddir | โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adddi 11141 | . . 3 โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (๐ถ ยท (๐ด + ๐ต)) = ((๐ถ ยท ๐ด) + (๐ถ ยท ๐ต))) | |
2 | 1 | 3coml 1128 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ ยท (๐ด + ๐ต)) = ((๐ถ ยท ๐ด) + (๐ถ ยท ๐ต))) |
3 | addcl 11134 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) | |
4 | mulcom 11138 | . . 3 โข (((๐ด + ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = (๐ถ ยท (๐ด + ๐ต))) | |
5 | 3, 4 | stoic3 1779 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = (๐ถ ยท (๐ด + ๐ต))) |
6 | mulcom 11138 | . . . 4 โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) = (๐ถ ยท ๐ด)) | |
7 | 6 | 3adant2 1132 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) = (๐ถ ยท ๐ด)) |
8 | mulcom 11138 | . . . 4 โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) = (๐ถ ยท ๐ต)) | |
9 | 8 | 3adant1 1131 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) = (๐ถ ยท ๐ต)) |
10 | 7, 9 | oveq12d 7376 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) = ((๐ถ ยท ๐ด) + (๐ถ ยท ๐ต))) |
11 | 2, 5, 10 | 3eqtr4d 2787 | 1 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง w3a 1088 = wceq 1542 โ wcel 2107 (class class class)co 7358 โcc 11050 + caddc 11055 ยท cmul 11057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-addcl 11112 ax-mulcom 11116 ax-distr 11119 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-iota 6449 df-fv 6505 df-ov 7361 |
This theorem is referenced by: mulid1 11154 adddiri 11169 adddird 11181 muladd11 11326 00id 11331 cnegex2 11338 muladd 11588 ser1const 13965 hashxplem 14334 demoivreALT 16084 dvds2ln 16172 dvds2add 16173 odd2np1lem 16223 cncrng 20821 icccvx 24316 cnlmod 24506 sincosq1eq 25872 abssinper 25880 sineq0 25883 bposlem9 26643 cncvcOLD 29528 ipasslem1 29776 ipasslem11 29785 cdj3i 31386 mblfinlem3 36120 expgrowth 42622 fmtnofac2lem 45767 2zrngALT 46253 |
Copyright terms: Public domain | W3C validator |