Step | Hyp | Ref
| Expression |
1 | | psdvsca.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | eqid 2735 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | eqid 2735 |
. . . 4
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
4 | | psdvsca.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
5 | | psdvsca.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CRing) |
6 | 5 | crngringd 20264 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
7 | | ringmgm 20262 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mgm) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Mgm) |
9 | | psdvsca.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐼) |
10 | | psdvsca.m |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑆) |
11 | | psdvsca.k |
. . . . . 6
⊢ 𝐾 = (Base‘𝑅) |
12 | | psdvsca.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
13 | | psdvsca.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
14 | 1, 10, 11, 4, 6, 12, 13 | psrvscacl 21989 |
. . . . 5
⊢ (𝜑 → (𝐶 · 𝐹) ∈ 𝐵) |
15 | 1, 4, 8, 9, 14 | psdcl 22183 |
. . . 4
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) ∈ 𝐵) |
16 | 1, 2, 3, 4, 15 | psrelbas 21972 |
. . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
17 | 16 | ffnd 6738 |
. 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
18 | 1, 4, 8, 9, 13 | psdcl 22183 |
. . . . 5
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |
19 | 1, 10, 11, 4, 6, 12, 18 | psrvscacl 21989 |
. . . 4
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)) ∈ 𝐵) |
20 | 1, 2, 3, 4, 19 | psrelbas 21972 |
. . 3
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
21 | 20 | ffnd 6738 |
. 2
⊢ (𝜑 → (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
22 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring) |
23 | 3 | psrbagf 21956 |
. . . . . . . 8
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑:𝐼⟶ℕ0) |
24 | 23 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑:𝐼⟶ℕ0) |
25 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑋 ∈ 𝐼) |
26 | 24, 25 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑‘𝑋) ∈
ℕ0) |
27 | | peano2nn0 12564 |
. . . . . . 7
⊢ ((𝑑‘𝑋) ∈ ℕ0 → ((𝑑‘𝑋) + 1) ∈
ℕ0) |
28 | 27 | nn0zd 12637 |
. . . . . 6
⊢ ((𝑑‘𝑋) ∈ ℕ0 → ((𝑑‘𝑋) + 1) ∈ ℤ) |
29 | 26, 28 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑‘𝑋) + 1) ∈ ℤ) |
30 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐶 ∈ 𝐾) |
31 | 1, 11, 3, 4, 13 | psrelbas 21972 |
. . . . . . 7
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
33 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
34 | | reldmpsr 21952 |
. . . . . . . . . . 11
⊢ Rel dom
mPwSer |
35 | 1, 4, 34 | strov2rcl 17253 |
. . . . . . . . . 10
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
36 | 13, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ V) |
37 | 3 | psrbagsn 22105 |
. . . . . . . . 9
⊢ (𝐼 ∈ V → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
40 | 3 | psrbagaddcl 21962 |
. . . . . . 7
⊢ ((𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
41 | 33, 39, 40 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
42 | 32, 41 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ 𝐾) |
43 | | eqid 2735 |
. . . . . 6
⊢
(.g‘𝑅) = (.g‘𝑅) |
44 | | eqid 2735 |
. . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) |
45 | 11, 43, 44 | mulgass3 20370 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (((𝑑‘𝑋) + 1) ∈ ℤ ∧ 𝐶 ∈ 𝐾 ∧ (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ 𝐾)) → (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
46 | 22, 29, 30, 42, 45 | syl13anc 1371 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
47 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹 ∈ 𝐵) |
48 | 1, 4, 3, 25, 47, 33 | psdcoef 22182 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
49 | 48 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑)) = (𝐶(.r‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
50 | 1, 10, 11, 4, 44, 3, 30, 47, 41 | psrvscaval 21988 |
. . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
51 | 50 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐶(.r‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) |
52 | 46, 49, 51 | 3eqtr4rd 2786 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑))) |
53 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐶 · 𝐹) ∈ 𝐵) |
54 | 1, 4, 3, 25, 53, 33 | psdcoef 22182 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹))‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐶 · 𝐹)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) |
55 | 18 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) |
56 | 1, 10, 11, 4, 44, 3, 30, 55, 33 | psrvscaval 21988 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))‘𝑑) = (𝐶(.r‘𝑅)((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹)‘𝑑))) |
57 | 52, 54, 56 | 3eqtr4d 2785 |
. 2
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹))‘𝑑) = ((𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))‘𝑑)) |
58 | 17, 21, 57 | eqfnfvd 7054 |
1
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐶 · 𝐹)) = (𝐶 · (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹))) |