Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ LMod) |
2 | | linccl.r |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
3 | 2 | oveq1i 6660 |
. . . . . . 7
⊢ (𝑅 ↑𝑚
𝑉) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) |
4 | 3 | eleq2i 2693 |
. . . . . 6
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
5 | 4 | biimpi 206 |
. . . . 5
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
6 | 5 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
7 | 6 | adantl 482 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
8 | | linccl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
9 | 8 | sseq2i 3630 |
. . . . . 6
⊢ (𝑉 ⊆ 𝐵 ↔ 𝑉 ⊆ (Base‘𝑀)) |
10 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘𝑀)
∈ V |
11 | 10 | ssex 4802 |
. . . . . . . 8
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ V) |
12 | | elpwg 4166 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫
(Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (𝑉 ⊆ (Base‘𝑀) → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
14 | 13 | ibir 257 |
. . . . . 6
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
15 | 9, 14 | sylbi 207 |
. . . . 5
⊢ (𝑉 ⊆ 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
16 | 15 | 3ad2ant2 1083 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
17 | 16 | adantl 482 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
18 | | lincval 42198 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
19 | 1, 7, 17, 18 | syl3anc 1326 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
20 | | eqid 2622 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
21 | | lmodcmn 18911 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
22 | 21 | adantr 481 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ CMnd) |
23 | | simpr1 1067 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ Fin) |
24 | 1 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) |
25 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
26 | 2, 25 | eqeltri 2697 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
27 | | elmapg 7870 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝑉 ∈ Fin) → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆:𝑉⟶𝑅)) |
28 | 26, 27 | mpan 706 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆:𝑉⟶𝑅)) |
29 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝑆:𝑉⟶𝑅 ∧ 𝑣 ∈ 𝑉) → (𝑆‘𝑣) ∈ 𝑅) |
30 | 29 | ex 450 |
. . . . . . . . . 10
⊢ (𝑆:𝑉⟶𝑅 → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
31 | 28, 30 | syl6bi 243 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅))) |
32 | 31 | imp 445 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
33 | 32 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
34 | 33 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
35 | 34 | imp 445 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → (𝑆‘𝑣) ∈ 𝑅) |
36 | | ssel 3597 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
37 | 36 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
38 | 37 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
39 | 38 | imp 445 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) |
40 | | eqid 2622 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
41 | | eqid 2622 |
. . . . . 6
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
42 | 8, 40, 41, 2 | lmodvscl 18880 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑆‘𝑣) ∈ 𝑅 ∧ 𝑣 ∈ 𝐵) → ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) |
43 | 24, 35, 39, 42 | syl3anc 1326 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) |
44 | | eqid 2622 |
. . . 4
⊢ (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) |
45 | 43, 44 | fmptd 6385 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)):𝑉⟶𝐵) |
46 | 16 | anim2i 593 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
47 | | simpr3 1069 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) |
48 | | elmapi 7879 |
. . . . . . 7
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → 𝑆:𝑉⟶𝑅) |
49 | 48 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑆:𝑉⟶𝑅) |
50 | 49 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆:𝑉⟶𝑅) |
51 | | fvexd 6203 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) →
(0g‘(Scalar‘𝑀)) ∈ V) |
52 | 50, 23, 51 | fdmfifsupp 8285 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 finSupp
(0g‘(Scalar‘𝑀))) |
53 | 40, 2 | scmfsupp 42159 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑆 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
54 | 46, 47, 52, 53 | syl3anc 1326 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
55 | 8, 20, 22, 23, 45, 54 | gsumcl 18316 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝐵) |
56 | 19, 55 | eqeltrd 2701 |
1
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵) |