Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
2 | | eqid 2610 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
3 | | lincscmcl.r |
. . . . 5
⊢ 𝑅 =
(Base‘(Scalar‘𝑀)) |
4 | 1, 2, 3 | lcoval 41995 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
(𝐷 ∈ (𝑀 LinCo 𝑉) ↔ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) |
5 | 4 | adantr 480 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → (𝐷 ∈ (𝑀 LinCo 𝑉) ↔ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) |
6 | | simpl 472 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑀 ∈
LMod) |
7 | 6 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝑀 ∈ LMod) |
8 | | simpr 476 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → 𝐶 ∈ 𝑅) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐶 ∈ 𝑅) |
10 | | simprl 790 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐷 ∈ (Base‘𝑀)) |
11 | | lincscmcl.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑀) |
12 | 1, 2, 11, 3 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (Base‘𝑀)) → (𝐶 · 𝐷) ∈ (Base‘𝑀)) |
13 | 7, 9, 10, 12 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 · 𝐷) ∈ (Base‘𝑀)) |
14 | 2 | lmodring 18694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) ∈
Ring) |
15 | 14 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → (Scalar‘𝑀) ∈ Ring) |
16 | 15 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (Scalar‘𝑀) ∈ Ring) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ (𝑅 ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) ∧ 𝑣 ∈ 𝑉) → (Scalar‘𝑀) ∈ Ring) |
18 | 8 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → 𝐶 ∈ 𝑅) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ (𝑅 ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ 𝑅) |
20 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝑅 ↑𝑚 𝑉) → 𝑥:𝑉⟶𝑅) |
21 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥:𝑉⟶𝑅 ∧ 𝑣 ∈ 𝑉) → (𝑥‘𝑣) ∈ 𝑅) |
22 | 21 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥:𝑉⟶𝑅 → (𝑣 ∈ 𝑉 → (𝑥‘𝑣) ∈ 𝑅)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑅 ↑𝑚 𝑉) → (𝑣 ∈ 𝑉 → (𝑥‘𝑣) ∈ 𝑅)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝑣 ∈ 𝑉 → (𝑥‘𝑣) ∈ 𝑅)) |
25 | 24 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑣 ∈ 𝑉 → (𝑥‘𝑣) ∈ 𝑅)) |
26 | 25 | imp 444 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ (𝑅 ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) ∧ 𝑣 ∈ 𝑉) → (𝑥‘𝑣) ∈ 𝑅) |
27 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(.r‘(Scalar‘𝑀)) =
(.r‘(Scalar‘𝑀)) |
28 | 3, 27 | ringcl 18384 |
. . . . . . . . . . . . . 14
⊢
(((Scalar‘𝑀)
∈ Ring ∧ 𝐶 ∈
𝑅 ∧ (𝑥‘𝑣) ∈ 𝑅) → (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)) ∈ 𝑅) |
29 | 17, 19, 26, 28 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ (𝑅 ↑𝑚
𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) ∧ 𝑣 ∈ 𝑉) → (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)) ∈ 𝑅) |
30 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) = (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) |
31 | 29, 30 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))):𝑉⟶𝑅) |
32 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝑀)) ∈ V |
33 | 3, 32 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 𝑅 ∈ V |
34 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
𝑉 ∈ 𝒫
(Base‘𝑀)) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
37 | | elmapg 7757 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ V ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) ∈ (𝑅 ↑𝑚 𝑉) ↔ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))):𝑉⟶𝑅)) |
38 | 33, 36, 37 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) ∈ (𝑅 ↑𝑚 𝑉) ↔ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))):𝑉⟶𝑅)) |
39 | 31, 38 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) ∈ (𝑅 ↑𝑚 𝑉)) |
40 | 15, 35, 8 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ((Scalar‘𝑀) ∈ Ring ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝐶 ∈ 𝑅)) |
41 | 40 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → ((Scalar‘𝑀) ∈ Ring ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝐶 ∈ 𝑅)) |
42 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 ∈ (𝑅 ↑𝑚 𝑉)) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → 𝑥 ∈ (𝑅 ↑𝑚 𝑉)) |
44 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 finSupp
(0g‘(Scalar‘𝑀))) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → 𝑥 finSupp
(0g‘(Scalar‘𝑀))) |
46 | 3 | rmfsupp 41949 |
. . . . . . . . . . . 12
⊢
((((Scalar‘𝑀)
∈ Ring ∧ 𝑉 ∈
𝒫 (Base‘𝑀)
∧ 𝐶 ∈ 𝑅) ∧ 𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀))) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) finSupp
(0g‘(Scalar‘𝑀))) |
47 | 41, 43, 45, 46 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) finSupp
(0g‘(Scalar‘𝑀))) |
48 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 = (𝑥( linC ‘𝑀)𝑉) → (𝐶 · 𝐷) = (𝐶 · (𝑥( linC ‘𝑀)𝑉))) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 · 𝐷) = (𝐶 · (𝑥( linC ‘𝑀)𝑉))) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 · 𝐷) = (𝐶 · (𝑥( linC ‘𝑀)𝑉))) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝐶 · 𝐷) = (𝐶 · (𝑥( linC ‘𝑀)𝑉))) |
52 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
53 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) → 𝑥 ∈ (𝑅 ↑𝑚 𝑉)) |
54 | 53, 8 | anim12i 588 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐶 ∈ 𝑅)) |
55 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥( linC ‘𝑀)𝑉) = (𝑥( linC ‘𝑀)𝑉) |
56 | 11, 27, 55, 3, 30 | lincscm 42013 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧
(𝑥 ∈ (𝑅 ↑𝑚
𝑉) ∧ 𝐶 ∈ 𝑅) ∧ 𝑥 finSupp
(0g‘(Scalar‘𝑀))) → (𝐶 · (𝑥( linC ‘𝑀)𝑉)) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉)) |
57 | 52, 54, 45, 56 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝐶 · (𝑥( linC ‘𝑀)𝑉)) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉)) |
58 | 51, 57 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → (𝐶 · 𝐷) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉)) |
59 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) → (𝑠 finSupp
(0g‘(Scalar‘𝑀)) ↔ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) finSupp
(0g‘(Scalar‘𝑀)))) |
60 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) → (𝑠( linC ‘𝑀)𝑉) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉)) |
61 | 60 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) → ((𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉) ↔ (𝐶 · 𝐷) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉))) |
62 | 59, 61 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) → ((𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉)) ↔ ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉)))) |
63 | 62 | rspcev 3282 |
. . . . . . . . . . 11
⊢ (((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) ∈ (𝑅 ↑𝑚 𝑉) ∧ ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣))) finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘(Scalar‘𝑀))(𝑥‘𝑣)))( linC ‘𝑀)𝑉))) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
64 | 39, 47, 58, 63 | syl12anc 1316 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) ∧ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅)) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
65 | 64 | ex 449 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) ∧ 𝐷 ∈ (Base‘𝑀)) → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉)))) |
66 | 65 | ex 449 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝑅 ↑𝑚 𝑉) ∧ (𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
67 | 66 | rexlimiva 3010 |
. . . . . . 7
⊢
(∃𝑥 ∈
(𝑅
↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐷 ∈ (Base‘𝑀) → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
68 | 67 | impcom 445 |
. . . . . 6
⊢ ((𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉)))) |
69 | 68 | impcom 445 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))) |
70 | 1, 2, 3 | lcoval 41995 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) →
((𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 · 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
71 | 70 | ad2antrr 758 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → ((𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 · 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ (𝑅 ↑𝑚 𝑉)(𝑠 finSupp
(0g‘(Scalar‘𝑀)) ∧ (𝐶 · 𝐷) = (𝑠( linC ‘𝑀)𝑉))))) |
72 | 13, 69, 71 | mpbir2and 959 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉)) |
73 | 72 | ex 449 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → ((𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ (𝑅 ↑𝑚 𝑉)(𝑥 finSupp
(0g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉))) |
74 | 5, 73 | sylbid 229 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅) → (𝐷 ∈ (𝑀 LinCo 𝑉) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉))) |
75 | 74 | 3impia 1253 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 · 𝐷) ∈ (𝑀 LinCo 𝑉)) |