Step |
Hyp |
Ref |
Expression |
1 |
|
rmfsuppf2.r |
⊢ 𝑅 = ( Base ‘ 𝑀 ) |
2 |
|
rmfsupp2.m |
⊢ ( 𝜑 → 𝑀 ∈ Ring ) |
3 |
|
rmfsupp2.v |
⊢ ( 𝜑 → 𝑉 ∈ 𝑋 ) |
4 |
|
rmfsupp2.c |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐶 ∈ 𝑅 ) |
5 |
|
rmfsupp2.a |
⊢ ( 𝜑 → 𝐴 : 𝑉 ⟶ 𝑅 ) |
6 |
|
rmfsupp2.1 |
⊢ ( 𝜑 → 𝐴 finSupp ( 0g ‘ 𝑀 ) ) |
7 |
|
funmpt |
⊢ Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) |
8 |
7
|
a1i |
⊢ ( 𝜑 → Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ) |
9 |
3
|
mptexd |
⊢ ( 𝜑 → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∈ V ) |
10 |
|
ringgrp |
⊢ ( 𝑀 ∈ Ring → 𝑀 ∈ Grp ) |
11 |
|
eqid |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) |
12 |
1 11
|
grpidcl |
⊢ ( 𝑀 ∈ Grp → ( 0g ‘ 𝑀 ) ∈ 𝑅 ) |
13 |
2 10 12
|
3syl |
⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ 𝑅 ) |
14 |
|
suppval1 |
⊢ ( ( Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ 𝑅 ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
15 |
8 9 13 14
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
16 |
|
ovex |
⊢ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ∈ V |
17 |
|
eqid |
⊢ ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) |
18 |
16 17
|
dmmpti |
⊢ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) = 𝑉 |
19 |
18
|
a1i |
⊢ ( 𝜑 → dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) = 𝑉 ) |
20 |
|
ovex |
⊢ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ∈ V |
21 |
|
nfcv |
⊢ Ⅎ 𝑣 𝑢 |
22 |
|
nfcv |
⊢ Ⅎ 𝑣 ( 𝐴 ‘ 𝑢 ) |
23 |
|
nfcv |
⊢ Ⅎ 𝑣 ( .r ‘ 𝑀 ) |
24 |
|
nfcsb1v |
⊢ Ⅎ 𝑣 ⦋ 𝑢 / 𝑣 ⦌ 𝐶 |
25 |
22 23 24
|
nfov |
⊢ Ⅎ 𝑣 ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) |
26 |
|
fveq2 |
⊢ ( 𝑣 = 𝑢 → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑢 ) ) |
27 |
|
csbeq1a |
⊢ ( 𝑣 = 𝑢 → 𝐶 = ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) |
28 |
26 27
|
oveq12d |
⊢ ( 𝑣 = 𝑢 → ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) = ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
29 |
21 25 28 17
|
fvmptf |
⊢ ( ( 𝑢 ∈ 𝑉 ∧ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ∈ V ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
30 |
20 29
|
mpan2 |
⊢ ( 𝑢 ∈ 𝑉 → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
31 |
30 18
|
eleq2s |
⊢ ( 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) = ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
33 |
32
|
neeq1d |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) ) ) |
34 |
19 33
|
rabeqbidva |
⊢ ( 𝜑 → { 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑢 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) } ) |
35 |
5
|
fdmd |
⊢ ( 𝜑 → dom 𝐴 = 𝑉 ) |
36 |
35
|
rabeqdv |
⊢ ( 𝜑 → { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑢 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
37 |
5
|
ffund |
⊢ ( 𝜑 → Fun 𝐴 ) |
38 |
1
|
fvexi |
⊢ 𝑅 ∈ V |
39 |
38
|
a1i |
⊢ ( 𝜑 → 𝑅 ∈ V ) |
40 |
39 3
|
elmapd |
⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐴 : 𝑉 ⟶ 𝑅 ) ) |
41 |
5 40
|
mpbird |
⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) |
42 |
|
suppval1 |
⊢ ( ( Fun 𝐴 ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑅 ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
43 |
37 41 13 42
|
syl3anc |
⊢ ( 𝜑 → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
44 |
6
|
fsuppimpd |
⊢ ( 𝜑 → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) |
45 |
43 44
|
eqeltrrd |
⊢ ( 𝜑 → { 𝑢 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ) |
46 |
36 45
|
eqeltrrd |
⊢ ( 𝜑 → { 𝑢 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ) |
47 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) |
48 |
47
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) = ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ) |
49 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → 𝑀 ∈ Ring ) |
50 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → 𝑢 ∈ 𝑉 ) |
51 |
4
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑉 𝐶 ∈ 𝑅 ) |
52 |
51
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑉 𝐶 ∈ 𝑅 ) |
53 |
|
rspcsbela |
⊢ ( ( 𝑢 ∈ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 𝐶 ∈ 𝑅 ) → ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ∈ 𝑅 ) |
54 |
50 52 53
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ∈ 𝑅 ) |
55 |
|
eqid |
⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 ) |
56 |
1 55 11
|
ringlz |
⊢ ( ( 𝑀 ∈ Ring ∧ ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ∈ 𝑅 ) → ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) = ( 0g ‘ 𝑀 ) ) |
57 |
49 54 56
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) = ( 0g ‘ 𝑀 ) ) |
58 |
48 57
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) = ( 0g ‘ 𝑀 ) ) |
59 |
58
|
ex |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑢 ) = ( 0g ‘ 𝑀 ) → ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) = ( 0g ‘ 𝑀 ) ) ) |
60 |
59
|
necon3d |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → ( ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) ) ) |
61 |
60
|
ss2rabdv |
⊢ ( 𝜑 → { 𝑢 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑢 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) |
62 |
|
ssfi |
⊢ ( ( { 𝑢 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ∧ { 𝑢 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑢 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ) → { 𝑢 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ) |
63 |
46 61 62
|
syl2anc |
⊢ ( 𝜑 → { 𝑢 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑢 ) ( .r ‘ 𝑀 ) ⦋ 𝑢 / 𝑣 ⦌ 𝐶 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ) |
64 |
34 63
|
eqeltrd |
⊢ ( 𝜑 → { 𝑢 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ‘ 𝑢 ) ≠ ( 0g ‘ 𝑀 ) } ∈ Fin ) |
65 |
15 64
|
eqeltrd |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) |
66 |
|
isfsupp |
⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ 𝑅 ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) ) |
67 |
9 13 66
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) ) |
68 |
8 65 67
|
mpbir2and |
⊢ ( 𝜑 → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( .r ‘ 𝑀 ) 𝐶 ) ) finSupp ( 0g ‘ 𝑀 ) ) |