| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑀 ∈ LMod) | 
| 2 |  | lincvalsc0.s | . . . . . . . 8
⊢ 𝑆 = (Scalar‘𝑀) | 
| 3 | 2 | eqcomi 2745 | . . . . . . . . 9
⊢
(Scalar‘𝑀) =
𝑆 | 
| 4 | 3 | fveq2i 6908 | . . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) | 
| 5 |  | lincvalsc0.0 | . . . . . . . 8
⊢  0 =
(0g‘𝑆) | 
| 6 | 2, 4, 5 | lmod0cl 20887 | . . . . . . 7
⊢ (𝑀 ∈ LMod → 0 ∈
(Base‘(Scalar‘𝑀))) | 
| 7 | 6 | adantr 480 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 0 ∈
(Base‘(Scalar‘𝑀))) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑉) → 0 ∈
(Base‘(Scalar‘𝑀))) | 
| 9 |  | lincvalsc0.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) | 
| 10 | 8, 9 | fmptd 7133 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀))) | 
| 11 |  | fvexd 6920 | . . . . 5
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) | 
| 12 |  | elmapg 8880 | . . . . 5
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) | 
| 13 | 11, 12 | sylan 580 | . . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) | 
| 14 | 10, 13 | mpbird 257 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉)) | 
| 15 |  | lincvalsc0.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑀) | 
| 16 | 15 | pweqi 4615 | . . . . . 6
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) | 
| 17 | 16 | eleq2i 2832 | . . . . 5
⊢ (𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 18 | 17 | biimpi 216 | . . . 4
⊢ (𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 19 | 18 | adantl 481 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) | 
| 20 |  | lincval 48331 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) | 
| 21 | 1, 14, 19, 20 | syl3anc 1372 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) | 
| 22 |  | simpr 484 | . . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) | 
| 23 | 5 | fvexi 6919 | . . . . . . 7
⊢  0 ∈
V | 
| 24 |  | eqidd 2737 | . . . . . . . 8
⊢ (𝑥 = 𝑣 → 0 = 0 ) | 
| 25 | 24, 9 | fvmptg 7013 | . . . . . . 7
⊢ ((𝑣 ∈ 𝑉 ∧ 0 ∈ V) → (𝐹‘𝑣) = 0 ) | 
| 26 | 22, 23, 25 | sylancl 586 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) = 0 ) | 
| 27 | 26 | oveq1d 7447 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ( 0 (
·𝑠 ‘𝑀)𝑣)) | 
| 28 | 1 | adantr 480 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) | 
| 29 |  | elelpwi 4609 | . . . . . . . . 9
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑣 ∈ 𝐵) | 
| 30 | 29 | expcom 413 | . . . . . . . 8
⊢ (𝑉 ∈ 𝒫 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) | 
| 31 | 30 | adantl 481 | . . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) | 
| 32 | 31 | imp 406 | . . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) | 
| 33 |  | eqid 2736 | . . . . . . 7
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) | 
| 34 |  | lincvalsc0.z | . . . . . . 7
⊢ 𝑍 = (0g‘𝑀) | 
| 35 | 15, 2, 33, 5, 34 | lmod0vs 20894 | . . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) | 
| 36 | 28, 32, 35 | syl2anc 584 | . . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) | 
| 37 | 27, 36 | eqtrd 2776 | . . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = 𝑍) | 
| 38 | 37 | mpteq2dva 5241 | . . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ 𝑍)) | 
| 39 | 38 | oveq2d 7448 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍))) | 
| 40 |  | lmodgrp 20866 | . . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) | 
| 41 | 40 | grpmndd 18965 | . . 3
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) | 
| 42 | 34 | gsumz 18850 | . . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) | 
| 43 | 41, 42 | sylan 580 | . 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) | 
| 44 | 21, 39, 43 | 3eqtrd 2780 | 1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) |