Step | Hyp | Ref
| Expression |
1 | | funmpt 6418 |
. . 3
⊢ Fun
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → Fun (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))) |
3 | | rmfsupp2.v |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝑋) |
4 | 3 | mptexd 7040 |
. . . 4
⊢ (𝜑 → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∈ V) |
5 | | rmfsupp2.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ Ring) |
6 | | ringgrp 19567 |
. . . . 5
⊢ (𝑀 ∈ Ring → 𝑀 ∈ Grp) |
7 | | rmfsuppf2.r |
. . . . . 6
⊢ 𝑅 = (Base‘𝑀) |
8 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑀) |
9 | 7, 8 | grpidcl 18395 |
. . . . 5
⊢ (𝑀 ∈ Grp →
(0g‘𝑀)
∈ 𝑅) |
10 | 5, 6, 9 | 3syl 18 |
. . . 4
⊢ (𝜑 → (0g‘𝑀) ∈ 𝑅) |
11 | | suppval1 7909 |
. . . 4
⊢ ((Fun
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∧ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∈ V ∧ (0g‘𝑀) ∈ 𝑅) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) supp (0g‘𝑀)) = {𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) ≠ (0g‘𝑀)}) |
12 | 2, 4, 10, 11 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) supp (0g‘𝑀)) = {𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) ≠ (0g‘𝑀)}) |
13 | | ovex 7246 |
. . . . . . 7
⊢ ((𝐴‘𝑣)(.r‘𝑀)𝐶) ∈ V |
14 | | eqid 2737 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) |
15 | 13, 14 | dmmpti 6522 |
. . . . . 6
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) = 𝑉 |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝜑 → dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) = 𝑉) |
17 | | ovex 7246 |
. . . . . . . . 9
⊢ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ∈ V |
18 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑣𝑢 |
19 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣(𝐴‘𝑢) |
20 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣(.r‘𝑀) |
21 | | nfcsb1v 3836 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣⦋𝑢 / 𝑣⦌𝐶 |
22 | 19, 20, 21 | nfov 7243 |
. . . . . . . . . 10
⊢
Ⅎ𝑣((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) |
23 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑢 → (𝐴‘𝑣) = (𝐴‘𝑢)) |
24 | | csbeq1a 3825 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑢 → 𝐶 = ⦋𝑢 / 𝑣⦌𝐶) |
25 | 23, 24 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑢 → ((𝐴‘𝑣)(.r‘𝑀)𝐶) = ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
26 | 18, 22, 25, 14 | fvmptf 6839 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑉 ∧ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ∈ V) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) = ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
27 | 17, 26 | mpan2 691 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝑉 → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) = ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
28 | 27, 15 | eleq2s 2856 |
. . . . . . 7
⊢ (𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) = ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
29 | 28 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) = ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
30 | 29 | neeq1d 3000 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))) → (((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) ≠ (0g‘𝑀) ↔ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀))) |
31 | 16, 30 | rabeqbidva 3397 |
. . . 4
⊢ (𝜑 → {𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) ≠ (0g‘𝑀)} = {𝑢 ∈ 𝑉 ∣ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀)}) |
32 | | rmfsupp2.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴:𝑉⟶𝑅) |
33 | 32 | fdmd 6556 |
. . . . . . 7
⊢ (𝜑 → dom 𝐴 = 𝑉) |
34 | 33 | rabeqdv 3395 |
. . . . . 6
⊢ (𝜑 → {𝑢 ∈ dom 𝐴 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)} = {𝑢 ∈ 𝑉 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)}) |
35 | 32 | ffund 6549 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐴) |
36 | 7 | fvexi 6731 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ V) |
38 | 37, 3 | elmapd 8522 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ (𝑅 ↑m 𝑉) ↔ 𝐴:𝑉⟶𝑅)) |
39 | 32, 38 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (𝑅 ↑m 𝑉)) |
40 | | suppval1 7909 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (0g‘𝑀) ∈ 𝑅) → (𝐴 supp (0g‘𝑀)) = {𝑢 ∈ dom 𝐴 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)}) |
41 | 35, 39, 10, 40 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐴 supp (0g‘𝑀)) = {𝑢 ∈ dom 𝐴 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)}) |
42 | | rmfsupp2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 finSupp (0g‘𝑀)) |
43 | 42 | fsuppimpd 8992 |
. . . . . . 7
⊢ (𝜑 → (𝐴 supp (0g‘𝑀)) ∈ Fin) |
44 | 41, 43 | eqeltrrd 2839 |
. . . . . 6
⊢ (𝜑 → {𝑢 ∈ dom 𝐴 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)} ∈ Fin) |
45 | 34, 44 | eqeltrrd 2839 |
. . . . 5
⊢ (𝜑 → {𝑢 ∈ 𝑉 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)} ∈ Fin) |
46 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → (𝐴‘𝑢) = (0g‘𝑀)) |
47 | 46 | oveq1d 7228 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) = ((0g‘𝑀)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶)) |
48 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → 𝑀 ∈ Ring) |
49 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → 𝑢 ∈ 𝑉) |
50 | | rmfsupp2.c |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ 𝑅) |
51 | 50 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 𝐶 ∈ 𝑅) |
52 | 51 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → ∀𝑣 ∈ 𝑉 𝐶 ∈ 𝑅) |
53 | | rspcsbela 4350 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑉 ∧ ∀𝑣 ∈ 𝑉 𝐶 ∈ 𝑅) → ⦋𝑢 / 𝑣⦌𝐶 ∈ 𝑅) |
54 | 49, 52, 53 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → ⦋𝑢 / 𝑣⦌𝐶 ∈ 𝑅) |
55 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑀) = (.r‘𝑀) |
56 | 7, 55, 8 | ringlz 19605 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Ring ∧
⦋𝑢 / 𝑣⦌𝐶 ∈ 𝑅) → ((0g‘𝑀)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) = (0g‘𝑀)) |
57 | 48, 54, 56 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → ((0g‘𝑀)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) = (0g‘𝑀)) |
58 | 47, 57 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑉) ∧ (𝐴‘𝑢) = (0g‘𝑀)) → ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) = (0g‘𝑀)) |
59 | 58 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → ((𝐴‘𝑢) = (0g‘𝑀) → ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) = (0g‘𝑀))) |
60 | 59 | necon3d 2961 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → (((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀) → (𝐴‘𝑢) ≠ (0g‘𝑀))) |
61 | 60 | ss2rabdv 3989 |
. . . . 5
⊢ (𝜑 → {𝑢 ∈ 𝑉 ∣ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀)} ⊆ {𝑢 ∈ 𝑉 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)}) |
62 | | ssfi 8851 |
. . . . 5
⊢ (({𝑢 ∈ 𝑉 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)} ∈ Fin ∧ {𝑢 ∈ 𝑉 ∣ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀)} ⊆ {𝑢 ∈ 𝑉 ∣ (𝐴‘𝑢) ≠ (0g‘𝑀)}) → {𝑢 ∈ 𝑉 ∣ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀)} ∈ Fin) |
63 | 45, 61, 62 | syl2anc 587 |
. . . 4
⊢ (𝜑 → {𝑢 ∈ 𝑉 ∣ ((𝐴‘𝑢)(.r‘𝑀)⦋𝑢 / 𝑣⦌𝐶) ≠ (0g‘𝑀)} ∈ Fin) |
64 | 31, 63 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → {𝑢 ∈ dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∣ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶))‘𝑢) ≠ (0g‘𝑀)} ∈ Fin) |
65 | 12, 64 | eqeltrd 2838 |
. 2
⊢ (𝜑 → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) supp (0g‘𝑀)) ∈ Fin) |
66 | | isfsupp 8989 |
. . 3
⊢ (((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∈ V ∧ (0g‘𝑀) ∈ 𝑅) → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) finSupp (0g‘𝑀) ↔ (Fun (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∧ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) supp (0g‘𝑀)) ∈
Fin))) |
67 | 4, 10, 66 | syl2anc 587 |
. 2
⊢ (𝜑 → ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) finSupp (0g‘𝑀) ↔ (Fun (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) ∧ ((𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) supp (0g‘𝑀)) ∈
Fin))) |
68 | 2, 65, 67 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(.r‘𝑀)𝐶)) finSupp (0g‘𝑀)) |