Step | Hyp | Ref
| Expression |
1 | | eqid 2826 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2826 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | | lincsum.p |
. . 3
⊢ + =
(+g‘𝑀) |
4 | | lmodcmn 19268 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
5 | 4 | adantr 474 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
CMnd) |
6 | 5 | 3ad2ant1 1169 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ CMnd) |
7 | | simpr 479 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
8 | 7 | 3ad2ant1 1169 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
9 | | simpl 476 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
LMod) |
10 | 9 | 3ad2ant1 1169 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ LMod) |
11 | 10 | adantr 474 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
12 | | elmapi 8145 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
13 | | ffvelrn 6607 |
. . . . . . . . 9
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
14 | 13 | ex 403 |
. . . . . . . 8
⊢ (𝐴:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
16 | 15 | adantr 474 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
17 | 16 | 3ad2ant2 1170 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
18 | 17 | imp 397 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
19 | | elelpwi 4392 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀)) |
20 | 19 | expcom 404 |
. . . . . . 7
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
21 | 20 | adantl 475 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
22 | 21 | 3ad2ant1 1169 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
23 | 22 | imp 397 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
24 | | lincsum.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑀) |
25 | | eqid 2826 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
26 | | lincsum.r |
. . . . 5
⊢ 𝑅 = (Base‘𝑆) |
27 | 1, 24, 25, 26 | lmodvscl 19237 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
28 | 11, 18, 23, 27 | syl3anc 1496 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
29 | | elmapi 8145 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵:𝑉⟶𝑅) |
30 | | ffvelrn 6607 |
. . . . . . . . 9
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
31 | 30 | ex 403 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
32 | 29, 31 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
33 | 32 | adantl 475 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
34 | 33 | 3ad2ant2 1170 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
35 | 34 | imp 397 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
36 | 1, 24, 25, 26 | lmodvscl 19237 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
37 | 11, 35, 23, 36 | syl3anc 1496 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
38 | | eqidd 2827 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
39 | | eqidd 2827 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
40 | | id 22 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
41 | | simpl 476 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
42 | | simpl 476 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐴 finSupp
(0g‘𝑆)) |
43 | 24, 26 | scmfsupp 43007 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
44 | 40, 41, 42, 43 | syl3an 1205 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
45 | | simpr 479 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) |
46 | | simpr 479 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐵 finSupp
(0g‘𝑆)) |
47 | 24, 26 | scmfsupp 43007 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
48 | 40, 45, 46, 47 | syl3an 1205 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 18678 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
50 | 7 | adantr 474 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
51 | | elmapfn 8146 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 Fn 𝑉) |
52 | 51 | ad2antrl 721 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 Fn 𝑉) |
53 | | elmapfn 8146 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 Fn 𝑉) |
54 | 53 | ad2antll 722 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 Fn 𝑉) |
55 | 50, 52, 54 | offvalfv 42969 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓 ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
56 | 55 | 3adant3 1168 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘𝑓 ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
57 | 24 | lmodfgrp 19229 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Grp) |
58 | | grpmnd 17784 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Mnd) |
60 | 59 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → 𝑆 ∈ Mnd) |
61 | | ffvelrn 6607 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
62 | 61 | ex 403 |
. . . . . . . . . . . . 13
⊢ (𝐴:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
63 | 12, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
64 | 63 | ad2antrl 721 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
65 | 64 | imp 397 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
66 | 24 | fveq2i 6437 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
67 | 26, 66 | eqtri 2850 |
. . . . . . . . . 10
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
68 | 65, 67 | syl6eleq 2917 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
69 | | ffvelrn 6607 |
. . . . . . . . . . . . . 14
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ 𝑅) |
70 | 69, 67 | syl6eleq 2917 |
. . . . . . . . . . . . 13
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
71 | 70 | ex 403 |
. . . . . . . . . . . 12
⊢ (𝐵:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
72 | 29, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
73 | 72 | ad2antll 722 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
74 | 73 | imp 397 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
75 | 24 | eqcomi 2835 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑀) =
𝑆 |
76 | 75 | fveq2i 6437 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
77 | | lincsum.b |
. . . . . . . . . 10
⊢ ✚ =
(+g‘𝑆) |
78 | 76, 77 | mndcl 17655 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀)) ∧ (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
79 | 60, 68, 74, 78 | syl3anc 1496 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
80 | 79 | fmpttd 6635 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))) |
81 | | fvex 6447 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
82 | | elmapg 8136 |
. . . . . . . 8
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
83 | 81, 50, 82 | sylancr 583 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
84 | 80, 83 | mpbird 249 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
85 | 84 | 3adant3 1168 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
86 | 56, 85 | eqeltrd 2907 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘𝑓 ✚ 𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)) |
87 | | lincval 43046 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴 ∘𝑓
✚
𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
88 | 10, 86, 8, 87 | syl3anc 1496 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
89 | 51, 53 | anim12i 608 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
90 | 89 | adantl 475 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
91 | 90 | adantr 474 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
92 | 50 | anim1i 610 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) |
93 | | fnfvof 7172 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
94 | 91, 92, 93 | syl2anc 581 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
95 | 77 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ✚ =
(+g‘𝑆)) |
96 | 95 | oveqd 6923 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥) ✚ (𝐵‘𝑥)) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
97 | 94, 96 | eqtrd 2862 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
98 | 97 | oveq1d 6921 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
99 | 9 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ LMod) |
100 | 99 | adantr 474 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
101 | 15 | ad2antrl 721 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
102 | 101 | imp 397 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
103 | 32 | ad2antll 722 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
104 | 103 | imp 397 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
105 | 21 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
106 | 105 | imp 397 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
107 | | eqid 2826 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
108 | 24 | fveq2i 6437 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘(Scalar‘𝑀)) |
109 | 1, 3, 107, 25, 67, 108 | lmodvsdir 19244 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ ((𝐴‘𝑥) ∈ 𝑅 ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀))) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
110 | 100, 102,
104, 106, 109 | syl13anc 1497 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
111 | 98, 110 | eqtrd 2862 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
112 | 111 | mpteq2dva 4968 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
113 | 112 | oveq2d 6922 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
114 | 113 | 3adant3 1168 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
115 | 88, 114 | eqtrd 2862 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
116 | | lincsum.x |
. . . 4
⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) |
117 | | lincsum.y |
. . . 4
⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) |
118 | 116, 117 | oveq12i 6918 |
. . 3
⊢ (𝑋 + 𝑌) = ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) |
119 | 67 | oveq1i 6916 |
. . . . . . . . 9
⊢ (𝑅 ↑𝑚
𝑉) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) |
120 | 119 | eleq2i 2899 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
121 | 120 | biimpi 208 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
122 | 121 | ad2antrl 721 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
123 | | lincval 43046 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐴 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
124 | 99, 122, 50, 123 | syl3anc 1496 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
125 | 119 | eleq2i 2899 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
126 | 125 | biimpi 208 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
127 | 126 | ad2antll 722 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
128 | | lincval 43046 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐵 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
129 | 99, 127, 50, 128 | syl3anc 1496 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
130 | 124, 129 | oveq12d 6924 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
131 | 130 | 3adant3 1168 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
132 | 118, 131 | syl5eq 2874 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
133 | 49, 115, 132 | 3eqtr4rd 2873 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉)) |