Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2622 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
3 | | lincsum.p |
. . 3
⊢ + =
(+g‘𝑀) |
4 | | lmodcmn 18911 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
CMnd) |
6 | 5 | 3ad2ant1 1082 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ CMnd) |
7 | | simpr 477 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
8 | 7 | 3ad2ant1 1082 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
9 | | simpl 473 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
LMod) |
10 | 9 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → 𝑀 ∈ LMod) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
12 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
13 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
14 | 13 | ex 450 |
. . . . . . . 8
⊢ (𝐴:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
17 | 16 | 3ad2ant2 1083 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
18 | 17 | imp 445 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
19 | | elelpwi 4171 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀)) |
20 | 19 | expcom 451 |
. . . . . . 7
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
21 | 20 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
22 | 21 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
23 | 22 | imp 445 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
24 | | lincsum.s |
. . . . 5
⊢ 𝑆 = (Scalar‘𝑀) |
25 | | eqid 2622 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
26 | | lincsum.r |
. . . . 5
⊢ 𝑅 = (Base‘𝑆) |
27 | 1, 24, 25, 26 | lmodvscl 18880 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
28 | 11, 18, 23, 27 | syl3anc 1326 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
29 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵:𝑉⟶𝑅) |
30 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
31 | 30 | ex 450 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
32 | 29, 31 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
33 | 32 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
34 | 33 | 3ad2ant2 1083 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
35 | 34 | imp 445 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
36 | 1, 24, 25, 26 | lmodvscl 18880 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
37 | 11, 35, 23, 36 | syl3anc 1326 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) ∧ 𝑥 ∈ 𝑉) → ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
38 | | eqidd 2623 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
39 | | eqidd 2623 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
40 | | id 22 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀))) |
41 | | simpl 473 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
42 | | simpl 473 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐴 finSupp
(0g‘𝑆)) |
43 | 24, 26 | scmfsupp 42159 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐴 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
44 | 40, 41, 42, 43 | syl3an 1368 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
45 | | simpr 477 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) |
46 | | simpr 477 |
. . . 4
⊢ ((𝐴 finSupp
(0g‘𝑆)
∧ 𝐵 finSupp
(0g‘𝑆))
→ 𝐵 finSupp
(0g‘𝑆)) |
47 | 24, 26 | scmfsupp 42159 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 finSupp (0g‘𝑆)) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
48 | 40, 45, 46, 47 | syl3an 1368 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)) finSupp (0g‘𝑀)) |
49 | 1, 2, 3, 6, 8, 28,
37, 38, 39, 44, 48 | gsummptfsadd 18324 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
50 | 7 | adantr 481 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
51 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 Fn 𝑉) |
52 | 51 | ad2antrl 764 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 Fn 𝑉) |
53 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 Fn 𝑉) |
54 | 53 | ad2antll 765 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 Fn 𝑉) |
55 | 50, 52, 54 | offvalfv 42121 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓 ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
56 | 55 | 3adant3 1081 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘𝑓 ✚ 𝐵) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦)))) |
57 | 24 | lmodfgrp 18872 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Grp) |
58 | | grpmnd 17429 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod → 𝑆 ∈ Mnd) |
60 | 59 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → 𝑆 ∈ Mnd) |
61 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
62 | 61 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝐴:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
63 | 12, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
64 | 63 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 → (𝐴‘𝑦) ∈ 𝑅)) |
65 | 64 | imp 445 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ 𝑅) |
66 | 24 | fveq2i 6194 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘(Scalar‘𝑀)) |
67 | 26, 66 | eqtri 2644 |
. . . . . . . . . 10
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
68 | 65, 67 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
69 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ 𝑅) |
70 | 69, 67 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ ((𝐵:𝑉⟶𝑅 ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
71 | 70 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐵:𝑉⟶𝑅 → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
72 | 29, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
73 | 72 | ad2antll 765 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀)))) |
74 | 73 | imp 445 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) |
75 | 24 | eqcomi 2631 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑀) =
𝑆 |
76 | 75 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
77 | | lincsum.b |
. . . . . . . . . 10
⊢ ✚ =
(+g‘𝑆) |
78 | 76, 77 | mndcl 17301 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ (𝐴‘𝑦) ∈ (Base‘(Scalar‘𝑀)) ∧ (𝐵‘𝑦) ∈ (Base‘(Scalar‘𝑀))) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
79 | 60, 68, 74, 78 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑦 ∈ 𝑉) → ((𝐴‘𝑦) ✚ (𝐵‘𝑦)) ∈ (Base‘(Scalar‘𝑀))) |
80 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) = (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) |
81 | 79, 80 | fmptd 6385 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))) |
82 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
83 | | elmapg 7870 |
. . . . . . . 8
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
84 | 82, 50, 83 | sylancr 695 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))) |
85 | 81, 84 | mpbird 247 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
86 | 85 | 3adant3 1081 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑦 ∈ 𝑉 ↦ ((𝐴‘𝑦) ✚ (𝐵‘𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
87 | 56, 86 | eqeltrd 2701 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝐴 ∘𝑓 ✚ 𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)) |
88 | | lincval 42198 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴 ∘𝑓
✚
𝐵) ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
89 | 10, 87, 8, 88 | syl3anc 1326 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
90 | 51, 53 | anim12i 590 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
91 | 90 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
92 | 91 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉)) |
93 | 50 | anim1i 592 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) |
94 | | fnfvof 6911 |
. . . . . . . . . 10
⊢ (((𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑉)) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
95 | 92, 93, 94 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥) ✚ (𝐵‘𝑥))) |
96 | 77 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ✚ =
(+g‘𝑆)) |
97 | 96 | oveqd 6667 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥) ✚ (𝐵‘𝑥)) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
98 | 95, 97 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥) = ((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))) |
99 | 98 | oveq1d 6665 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
100 | 9 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ LMod) |
101 | 100 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
102 | 15 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ 𝑅)) |
103 | 102 | imp 445 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
104 | 32 | ad2antll 765 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → (𝐵‘𝑥) ∈ 𝑅)) |
105 | 104 | imp 445 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) ∈ 𝑅) |
106 | 21 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
107 | 106 | imp 445 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
108 | | eqid 2622 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
109 | 24 | fveq2i 6194 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘(Scalar‘𝑀)) |
110 | 1, 3, 108, 25, 67, 109 | lmodvsdir 18887 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ ((𝐴‘𝑥) ∈ 𝑅 ∧ (𝐵‘𝑥) ∈ 𝑅 ∧ 𝑥 ∈ (Base‘𝑀))) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
111 | 101, 103,
105, 107, 110 | syl13anc 1328 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥)(+g‘𝑆)(𝐵‘𝑥))( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
112 | 99, 111 | eqtrd 2656 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥) = (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
113 | 112 | mpteq2dva 4744 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
114 | 113 | oveq2d 6666 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
115 | 114 | 3adant3 1081 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴 ∘𝑓 ✚ 𝐵)‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
116 | 89, 115 | eqtrd 2656 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) + ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
117 | | lincsum.x |
. . . 4
⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) |
118 | | lincsum.y |
. . . 4
⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉) |
119 | 117, 118 | oveq12i 6662 |
. . 3
⊢ (𝑋 + 𝑌) = ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) |
120 | 67 | oveq1i 6660 |
. . . . . . . . 9
⊢ (𝑅 ↑𝑚
𝑉) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) |
121 | 120 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
122 | 121 | biimpi 206 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
123 | 122 | ad2antrl 764 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
124 | | lincval 42198 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐴 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
125 | 100, 123,
50, 124 | syl3anc 1326 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
126 | 120 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
127 | 126 | biimpi 206 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
128 | 127 | ad2antll 765 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
129 | | lincval 42198 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐵 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
130 | 100, 128,
50, 129 | syl3anc 1326 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
131 | 125, 130 | oveq12d 6668 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
132 | 131 | 3adant3 1081 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
133 | 119, 132 | syl5eq 2668 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥))) + (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝐵‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
134 | 49, 116, 133 | 3eqtr4rd 2667 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘𝑓 ✚ 𝐵)( linC ‘𝑀)𝑉)) |