Step | Hyp | Ref
| Expression |
1 | | elmapi 7765 |
. . . . 5
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
2 | | fdm 5964 |
. . . . . 6
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
3 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
4 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑥 → (𝐴‘𝑣) = (𝐴‘𝑥)) |
5 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥) |
6 | 4, 5 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑥 → ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
7 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) ∧ 𝑣 = 𝑥) → ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣) = ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
8 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
9 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ V) |
11 | 3, 7, 8, 10 | fvmptd 6197 |
. . . . . . . . . . 11
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) = ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
12 | 11 | neeq1d 2841 |
. . . . . . . . . 10
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → (((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀) ↔ ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ≠ (0g‘𝑀))) |
13 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝑥) = (0g‘𝑆) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) = ((0g‘𝑆)( ·𝑠
‘𝑀)𝑥)) |
14 | | simplrr 797 |
. . . . . . . . . . . . . 14
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → 𝑀 ∈ LMod) |
15 | | elelpwi 4119 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀)) |
16 | 15 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝑀 ∈ LMod) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (Base‘𝑀))) |
19 | 18 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑀)) |
20 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑀) =
(Base‘𝑀) |
21 | | scmsuppss.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (Scalar‘𝑀) |
22 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
23 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑆) = (0g‘𝑆) |
24 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑀) = (0g‘𝑀) |
25 | 20, 21, 22, 23, 24 | lmod0vs 18719 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑀)) →
((0g‘𝑆)(
·𝑠 ‘𝑀)𝑥) = (0g‘𝑀)) |
26 | 14, 19, 25 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → ((0g‘𝑆)(
·𝑠 ‘𝑀)𝑥) = (0g‘𝑀)) |
27 | 13, 26 | sylan9eqr 2666 |
. . . . . . . . . . . 12
⊢ (((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) ∧ (𝐴‘𝑥) = (0g‘𝑆)) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) = (0g‘𝑀)) |
28 | 27 | ex 449 |
. . . . . . . . . . 11
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → ((𝐴‘𝑥) = (0g‘𝑆) → ((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) = (0g‘𝑀))) |
29 | 28 | necon3d 2803 |
. . . . . . . . . 10
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥)( ·𝑠
‘𝑀)𝑥) ≠ (0g‘𝑀) → (𝐴‘𝑥) ≠ (0g‘𝑆))) |
30 | 12, 29 | sylbid 229 |
. . . . . . . . 9
⊢ ((((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) ∧ 𝑥 ∈ 𝑉) → (((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀) → (𝐴‘𝑥) ≠ (0g‘𝑆))) |
31 | 30 | ss2rabdv 3646 |
. . . . . . . 8
⊢ (((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) → {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
32 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ V |
33 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) |
34 | 32, 33 | dmmpti 5936 |
. . . . . . . . . . . 12
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) = 𝑉 |
35 | | rabeq 3166 |
. . . . . . . . . . . 12
⊢ (dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) = 𝑉 → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)}) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . . . 11
⊢ (dom
𝐴 = 𝑉 → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)}) |
37 | | rabeq 3166 |
. . . . . . . . . . 11
⊢ (dom
𝐴 = 𝑉 → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
38 | 36, 37 | sseq12d 3597 |
. . . . . . . . . 10
⊢ (dom
𝐴 = 𝑉 → ({𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)} ↔ {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)})) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) → ({𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)} ↔ {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)})) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ (((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) → ({𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)} ↔ {𝑥 ∈ 𝑉 ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)})) |
41 | 31, 40 | mpbird 246 |
. . . . . . 7
⊢ (((dom
𝐴 = 𝑉 ∧ 𝐴:𝑉⟶𝑅) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑀 ∈ LMod)) → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
42 | 41 | exp43 638 |
. . . . . 6
⊢ (dom
𝐴 = 𝑉 → (𝐴:𝑉⟶𝑅 → (𝑉 ∈ 𝒫 (Base‘𝑀) → (𝑀 ∈ LMod → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)})))) |
43 | 2, 42 | mpcom 37 |
. . . . 5
⊢ (𝐴:𝑉⟶𝑅 → (𝑉 ∈ 𝒫 (Base‘𝑀) → (𝑀 ∈ LMod → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}))) |
44 | 1, 43 | syl 17 |
. . . 4
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) → (𝑀 ∈ LMod → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}))) |
45 | 44 | com13 86 |
. . 3
⊢ (𝑀 ∈ LMod → (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝐴 ∈ (𝑅 ↑𝑚
𝑉) → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}))) |
46 | 45 | 3imp 1249 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
47 | | funmpt 5840 |
. . . 4
⊢ Fun
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) |
48 | 47 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → Fun (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))) |
49 | | mptexg 6389 |
. . . 4
⊢ (𝑉 ∈ 𝒫
(Base‘𝑀) →
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∈ V) |
50 | 49 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∈ V) |
51 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑀) ∈ V |
52 | 51 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) →
(0g‘𝑀)
∈ V) |
53 | | suppval1 7188 |
. . 3
⊢ ((Fun
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∧ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∈ V ∧ (0g‘𝑀) ∈ V) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)}) |
54 | 48, 50, 52, 53 | syl3anc 1318 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣))‘𝑥) ≠ (0g‘𝑀)}) |
55 | | elmapfun 7767 |
. . . 4
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐴) |
56 | 55 | 3ad2ant3 1077 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → Fun 𝐴) |
57 | | simp3 1056 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
58 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑆) ∈ V |
59 | 58 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) →
(0g‘𝑆)
∈ V) |
60 | | suppval1 7188 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑆)
∈ V) → (𝐴 supp
(0g‘𝑆)) =
{𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
61 | 56, 57, 59, 60 | syl3anc 1318 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → (𝐴 supp (0g‘𝑆)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑆)}) |
62 | 46, 54, 61 | 3sstr4d 3611 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)( ·𝑠
‘𝑀)𝑣)) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑆))) |