Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ LMod) |
2 | | linccl.r |
. . . . . . . 8
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
3 | 2 | oveq1i 6559 |
. . . . . . 7
⊢ (𝑅 ↑𝑚
𝑉) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) |
4 | 3 | eleq2i 2680 |
. . . . . 6
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
5 | 4 | biimpi 205 |
. . . . 5
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
6 | 5 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
7 | 6 | adantl 481 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
8 | | linccl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
9 | 8 | sseq2i 3593 |
. . . . . 6
⊢ (𝑉 ⊆ 𝐵 ↔ 𝑉 ⊆ (Base‘𝑀)) |
10 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑀)
∈ V |
11 | 10 | ssex 4730 |
. . . . . . . 8
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ V) |
12 | | elpwg 4116 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫
(Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (𝑉 ⊆ (Base‘𝑀) → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
14 | 13 | ibir 256 |
. . . . . 6
⊢ (𝑉 ⊆ (Base‘𝑀) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
15 | 9, 14 | sylbi 206 |
. . . . 5
⊢ (𝑉 ⊆ 𝐵 → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
16 | 15 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
17 | 16 | adantl 481 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
18 | | lincval 41992 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
19 | 1, 7, 17, 18 | syl3anc 1318 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)))) |
20 | | eqid 2610 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
21 | | lmodcmn 18734 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd) |
22 | 21 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑀 ∈ CMnd) |
23 | | simpr1 1060 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ Fin) |
24 | 1 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑀 ∈ LMod) |
25 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
26 | 2, 25 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
27 | | elmapg 7757 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ V ∧ 𝑉 ∈ Fin) → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆:𝑉⟶𝑅)) |
28 | 26, 27 | mpan 702 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) ↔ 𝑆:𝑉⟶𝑅)) |
29 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝑆:𝑉⟶𝑅 ∧ 𝑣 ∈ 𝑉) → (𝑆‘𝑣) ∈ 𝑅) |
30 | 29 | ex 449 |
. . . . . . . . . 10
⊢ (𝑆:𝑉⟶𝑅 → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
31 | 28, 30 | syl6bi 242 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin → (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅))) |
32 | 31 | imp 444 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
33 | 32 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
34 | 33 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 → (𝑆‘𝑣) ∈ 𝑅)) |
35 | 34 | imp 444 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → (𝑆‘𝑣) ∈ 𝑅) |
36 | | ssel 3562 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝐵 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
37 | 36 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
38 | 37 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵)) |
39 | 38 | imp 444 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝐵) |
40 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
41 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
42 | 8, 40, 41, 2 | lmodvscl 18703 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑆‘𝑣) ∈ 𝑅 ∧ 𝑣 ∈ 𝐵) → ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) |
43 | 24, 35, 39, 42 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝐵) |
44 | | eqid 2610 |
. . . 4
⊢ (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) |
45 | 43, 44 | fmptd 6292 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)):𝑉⟶𝐵) |
46 | 16 | anim2i 591 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
47 | | simpr3 1062 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) |
48 | | elmapi 7765 |
. . . . . . 7
⊢ (𝑆 ∈ (𝑅 ↑𝑚 𝑉) → 𝑆:𝑉⟶𝑅) |
49 | 48 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑆:𝑉⟶𝑅) |
50 | 49 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆:𝑉⟶𝑅) |
51 | | fvex 6113 |
. . . . . 6
⊢
(0g‘(Scalar‘𝑀)) ∈ V |
52 | 51 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) →
(0g‘(Scalar‘𝑀)) ∈ V) |
53 | 50, 23, 52 | fdmfifsupp 8168 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑆 finSupp
(0g‘(Scalar‘𝑀))) |
54 | 40, 2 | scmfsupp 41953 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑆 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
55 | 46, 47, 53, 54 | syl3anc 1318 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
56 | 8, 20, 22, 23, 45, 55 | gsumcl 18139 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑆‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝐵) |
57 | 19, 56 | eqeltrd 2688 |
1
⊢ ((𝑀 ∈ LMod ∧ (𝑉 ∈ Fin ∧ 𝑉 ⊆ 𝐵 ∧ 𝑆 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑆( linC ‘𝑀)𝑉) ∈ 𝐵) |