| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | psdadd.s | . . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) | 
| 2 |  | psdadd.b | . . . . 5
⊢ 𝐵 = (Base‘𝑆) | 
| 3 |  | eqid 2737 | . . . . 5
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 4 |  | psdadd.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐼) | 
| 5 |  | psdadd.f | . . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝐵) | 
| 6 | 1, 2, 3, 4, 5 | psdval 22163 | . . . 4
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 7 |  | psdadd.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝐵) | 
| 8 | 1, 2, 3, 4, 7 | psdval 22163 | . . . 4
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 9 | 6, 8 | oveq12d 7449 | . . 3
⊢ (𝜑 → ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∘f
(+g‘𝑅)(((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺)) = ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) ∘f
(+g‘𝑅)(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))))) | 
| 10 |  | ovex 7464 | . . . . . 6
⊢ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) ∈ V | 
| 11 |  | eqid 2737 | . . . . . 6
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 12 | 10, 11 | fnmpti 6711 | . . . . 5
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 13 | 12 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 14 |  | ovex 7464 | . . . . . 6
⊢ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) ∈ V | 
| 15 |  | eqid 2737 | . . . . . 6
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 16 | 14, 15 | fnmpti 6711 | . . . . 5
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 17 | 16 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 18 |  | ovex 7464 | . . . . . 6
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 19 | 18 | rabex 5339 | . . . . 5
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V | 
| 20 | 19 | a1i 11 | . . . 4
⊢ (𝜑 → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) | 
| 21 |  | inidm 4227 | . . . 4
⊢ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∩ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 22 |  | fveq1 6905 | . . . . . . 7
⊢ (𝑏 = 𝑑 → (𝑏‘𝑋) = (𝑑‘𝑋)) | 
| 23 | 22 | oveq1d 7446 | . . . . . 6
⊢ (𝑏 = 𝑑 → ((𝑏‘𝑋) + 1) = ((𝑑‘𝑋) + 1)) | 
| 24 |  | fvoveq1 7454 | . . . . . 6
⊢ (𝑏 = 𝑑 → (𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 25 | 23, 24 | oveq12d 7449 | . . . . 5
⊢ (𝑏 = 𝑑 → (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 26 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 27 |  | ovexd 7466 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) ∈ V) | 
| 28 | 11, 25, 26, 27 | fvmptd3 7039 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 29 |  | fvoveq1 7454 | . . . . . 6
⊢ (𝑏 = 𝑑 → (𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 30 | 23, 29 | oveq12d 7449 | . . . . 5
⊢ (𝑏 = 𝑑 → (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 31 |  | ovexd 7466 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) ∈ V) | 
| 32 | 15, 30, 26, 31 | fvmptd3 7039 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))‘𝑑) = (((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 33 | 13, 17, 20, 20, 21, 28, 32 | offval 7706 | . . 3
⊢ (𝜑 → ((𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) ∘f
(+g‘𝑅)(𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑏‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑏 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) = (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦
((((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))(+g‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))))) | 
| 34 |  | eqid 2737 | . . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 35 |  | psdadd.p | . . . . . . . . . 10
⊢  + =
(+g‘𝑆) | 
| 36 | 1, 2, 34, 35, 5, 7 | psradd 21957 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 + 𝐺) = (𝐹 ∘f
(+g‘𝑅)𝐺)) | 
| 37 | 36 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹 + 𝐺) = (𝐹 ∘f
(+g‘𝑅)𝐺)) | 
| 38 | 37 | fveq1d 6908 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝐹 ∘f
(+g‘𝑅)𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 39 |  | reldmpsr 21934 | . . . . . . . . . . . . 13
⊢ Rel dom
mPwSer | 
| 40 | 1, 2, 39 | strov2rcl 17255 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) | 
| 41 | 5, 40 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ V) | 
| 42 | 3 | psrbagsn 22087 | . . . . . . . . . . 11
⊢ (𝐼 ∈ V → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 44 | 43 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 45 | 3 | psrbagaddcl 21944 | . . . . . . . . 9
⊢ ((𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∧ (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 46 | 26, 44, 45 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 47 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 48 | 1, 47, 3, 2, 5 | psrelbas 21954 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 49 | 48 | ffnd 6737 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 50 | 1, 47, 3, 2, 7 | psrelbas 21954 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 51 | 50 | ffnd 6737 | . . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 52 |  | eqidd 2738 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 53 |  | eqidd 2738 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = (𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) | 
| 54 | 49, 51, 20, 20, 21, 52, 53 | ofval 7708 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐹 ∘f
(+g‘𝑅)𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 55 | 46, 54 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐹 ∘f
(+g‘𝑅)𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 56 | 38, 55 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) = ((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 57 | 56 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 58 |  | psdadd.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CMnd) | 
| 59 | 58 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑅 ∈ CMnd) | 
| 60 | 3 | psrbagf 21938 | . . . . . . . . 9
⊢ (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑑:𝐼⟶ℕ0) | 
| 61 | 60 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑑:𝐼⟶ℕ0) | 
| 62 | 4 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑋 ∈ 𝐼) | 
| 63 | 61, 62 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑑‘𝑋) ∈
ℕ0) | 
| 64 |  | peano2nn0 12566 | . . . . . . 7
⊢ ((𝑑‘𝑋) ∈ ℕ0 → ((𝑑‘𝑋) + 1) ∈
ℕ0) | 
| 65 | 63, 64 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑑‘𝑋) + 1) ∈
ℕ0) | 
| 66 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹 ∈ 𝐵) | 
| 67 | 1, 47, 3, 2, 66 | psrelbas 21954 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐹:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 68 | 67, 46 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ (Base‘𝑅)) | 
| 69 | 50 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐺:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑅)) | 
| 70 | 69, 46 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ (Base‘𝑅)) | 
| 71 |  | eqid 2737 | . . . . . . 7
⊢
(.g‘𝑅) = (.g‘𝑅) | 
| 72 | 47, 71, 34 | mulgnn0di 19843 | . . . . . 6
⊢ ((𝑅 ∈ CMnd ∧ (((𝑑‘𝑋) + 1) ∈ ℕ0 ∧
(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ (Base‘𝑅) ∧ (𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))) ∈ (Base‘𝑅))) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = ((((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))(+g‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 73 | 59, 65, 68, 70, 72 | syl13anc 1374 | . . . . 5
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))(+g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = ((((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))(+g‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 74 | 57, 73 | eqtr2d 2778 | . . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))(+g‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) = (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))) | 
| 75 | 74 | mpteq2dva 5242 | . . 3
⊢ (𝜑 → (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦
((((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐹‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0)))))(+g‘𝑅)(((𝑑‘𝑋) + 1)(.g‘𝑅)(𝐺‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) = (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 76 | 9, 33, 75 | 3eqtrd 2781 | . 2
⊢ (𝜑 → ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∘f
(+g‘𝑅)(((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺)) = (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 77 | 58 | cmnmndd 19822 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Mnd) | 
| 78 |  | mndmgm 18754 | . . . . 5
⊢ (𝑅 ∈ Mnd → 𝑅 ∈ Mgm) | 
| 79 | 77, 78 | syl 17 | . . . 4
⊢ (𝜑 → 𝑅 ∈ Mgm) | 
| 80 | 1, 2, 79, 4, 5 | psdcl 22165 | . . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∈ 𝐵) | 
| 81 | 1, 2, 79, 4, 7 | psdcl 22165 | . . 3
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺) ∈ 𝐵) | 
| 82 | 1, 2, 34, 35, 80, 81 | psradd 21957 | . 2
⊢ (𝜑 → ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) + (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺)) = ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) ∘f
(+g‘𝑅)(((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺))) | 
| 83 | 1, 2, 35, 79, 5, 7 | psraddcl 21958 | . . 3
⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) | 
| 84 | 1, 2, 3, 4, 83 | psdval 22163 | . 2
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐹 + 𝐺)) = (𝑑 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (((𝑑‘𝑋) + 1)(.g‘𝑅)((𝐹 + 𝐺)‘(𝑑 ∘f + (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑋, 1, 0))))))) | 
| 85 | 76, 82, 84 | 3eqtr4rd 2788 | 1
⊢ (𝜑 → (((𝐼 mPSDer 𝑅)‘𝑋)‘(𝐹 + 𝐺)) = ((((𝐼 mPSDer 𝑅)‘𝑋)‘𝐹) + (((𝐼 mPSDer 𝑅)‘𝑋)‘𝐺))) |