Step | Hyp | Ref
| Expression |
1 | | psdvsca.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2728 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2728 |
. . . 4
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
4 | | psdvsca.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
5 | | psdvsca.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | psdvsca.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CRing) |
7 | 6 | crngringd 20193 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
8 | | ringmgm 20191 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mgm) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Mgm) |
10 | | psdvsca.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
11 | | psdvsca.m |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑆) |
12 | | psdvsca.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑅) |
13 | | psdvsca.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
14 | | psdvsca.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
15 | 1, 11, 12, 4, 7, 13, 14 | psrvscacl 21901 |
. . . . 5
⊢ (𝜑 → (𝐶 · 𝐹) ∈ 𝐵) |
16 | 1, 4, 5, 9, 10, 15 | psdcl 22092 |
. . . 4
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) ∈ 𝐵) |
17 | 1, 2, 3, 4, 16 | psrelbas 21886 |
. . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
18 | 17 | ffnd 6728 |
. 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
19 | 1, 4, 5, 9, 10, 14 | psdcl 22092 |
. . . . 5
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |
20 | 1, 11, 12, 4, 7, 13, 19 | psrvscacl 21901 |
. . . 4
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)) ∈ 𝐵) |
21 | 1, 2, 3, 4, 20 | psrelbas 21886 |
. . 3
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
22 | 21 | ffnd 6728 |
. 2
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
23 | 7 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring) |
24 | 3 | psrbagf 21858 |
. . . . . . . 8
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑:𝐼⟶ℕ0) |
25 | 24 | adantl 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑:𝐼⟶ℕ0) |
26 | 10 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑋 ∈ 𝐼) |
27 | 25, 26 | ffvelcdmd 7100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑‘𝑋) ∈
ℕ0) |
28 | | peano2nn0 12550 |
. . . . . . 7
⊢ ((𝑑‘𝑋) ∈ ℕ0 → ((𝑑‘𝑋) + 1) ∈
ℕ0) |
29 | 28 | nn0zd 12622 |
. . . . . 6
⊢ ((𝑑‘𝑋) ∈ ℕ0 → ((𝑑‘𝑋) + 1) ∈ ℤ) |
30 | 27, 29 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑‘𝑋) + 1) ∈ ℤ) |
31 | 13 | adantr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐶 ∈ 𝐾) |
32 | 1, 12, 3, 4, 14 | psrelbas 21886 |
. . . . . . 7
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
33 | 32 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
34 | | simpr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
35 | 3 | psrbagsn 22014 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
36 | 5, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
37 | 36 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
38 | 3 | psrbagaddcl 21868 |
. . . . . . 7
⊢ ((𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
39 | 34, 37, 38 | syl2anc 582 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
40 | 33, 39 | ffvelcdmd 7100 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ 𝐾) |
41 | | eqid 2728 |
. . . . . 6
⊢
(.g‘𝑅) = (.g‘𝑅) |
42 | | eqid 2728 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
43 | 12, 41, 42 | mulgass3 20299 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (((𝑑‘𝑋) + 1) ∈ ℤ ∧ 𝐶 ∈ 𝐾 ∧ (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ 𝐾)) → (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
44 | 23, 30, 31, 40, 43 | syl13anc 1369 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
45 | 5 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑉) |
46 | 6 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing) |
47 | 14 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹 ∈ 𝐵) |
48 | 1, 4, 3, 45, 46, 26, 47, 34 | psdcoef 22091 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
49 | 48 | oveq2d 7442 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑)) = (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
50 | 1, 11, 12, 4, 42, 3, 31, 47, 39 | psrvscaval 21900 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
51 | 50 | oveq2d 7442 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
52 | 44, 49, 51 | 3eqtr4rd 2779 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑))) |
53 | 15 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶 · 𝐹) ∈ 𝐵) |
54 | 1, 4, 3, 45, 46, 26, 53, 34 | psdcoef 22091 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹))‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
55 | 19 | adantr 479 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |
56 | 1, 11, 12, 4, 42, 3, 31, 55, 34 | psrvscaval 21900 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))‘𝑑) = (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑))) |
57 | 52, 54, 56 | 3eqtr4d 2778 |
. 2
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹))‘𝑑) = ((𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))‘𝑑)) |
58 | 18, 22, 57 | eqfnfvd 7048 |
1
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) = (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))) |