| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 2 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
| 3 | | lincscm.r |
. . 3
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
| 4 | | eqid 2737 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 5 | | eqid 2737 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 6 | | lincscm.s |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑀) |
| 7 | | simp1l 1198 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑀 ∈ LMod) |
| 8 | | simpr 484 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
| 9 | 8 | 3ad2ant1 1134 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
| 10 | | simpr 484 |
. . . 4
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) → 𝑆 ∈ 𝑅) |
| 11 | 10 | 3ad2ant2 1135 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑆 ∈ 𝑅) |
| 12 | 7 | adantr 480 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) |
| 13 | | elmapi 8889 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴:𝑉⟶𝑅) |
| 14 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑣 ∈ 𝑉) → (𝐴‘𝑣) ∈ 𝑅) |
| 15 | 14 | ex 412 |
. . . . . . . 8
⊢ (𝐴:𝑉⟶𝑅 → (𝑣 ∈ 𝑉 → (𝐴‘𝑣) ∈ 𝑅)) |
| 16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑣 ∈ 𝑉 → (𝐴‘𝑣) ∈ 𝑅)) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) → (𝑣 ∈ 𝑉 → (𝐴‘𝑣) ∈ 𝑅)) |
| 18 | 17 | 3ad2ant2 1135 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 → (𝐴‘𝑣) ∈ 𝑅)) |
| 19 | 18 | imp 406 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → (𝐴‘𝑣) ∈ 𝑅) |
| 20 | | elelpwi 4610 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑣 ∈ (Base‘𝑀)) |
| 21 | 20 | expcom 413 |
. . . . . . 7
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑣 ∈ 𝑉 → 𝑣 ∈ (Base‘𝑀))) |
| 22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝑣 ∈ 𝑉 → 𝑣 ∈ (Base‘𝑀))) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 → 𝑣 ∈ (Base‘𝑀))) |
| 24 | 23 | imp 406 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Base‘𝑀)) |
| 25 | | eqid 2737 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
| 26 | 1, 2, 25, 3 | lmodvscl 20876 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝐴‘𝑣) ∈ 𝑅 ∧ 𝑣 ∈ (Base‘𝑀)) → ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ (Base‘𝑀)) |
| 27 | 12, 19, 24, 26 | syl3anc 1373 |
. . 3
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ (Base‘𝑀)) |
| 28 | 2, 3 | scmfsupp 48291 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
| 29 | 28 | 3adant2r 1180 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
| 30 | 1, 2, 3, 4, 5, 6, 7, 9, 11, 27, 29 | gsumvsmul 20924 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)))) = (𝑆 ∙ (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))))) |
| 31 | 2 | lmodring 20866 |
. . . . . . . . . 10
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Ring) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(Scalar‘𝑀) ∈
Ring) |
| 33 | 32 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (Scalar‘𝑀) ∈ Ring) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (Scalar‘𝑀) ∈ Ring) |
| 35 | 3 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑅 ↔ 𝑆 ∈ (Base‘(Scalar‘𝑀))) |
| 36 | 35 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑆 ∈ 𝑅 → 𝑆 ∈ (Base‘(Scalar‘𝑀))) |
| 37 | 36 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) → 𝑆 ∈ (Base‘(Scalar‘𝑀))) |
| 38 | 37 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑆 ∈ (Base‘(Scalar‘𝑀))) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑥 ∈ 𝑉) → 𝑆 ∈ (Base‘(Scalar‘𝑀))) |
| 40 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ 𝑅) |
| 41 | 40, 3 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀))) |
| 42 | 41 | ex 412 |
. . . . . . . . . . 11
⊢ (𝐴:𝑉⟶𝑅 → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀)))) |
| 43 | 13, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀)))) |
| 44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀)))) |
| 45 | 44 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑥 ∈ 𝑉 → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀)))) |
| 46 | 45 | imp 406 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀))) |
| 47 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
| 48 | | lincscm.t |
. . . . . . . 8
⊢ · =
(.r‘(Scalar‘𝑀)) |
| 49 | 47, 48 | ringcl 20247 |
. . . . . . 7
⊢
(((Scalar‘𝑀)
∈ Ring ∧ 𝑆 ∈
(Base‘(Scalar‘𝑀)) ∧ (𝐴‘𝑥) ∈ (Base‘(Scalar‘𝑀))) → (𝑆 · (𝐴‘𝑥)) ∈ (Base‘(Scalar‘𝑀))) |
| 50 | 34, 39, 46, 49 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝑆 · (𝐴‘𝑥)) ∈ (Base‘(Scalar‘𝑀))) |
| 51 | | lincscm.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ (𝑆 · (𝐴‘𝑥))) |
| 52 | 50, 51 | fmptd 7134 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀))) |
| 53 | | fvex 6919 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
| 54 | | elmapg 8879 |
. . . . . 6
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
| 55 | 53, 9, 54 | sylancr 587 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
| 56 | 52, 55 | mpbird 257 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 57 | | lincval 48326 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 58 | 7, 56, 9, 57 | syl3anc 1373 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 59 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
| 60 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑆 · (𝐴‘𝑣)) ∈ V |
| 61 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → (𝐴‘𝑥) = (𝐴‘𝑣)) |
| 62 | 61 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑆 · (𝐴‘𝑥)) = (𝑆 · (𝐴‘𝑣))) |
| 63 | 62, 51 | fvmptg 7014 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝑉 ∧ (𝑆 · (𝐴‘𝑣)) ∈ V) → (𝐹‘𝑣) = (𝑆 · (𝐴‘𝑣))) |
| 64 | 59, 60, 63 | sylancl 586 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) = (𝑆 · (𝐴‘𝑣))) |
| 65 | 64 | oveq1d 7446 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝑆 · (𝐴‘𝑣))( ·𝑠
‘𝑀)𝑣)) |
| 66 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → 𝑆 ∈ 𝑅) |
| 67 | 1, 2, 25, 3, 48 | lmodvsass 20885 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑆 ∈ 𝑅 ∧ (𝐴‘𝑣) ∈ 𝑅 ∧ 𝑣 ∈ (Base‘𝑀))) → ((𝑆 · (𝐴‘𝑣))( ·𝑠
‘𝑀)𝑣) = (𝑆( ·𝑠
‘𝑀)((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
| 68 | 12, 66, 19, 24, 67 | syl13anc 1374 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → ((𝑆 · (𝐴‘𝑣))( ·𝑠
‘𝑀)𝑣) = (𝑆( ·𝑠
‘𝑀)((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
| 69 | 6 | eqcomi 2746 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑀) = ∙ |
| 70 | 69 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → (
·𝑠 ‘𝑀) = ∙ ) |
| 71 | 70 | oveqd 7448 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → (𝑆( ·𝑠
‘𝑀)((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
| 72 | 68, 71 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → ((𝑆 · (𝐴‘𝑣))( ·𝑠
‘𝑀)𝑣) = (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
| 73 | 65, 72 | eqtrd 2777 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
| 74 | 73 | mpteq2dva 5242 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 75 | 74 | oveq2d 7447 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))))) |
| 76 | 58, 75 | eqtrd 2777 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ (𝑆 ∙ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))))) |
| 77 | | lincscm.x |
. . . . 5
⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉) |
| 78 | 77 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑋 = (𝐴( linC ‘𝑀)𝑉)) |
| 79 | 3 | oveq1i 7441 |
. . . . . . . . 9
⊢ (𝑅 ↑m 𝑉) =
((Base‘(Scalar‘𝑀)) ↑m 𝑉) |
| 80 | 79 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 81 | 80 | biimpi 216 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 82 | 81 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 83 | 82 | 3ad2ant2 1135 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) |
| 84 | | lincval 48326 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝐴 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 85 | 7, 83, 9, 84 | syl3anc 1373 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 86 | 78, 85 | eqtrd 2777 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
| 87 | 86 | oveq2d 7447 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑆 ∙ 𝑋) = (𝑆 ∙ (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))))) |
| 88 | 30, 76, 87 | 3eqtr4rd 2788 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝑆 ∈ 𝑅) ∧ 𝐴 finSupp
(0g‘(Scalar‘𝑀))) → (𝑆 ∙ 𝑋) = (𝐹( linC ‘𝑀)𝑉)) |