| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1137 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑀 ∈ LMod) | 
| 2 |  | lincfsuppcl.s | . . . . . . . . 9
⊢ 𝑆 = (Base‘𝑅) | 
| 3 |  | lincfsuppcl.r | . . . . . . . . . 10
⊢ 𝑅 = (Scalar‘𝑀) | 
| 4 | 3 | fveq2i 6909 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) | 
| 5 | 2, 4 | eqtri 2765 | . . . . . . . 8
⊢ 𝑆 =
(Base‘(Scalar‘𝑀)) | 
| 6 | 5 | oveq1i 7441 | . . . . . . 7
⊢ (𝑆 ↑m 𝑉) =
((Base‘(Scalar‘𝑀)) ↑m 𝑉) | 
| 7 | 6 | eleq2i 2833 | . . . . . 6
⊢ (𝐹 ∈ (𝑆 ↑m 𝑉) ↔ 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) | 
| 8 | 7 | biimpi 216 | . . . . 5
⊢ (𝐹 ∈ (𝑆 ↑m 𝑉) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) | 
| 10 | 9 | 3ad2ant3 1136 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉)) | 
| 11 |  | elpwg 4603 | . . . . . 6
⊢ (𝑉 ∈ 𝑊 → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) | 
| 12 |  | lincfsuppcl.b | . . . . . . . . 9
⊢ 𝐵 = (Base‘𝑀) | 
| 13 | 12 | a1i 11 | . . . . . . . 8
⊢ (𝑉 ∈ 𝑊 → 𝐵 = (Base‘𝑀)) | 
| 14 | 13 | eqcomd 2743 | . . . . . . 7
⊢ (𝑉 ∈ 𝑊 → (Base‘𝑀) = 𝐵) | 
| 15 | 14 | sseq2d 4016 | . . . . . 6
⊢ (𝑉 ∈ 𝑊 → (𝑉 ⊆ (Base‘𝑀) ↔ 𝑉 ⊆ 𝐵)) | 
| 16 | 11, 15 | bitr2d 280 | . . . . 5
⊢ (𝑉 ∈ 𝑊 → (𝑉 ⊆ 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀))) | 
| 17 | 16 | biimpa 476 | . . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 18 | 17 | 3ad2ant2 1135 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑉 ∈ 𝒫
(Base‘𝑀)) | 
| 19 |  | lincval 48326 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) | 
| 20 | 1, 10, 18, 19 | syl3anc 1373 | . 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) | 
| 21 |  | eqid 2737 | . . 3
⊢
(0g‘𝑀) = (0g‘𝑀) | 
| 22 |  | lmodcmn 20908 | . . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) | 
| 23 | 22 | 3ad2ant1 1134 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑀 ∈ CMnd) | 
| 24 |  | simpl 482 | . . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) → 𝑉 ∈ 𝑊) | 
| 25 | 24 | 3ad2ant2 1135 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝑉 ∈ 𝑊) | 
| 26 | 1 | adantr 480 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) | 
| 27 |  | elmapi 8889 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 ↑m 𝑉) → 𝐹:𝑉⟶𝑆) | 
| 28 |  | ffvelcdm 7101 | . . . . . . . . . 10
⊢ ((𝐹:𝑉⟶𝑆 ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝑆) | 
| 29 | 28 | ex 412 | . . . . . . . . 9
⊢ (𝐹:𝑉⟶𝑆 → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝑆)) | 
| 30 | 27, 29 | syl 17 | . . . . . . . 8
⊢ (𝐹 ∈ (𝑆 ↑m 𝑉) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝑆)) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢ ((𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 ) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝑆)) | 
| 32 | 31 | 3ad2ant3 1136 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝑆)) | 
| 33 | 32 | imp 406 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝑆) | 
| 34 |  | ssel 3977 | . . . . . . . 8
⊢ (𝑉 ⊆ 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) | 
| 35 | 34 | adantl 481 | . . . . . . 7
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) | 
| 36 | 35 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) | 
| 37 | 36 | imp 406 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) | 
| 38 |  | eqid 2737 | . . . . . 6
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) | 
| 39 | 12, 3, 38, 2 | lmodvscl 20876 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝐹‘𝑣) ∈ 𝑆 ∧ 𝑣 ∈ 𝐵) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) | 
| 40 | 26, 33, 37, 39 | syl3anc 1373 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) | 
| 41 | 40 | fmpttd 7135 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)):𝑉⟶𝐵) | 
| 42 |  | simpl 482 | . . . . 5
⊢ ((𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 ) → 𝐹 ∈ (𝑆 ↑m 𝑉)) | 
| 43 | 42 | 3ad2ant3 1136 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝐹 ∈ (𝑆 ↑m 𝑉)) | 
| 44 |  | simp3r 1203 | . . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝐹 finSupp 0 ) | 
| 45 |  | lincfsuppcl.0 | . . . . 5
⊢  0 =
(0g‘𝑅) | 
| 46 | 44, 45 | breqtrdi 5184 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → 𝐹 finSupp
(0g‘𝑅)) | 
| 47 | 3, 2 | scmfsupp 48291 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) | 
| 48 | 1, 18, 43, 46, 47 | syl211anc 1378 | . . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) | 
| 49 | 12, 21, 23, 25, 41, 48 | gsumcl 19933 | . 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝑀 Σg
(𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝐵) | 
| 50 | 20, 49 | eqeltrd 2841 | 1
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ 𝑊 ∧ 𝑉 ⊆ 𝐵) ∧ (𝐹 ∈ (𝑆 ↑m 𝑉) ∧ 𝐹 finSupp 0 )) → (𝐹( linC ‘𝑀)𝑉) ∈ 𝐵) |