Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2738 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | | lincsum.p |
. . 3
⊢ + =
(+g‘𝑀) |
4 | | lmodcmn 19972 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
5 | 4 | adantr 484 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
CMnd) |
6 | 5 | 3ad2ant1 1135 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ CMnd) |
7 | | simpr 488 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
8 | 7 | 3ad2ant1 1135 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
9 | | simpl 486 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
LMod) |
10 | 9 | 3ad2ant1 1135 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ LMod) |
11 | 10 | adantr 484 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
12 | | elmapi 8551 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴:𝑉⟶𝑅) |
13 | | ffvelrn 6921 |
. . . . . . . . 9
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
14 | 13 | ex 416 |
. . . . . . . 8
⊢ (𝐴:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
16 | 15 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
17 | 16 | 3ad2ant2 1136 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
18 | 17 | imp 410 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
19 | | elelpwi 4540 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀)) |
20 | 19 | expcom 417 |
. . . . . . 7
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
21 | 20 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
22 | 21 | 3ad2ant1 1135 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
23 | 22 | imp 410 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
24 | | lincsum.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑀) |
25 | | eqid 2738 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
26 | | lincsum.r |
. . . . 5
⊢ 𝑅 = (Base‘𝑆) |
27 | 1, 24, 25, 26 | lmodvscl 19941 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
28 | 11, 18, 23, 27 | syl3anc 1373 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
29 | | elmapi 8551 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵:𝑉⟶𝑅) |
30 | | ffvelrn 6921 |
. . . . . . . . 9
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
31 | 30 | ex 416 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
32 | 29, 31 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
34 | 33 | 3ad2ant2 1136 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
35 | 34 | imp 410 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
36 | 1, 24, 25, 26 | lmodvscl 19941 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
37 | 11, 35, 23, 36 | syl3anc 1373 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
38 | | eqidd 2739 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
39 | | eqidd 2739 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
40 | | id 22 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
41 | | simpl 486 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → 𝐴 ∈ (𝑅 ↑m 𝑉)) |
42 | | simpl 486 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐴 finSupp
(0g‘𝑆)) |
43 | 24, 26 | scmfsupp 45416 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
44 | 40, 41, 42, 43 | syl3an 1162 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
45 | | simpr 488 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → 𝐵 ∈ (𝑅 ↑m 𝑉)) |
46 | | simpr 488 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐵 finSupp
(0g‘𝑆)) |
47 | 24, 26 | scmfsupp 45416 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
48 | 40, 45, 46, 47 | syl3an 1162 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 19334 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
50 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
51 | | elmapfn 8567 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 Fn 𝑉) |
52 | 51 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 Fn 𝑉) |
53 | | elmapfn 8567 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 Fn 𝑉) |
54 | 53 | ad2antll 729 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 Fn 𝑉) |
55 | 50, 52, 54 | offvalfv 45380 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
56 | 55 | 3adant3 1134 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘f ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
57 | 24 | lmodfgrp 19933 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Grp) |
58 | 57 | grpmndd 18402 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Mnd) |
59 | 58 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → 𝑆 ∈ Mnd) |
60 | | ffvelrn 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
61 | 60 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝐴:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
62 | 12, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
63 | 62 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
64 | 63 | imp 410 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
65 | 24 | fveq2i 6739 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
66 | 26, 65 | eqtri 2766 |
. . . . . . . . . 10
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
67 | 64, 66 | eleqtrdi 2849 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
68 | | ffvelrn 6921 |
. . . . . . . . . . . . . 14
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ 𝑅) |
69 | 68, 66 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
70 | 69 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝐵:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
72 | 71 | ad2antll 729 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
73 | 72 | imp 410 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
74 | 24 | eqcomi 2747 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑀) =
𝑆 |
75 | 74 | fveq2i 6739 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
76 | | lincsum.b |
. . . . . . . . . 10
⊢ ✚ =
(+g‘𝑆) |
77 | 75, 76 | mndcl 18206 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀)) ∧ (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
78 | 59, 67, 73, 77 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑦 ∈ 𝑉) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
79 | 78 | fmpttd 6951 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))) |
80 | | fvex 6749 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
81 | | elmapg 8542 |
. . . . . . . 8
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
82 | 80, 50, 81 | sylancr 590 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
83 | 79, 82 | mpbird 260 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
84 | 83 | 3adant3 1134 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
85 | 56, 84 | eqeltrd 2839 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘f ✚ 𝐵) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
86 | | lincval 45452 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴 ∘f ✚ 𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
87 | 10, 85, 8, 86 | syl3anc 1373 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
88 | 51, 53 | anim12i 616 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
89 | 88 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
90 | 89 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
91 | 50 | anim1i 618 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) |
92 | | fnfvof 7504 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
93 | 90, 91, 92 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
94 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ✚ =
(+g‘𝑆)) |
95 | 94 | oveqd 7249 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥) ✚ (𝐵‘𝑥)) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
96 | 93, 95 | eqtrd 2778 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘f ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
97 | 96 | oveq1d 7247 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
98 | 9 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑀 ∈ LMod) |
99 | 98 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
100 | 15 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
101 | 100 | imp 410 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
102 | 32 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
103 | 102 | imp 410 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
104 | 21 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
105 | 104 | imp 410 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
106 | | eqid 2738 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
107 | 24 | fveq2i 6739 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘(Scalar‘𝑀)) |
108 | 1, 3, 106, 25, 66, 107 | lmodvsdir 19948 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ ((𝐴‘𝑥) ∈ 𝑅 ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀))) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
109 | 99, 101, 103, 105, 108 | syl13anc 1374 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
110 | 97, 109 | eqtrd 2778 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
111 | 110 | mpteq2dva 5165 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
112 | 111 | oveq2d 7248 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
113 | 112 | 3adant3 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘f ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
114 | 87, 113 | eqtrd 2778 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
115 | | lincsum.x |
. . . 4
⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) |
116 | | lincsum.y |
. . . 4
⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) |
117 | 115, 116 | oveq12i 7244 |
. . 3
⊢ (𝑋 + 𝑌) = ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) |
118 | 66 | oveq1i 7242 |
. . . . . . . . 9
⊢ (𝑅 ↑m 𝑉) =
((Base‘(Scalar‘𝑀)) ↑m 𝑉) |
119 | 118 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
120 | 119 | biimpi 219 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
121 | 120 | ad2antrl 728 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
122 | | lincval 45452 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐴 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
123 | 98, 121, 50, 122 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
124 | 118 | eleq2i 2830 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) ↔ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
125 | 124 | biimpi 219 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
126 | 125 | ad2antll 729 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
127 | | lincval 45452 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐵 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
128 | 98, 126, 50, 127 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
129 | 123, 128 | oveq12d 7250 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
130 | 129 | 3adant3 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
131 | 117, 130 | syl5eq 2791 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
132 | 49, 114, 131 | 3eqtr4rd 2789 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉)) |