Step | Hyp | Ref
| Expression |
1 | | eqid 2821 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2821 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | | lincsum.p |
. . 3
⊢ + =
(+g‘𝑀) |
4 | | lmodcmn 19682 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
5 | 4 | adantr 483 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
CMnd) |
6 | 5 | 3ad2ant1 1129 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ CMnd) |
7 | | simpr 487 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
8 | 7 | 3ad2ant1 1129 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
9 | | simpl 485 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
LMod) |
10 | 9 | 3ad2ant1 1129 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ LMod) |
11 | 10 | adantr 483 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
12 | | elmapi 8428 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴:𝑉⟶𝑅) |
13 | | ffvelrn 6849 |
. . . . . . . . 9
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
14 | 13 | ex 415 |
. . . . . . . 8
⊢ (𝐴:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
16 | 15 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
17 | 16 | 3ad2ant2 1130 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
18 | 17 | imp 409 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
19 | | elelpwi 4551 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀)) |
20 | 19 | expcom 416 |
. . . . . . 7
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
21 | 20 | adantl 484 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
22 | 21 | 3ad2ant1 1129 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
23 | 22 | imp 409 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
24 | | lincsum.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑀) |
25 | | eqid 2821 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
26 | | lincsum.r |
. . . . 5
⊢ 𝑅 = (Base‘𝑆) |
27 | 1, 24, 25, 26 | lmodvscl 19651 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
28 | 11, 18, 23, 27 | syl3anc 1367 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
29 | | elmapi 8428 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵:𝑉⟶𝑅) |
30 | | ffvelrn 6849 |
. . . . . . . . 9
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
31 | 30 | ex 415 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
32 | 29, 31 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
33 | 32 | adantl 484 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
34 | 33 | 3ad2ant2 1130 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
35 | 34 | imp 409 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
36 | 1, 24, 25, 26 | lmodvscl 19651 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
37 | 11, 35, 23, 36 | syl3anc 1367 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
38 | | eqidd 2822 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
39 | | eqidd 2822 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
40 | | id 22 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
41 | | simpl 485 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → 𝐴 ∈ (𝑅 ↑m 𝑉)) |
42 | | simpl 485 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐴 finSupp
(0g‘𝑆)) |
43 | 24, 26 | scmfsupp 44446 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
44 | 40, 41, 42, 43 | syl3an 1156 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
45 | | simpr 487 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → 𝐵 ∈ (𝑅 ↑m 𝑉)) |
46 | | simpr 487 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐵 finSupp
(0g‘𝑆)) |
47 | 24, 26 | scmfsupp 44446 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
48 | 40, 45, 46, 47 | syl3an 1156 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 19044 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
50 | 7 | adantr 483 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
51 | | elmapfn 8429 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 Fn 𝑉) |
52 | 51 | ad2antrl 726 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 Fn 𝑉) |
53 | | elmapfn 8429 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 Fn 𝑉) |
54 | 53 | ad2antll 727 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 Fn 𝑉) |
55 | 50, 52, 54 | offvalfv 44411 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
56 | 55 | 3adant3 1128 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘f ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
57 | 24 | lmodfgrp 19643 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Grp) |
58 | | grpmnd 18110 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Mnd) |
60 | 59 | ad3antrrr 728 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → 𝑆 ∈ Mnd) |
61 | | ffvelrn 6849 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
62 | 61 | ex 415 |
. . . . . . . . . . . . 13
⊢ (𝐴:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
63 | 12, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
64 | 63 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
65 | 64 | imp 409 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
66 | 24 | fveq2i 6673 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
67 | 26, 66 | eqtri 2844 |
. . . . . . . . . 10
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
68 | 65, 67 | eleqtrdi 2923 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
69 | | ffvelrn 6849 |
. . . . . . . . . . . . . 14
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ 𝑅) |
70 | 69, 67 | eleqtrdi 2923 |
. . . . . . . . . . . . 13
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
71 | 70 | ex 415 |
. . . . . . . . . . . 12
⊢ (𝐵:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
72 | 29, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
73 | 72 | ad2antll 727 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
74 | 73 | imp 409 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
75 | 24 | eqcomi 2830 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑀) =
𝑆 |
76 | 75 | fveq2i 6673 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
77 | | lincsum.b |
. . . . . . . . . 10
⊢ ✚ =
(+g‘𝑆) |
78 | 76, 77 | mndcl 17919 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀)) ∧ (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
79 | 60, 68, 74, 78 | syl3anc 1367 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
80 | 79 | fmpttd 6879 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))) |
81 | | fvex 6683 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
82 | | elmapg 8419 |
. . . . . . . 8
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
83 | 81, 50, 82 | sylancr 589 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
84 | 80, 83 | mpbird 259 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
85 | 84 | 3adant3 1128 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
86 | 56, 85 | eqeltrd 2913 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘f ✚ 𝐵) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
87 | | lincval 44484 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴 ∘f ✚ 𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
88 | 10, 86, 8, 87 | syl3anc 1367 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
89 | 51, 53 | anim12i 614 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
90 | 89 | adantl 484 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
91 | 90 | adantr 483 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
92 | 50 | anim1i 616 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) |
93 | | fnfvof 7423 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
94 | 91, 92, 93 | syl2anc 586 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
95 | 77 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ✚ =
(+g‘𝑆)) |
96 | 95 | oveqd 7173 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥) ✚ (𝐵‘𝑥)) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
97 | 94, 96 | eqtrd 2856 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
98 | 97 | oveq1d 7171 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
99 | 9 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑀 ∈ LMod) |
100 | 99 | adantr 483 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
101 | 15 | ad2antrl 726 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
102 | 101 | imp 409 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
103 | 32 | ad2antll 727 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
104 | 103 | imp 409 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
105 | 21 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
106 | 105 | imp 409 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
107 | | eqid 2821 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
108 | 24 | fveq2i 6673 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘(Scalar‘𝑀)) |
109 | 1, 3, 107, 25, 67, 108 | lmodvsdir 19658 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ ((𝐴‘𝑥) ∈ 𝑅 ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀))) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
110 | 100, 102,
104, 106, 109 | syl13anc 1368 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
111 | 98, 110 | eqtrd 2856 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
112 | 111 | mpteq2dva 5161 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
113 | 112 | oveq2d 7172 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
114 | 113 | 3adant3 1128 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
115 | 88, 114 | eqtrd 2856 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
116 | | lincsum.x |
. . . 4
⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) |
117 | | lincsum.y |
. . . 4
⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) |
118 | 116, 117 | oveq12i 7168 |
. . 3
⊢ (𝑋 + 𝑌) = ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) |
119 | 67 | oveq1i 7166 |
. . . . . . . . 9
⊢ (𝑅 ↑m 𝑉) =
((Base‘(Scalar‘𝑀)) ↑m 𝑉) |
120 | 119 | eleq2i 2904 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
121 | 120 | biimpi 218 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
122 | 121 | ad2antrl 726 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
123 | | lincval 44484 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐴 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
124 | 99, 122, 50, 123 | syl3anc 1367 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
125 | 119 | eleq2i 2904 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) ↔ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
126 | 125 | biimpi 218 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
127 | 126 | ad2antll 727 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
128 | | lincval 44484 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐵 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
129 | 99, 127, 50, 128 | syl3anc 1367 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
130 | 124, 129 | oveq12d 7174 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
131 | 130 | 3adant3 1128 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
132 | 118, 131 | syl5eq 2868 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
133 | 49, 115, 132 | 3eqtr4rd 2867 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉)) |