![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmodvsdi | Structured version Visualization version GIF version |
Description: Distributive law for scalar product (left-distributivity). (ax-hvdistr1 30817 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Ref | Expression |
---|---|
lmodvsdi.v | ⊢ 𝑉 = (Base‘𝑊) |
lmodvsdi.a | ⊢ + = (+g‘𝑊) |
lmodvsdi.f | ⊢ 𝐹 = (Scalar‘𝑊) |
lmodvsdi.s | ⊢ · = ( ·𝑠 ‘𝑊) |
lmodvsdi.k | ⊢ 𝐾 = (Base‘𝐹) |
Ref | Expression |
---|---|
lmodvsdi | ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodvsdi.v | . . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊) | |
2 | lmodvsdi.a | . . . . . . . . 9 ⊢ + = (+g‘𝑊) | |
3 | lmodvsdi.s | . . . . . . . . 9 ⊢ · = ( ·𝑠 ‘𝑊) | |
4 | lmodvsdi.f | . . . . . . . . 9 ⊢ 𝐹 = (Scalar‘𝑊) | |
5 | lmodvsdi.k | . . . . . . . . 9 ⊢ 𝐾 = (Base‘𝐹) | |
6 | eqid 2728 | . . . . . . . . 9 ⊢ (+g‘𝐹) = (+g‘𝐹) | |
7 | eqid 2728 | . . . . . . . . 9 ⊢ (.r‘𝐹) = (.r‘𝐹) | |
8 | eqid 2728 | . . . . . . . . 9 ⊢ (1r‘𝐹) = (1r‘𝐹) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | lmodlema 20747 | . . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋) + (𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋))) |
10 | 9 | simpld 494 | . . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋) + (𝑅 · 𝑋)))) |
11 | 10 | simp2d 1141 | . . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) |
12 | 11 | 3expia 1119 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) → ((𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))) |
13 | 12 | anabsan2 673 | . . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → ((𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))) |
14 | 13 | exp4b 430 | . . 3 ⊢ (𝑊 ∈ LMod → (𝑅 ∈ 𝐾 → (𝑌 ∈ 𝑉 → (𝑋 ∈ 𝑉 → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))))) |
15 | 14 | com34 91 | . 2 ⊢ (𝑊 ∈ LMod → (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑌 ∈ 𝑉 → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))))) |
16 | 15 | 3imp2 1347 | 1 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ‘cfv 6548 (class class class)co 7420 Basecbs 17179 +gcplusg 17232 .rcmulr 17233 Scalarcsca 17235 ·𝑠 cvsca 17236 1rcur 20120 LModclmod 20742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rab 3430 df-v 3473 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-lmod 20744 |
This theorem is referenced by: lmodcom 20790 lmodsubdi 20801 lmodvsghm 20805 islss3 20842 prdslmodd 20852 lmodvsinv2 20921 lmhmplusg 20928 lsmcl 20967 pj1lmhm 20984 lspfixed 21015 lspsolvlem 21029 clmvsdi 25018 cvsi 25056 eqgvscpbl 33062 imaslmod 33065 lshpkrlem4 38585 baerlem5alem1 41181 baerlem5blem1 41182 hdmap14lem8 41348 mendlmod 42617 lmodvsmdi 47446 |
Copyright terms: Public domain | W3C validator |