Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑀 ∈ LMod) |
2 | | lincvalsc0.s |
. . . . . . . 8
⊢ 𝑆 = (Scalar‘𝑀) |
3 | 2 | eqcomi 2631 |
. . . . . . . . 9
⊢
(Scalar‘𝑀) =
𝑆 |
4 | 3 | fveq2i 6194 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑀)) = (Base‘𝑆) |
5 | | lincvalsc0.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑆) |
6 | 2, 4, 5 | lmod0cl 18889 |
. . . . . . 7
⊢ (𝑀 ∈ LMod → 0 ∈
(Base‘(Scalar‘𝑀))) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 0 ∈
(Base‘(Scalar‘𝑀))) |
8 | 7 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝑉) → 0 ∈
(Base‘(Scalar‘𝑀))) |
9 | | lincvalsc0.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ 0 ) |
10 | 8, 9 | fmptd 6385 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹:𝑉⟶(Base‘(Scalar‘𝑀))) |
11 | | fvexd 6203 |
. . . . 5
⊢ (𝑀 ∈ LMod →
(Base‘(Scalar‘𝑀)) ∈ V) |
12 | | elmapg 7870 |
. . . . 5
⊢
(((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
13 | 11, 12 | sylan 488 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ↔ 𝐹:𝑉⟶(Base‘(Scalar‘𝑀)))) |
14 | 10, 13 | mpbird 247 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
15 | | lincvalsc0.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
16 | 15 | pweqi 4162 |
. . . . . 6
⊢ 𝒫
𝐵 = 𝒫
(Base‘𝑀) |
17 | 16 | eleq2i 2693 |
. . . . 5
⊢ (𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 (Base‘𝑀)) |
18 | 17 | biimpi 206 |
. . . 4
⊢ (𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
19 | 18 | adantl 482 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
20 | | lincval 42198 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
21 | 1, 14, 19, 20 | syl3anc 1326 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
22 | | simpr 477 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
23 | | fvex 6201 |
. . . . . . . 8
⊢
(0g‘𝑆) ∈ V |
24 | 5, 23 | eqeltri 2697 |
. . . . . . 7
⊢ 0 ∈
V |
25 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → 0 = 0 ) |
26 | 25, 9 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑉 ∧ 0 ∈ V) → (𝐹‘𝑣) = 0 ) |
27 | 22, 24, 26 | sylancl 694 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) = 0 ) |
28 | 27 | oveq1d 6665 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = ( 0 (
·𝑠 ‘𝑀)𝑣)) |
29 | 1 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) |
30 | | elelpwi 4171 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵) → 𝑣 ∈ 𝐵) |
31 | 30 | expcom 451 |
. . . . . . . 8
⊢ (𝑉 ∈ 𝒫 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
32 | 31 | adantl 482 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
33 | 32 | imp 445 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) |
34 | | eqid 2622 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
35 | | lincvalsc0.z |
. . . . . . 7
⊢ 𝑍 = (0g‘𝑀) |
36 | 15, 2, 34, 5, 35 | lmod0vs 18896 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
37 | 29, 33, 36 | syl2anc 693 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ( 0 (
·𝑠 ‘𝑀)𝑣) = 𝑍) |
38 | 28, 37 | eqtrd 2656 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) = 𝑍) |
39 | 38 | mpteq2dva 4744 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ 𝑍)) |
40 | 39 | oveq2d 6666 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍))) |
41 | | lmodgrp 18870 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) |
42 | | grpmnd 17429 |
. . . 4
⊢ (𝑀 ∈ Grp → 𝑀 ∈ Mnd) |
43 | 41, 42 | syl 17 |
. . 3
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) |
44 | 35 | gsumz 17374 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) |
45 | 43, 44 | sylan 488 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ 𝑍)) = 𝑍) |
46 | 21, 40, 45 | 3eqtrd 2660 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵) → (𝐹( linC ‘𝑀)𝑉) = 𝑍) |