| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | psrring.s | . . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) | 
| 2 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 3 |  | psr1cl.d | . . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 4 |  | psr1cl.b | . . . 4
⊢ 𝐵 = (Base‘𝑆) | 
| 5 |  | psrlidm.t | . . . . 5
⊢  · =
(.r‘𝑆) | 
| 6 |  | psrring.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 7 |  | psrlidm.x | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 8 |  | psrring.i | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 9 |  | psr1cl.z | . . . . . 6
⊢  0 =
(0g‘𝑅) | 
| 10 |  | psr1cl.o | . . . . . 6
⊢  1 =
(1r‘𝑅) | 
| 11 |  | psr1cl.u | . . . . . 6
⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 )) | 
| 12 | 1, 8, 6, 3, 9, 10,
11, 4 | psr1cl 21981 | . . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐵) | 
| 13 | 1, 4, 5, 6, 7, 12 | psrmulcl 21966 | . . . 4
⊢ (𝜑 → (𝑋 · 𝑈) ∈ 𝐵) | 
| 14 | 1, 2, 3, 4, 13 | psrelbas 21954 | . . 3
⊢ (𝜑 → (𝑋 · 𝑈):𝐷⟶(Base‘𝑅)) | 
| 15 | 14 | ffnd 6737 | . 2
⊢ (𝜑 → (𝑋 · 𝑈) Fn 𝐷) | 
| 16 | 1, 2, 3, 4, 7 | psrelbas 21954 | . . 3
⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) | 
| 17 | 16 | ffnd 6737 | . 2
⊢ (𝜑 → 𝑋 Fn 𝐷) | 
| 18 |  | eqid 2737 | . . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 19 | 7 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑋 ∈ 𝐵) | 
| 20 | 12 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈 ∈ 𝐵) | 
| 21 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ 𝐷) | 
| 22 | 1, 4, 18, 5, 3, 19, 20, 21 | psrmulval 21964 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))))) | 
| 23 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑔 = 𝑦 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑦 ∘r ≤ 𝑦)) | 
| 24 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐼 ∈ 𝑉) | 
| 25 | 3 | psrbagf 21938 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝐷 → 𝑦:𝐼⟶ℕ0) | 
| 26 | 25 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℕ0) | 
| 27 |  | nn0re 12535 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℝ) | 
| 28 | 27 | leidd 11829 | . . . . . . . . . 10
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ≤ 𝑧) | 
| 29 | 28 | adantl 481 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ℕ0) → 𝑧 ≤ 𝑧) | 
| 30 | 24, 26, 29 | caofref 7728 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∘r ≤ 𝑦) | 
| 31 | 23, 21, 30 | elrabd 3694 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) | 
| 32 | 31 | snssd 4809 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ⊆ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) | 
| 33 | 32 | resmptd 6058 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) | 
| 34 | 33 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))))) | 
| 35 |  | ringcmn 20279 | . . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) | 
| 36 | 6, 35 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) | 
| 37 | 36 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ CMnd) | 
| 38 |  | ovex 7464 | . . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 39 | 3, 38 | rab2ex 5342 | . . . . . 6
⊢ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V | 
| 40 | 39 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∈ V) | 
| 41 | 6 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑅 ∈ Ring) | 
| 42 | 16 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑋:𝐷⟶(Base‘𝑅)) | 
| 43 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) | 
| 44 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑔 = 𝑧 → (𝑔 ∘r ≤ 𝑦 ↔ 𝑧 ∘r ≤ 𝑦)) | 
| 45 | 44 | elrab 3692 | . . . . . . . . . 10
⊢ (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↔ (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦)) | 
| 46 | 43, 45 | sylib 218 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑧 ∈ 𝐷 ∧ 𝑧 ∘r ≤ 𝑦)) | 
| 47 | 46 | simpld 494 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∈ 𝐷) | 
| 48 | 42, 47 | ffvelcdmd 7105 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑋‘𝑧) ∈ (Base‘𝑅)) | 
| 49 | 1, 2, 3, 4, 20 | psrelbas 21954 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑈:𝐷⟶(Base‘𝑅)) | 
| 50 | 49 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑈:𝐷⟶(Base‘𝑅)) | 
| 51 | 21 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦 ∈ 𝐷) | 
| 52 | 3 | psrbagf 21938 | . . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0) | 
| 53 | 47, 52 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℕ0) | 
| 54 | 46 | simprd 495 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧 ∘r ≤ 𝑦) | 
| 55 | 3 | psrbagcon 21945 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐷 ∧ 𝑧:𝐼⟶ℕ0 ∧ 𝑧 ∘r ≤ 𝑦) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦)) | 
| 56 | 51, 53, 54, 55 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) ∈ 𝐷 ∧ (𝑦 ∘f − 𝑧) ∘r ≤ 𝑦)) | 
| 57 | 56 | simpld 494 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑦 ∘f − 𝑧) ∈ 𝐷) | 
| 58 | 50, 57 | ffvelcdmd 7105 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → (𝑈‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) | 
| 59 | 2, 18 | ringcl 20247 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅) ∧ (𝑈‘(𝑦 ∘f − 𝑧)) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅)) | 
| 60 | 41, 48, 58, 59 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) ∈ (Base‘𝑅)) | 
| 61 | 60 | fmpttd 7135 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))):{𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}⟶(Base‘𝑅)) | 
| 62 |  | eldifi 4131 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦}) → 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) | 
| 63 | 62, 57 | sylan2 593 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑦 ∘f − 𝑧) ∈ 𝐷) | 
| 64 |  | eqeq1 2741 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 ∘f − 𝑧) → (𝑥 = (𝐼 × {0}) ↔ (𝑦 ∘f − 𝑧) = (𝐼 × {0}))) | 
| 65 | 64 | ifbid 4549 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∘f − 𝑧) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 )) | 
| 66 | 10 | fvexi 6920 | . . . . . . . . . . . 12
⊢  1 ∈
V | 
| 67 | 9 | fvexi 6920 | . . . . . . . . . . . 12
⊢  0 ∈
V | 
| 68 | 66, 67 | ifex 4576 | . . . . . . . . . . 11
⊢ if((𝑦 ∘f −
𝑧) = (𝐼 × {0}), 1 , 0 ) ∈
V | 
| 69 | 65, 11, 68 | fvmpt 7016 | . . . . . . . . . 10
⊢ ((𝑦 ∘f −
𝑧) ∈ 𝐷 → (𝑈‘(𝑦 ∘f − 𝑧)) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 )) | 
| 70 | 63, 69 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘f − 𝑧)) = if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 )) | 
| 71 |  | eldifsni 4790 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦}) → 𝑧 ≠ 𝑦) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → 𝑧 ≠ 𝑦) | 
| 73 | 72 | necomd 2996 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → 𝑦 ≠ 𝑧) | 
| 74 | 24 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝐼 ∈ 𝑉) | 
| 75 |  | nn0sscn 12531 | . . . . . . . . . . . . . . . 16
⊢
ℕ0 ⊆ ℂ | 
| 76 |  | fss 6752 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦:𝐼⟶ℕ0 ∧
ℕ0 ⊆ ℂ) → 𝑦:𝐼⟶ℂ) | 
| 77 | 26, 75, 76 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑦:𝐼⟶ℂ) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑦:𝐼⟶ℂ) | 
| 79 |  | fss 6752 | . . . . . . . . . . . . . . 15
⊢ ((𝑧:𝐼⟶ℕ0 ∧
ℕ0 ⊆ ℂ) → 𝑧:𝐼⟶ℂ) | 
| 80 | 53, 75, 79 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → 𝑧:𝐼⟶ℂ) | 
| 81 |  | ofsubeq0 12263 | . . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑧:𝐼⟶ℂ) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧)) | 
| 82 | 74, 78, 80, 81 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧)) | 
| 83 | 62, 82 | sylan2 593 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 = 𝑧)) | 
| 84 | 83 | necon3bbid 2978 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (¬ (𝑦 ∘f − 𝑧) = (𝐼 × {0}) ↔ 𝑦 ≠ 𝑧)) | 
| 85 | 73, 84 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ¬ (𝑦 ∘f − 𝑧) = (𝐼 × {0})) | 
| 86 | 85 | iffalsed 4536 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → if((𝑦 ∘f − 𝑧) = (𝐼 × {0}), 1 , 0 ) = 0 ) | 
| 87 | 70, 86 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → (𝑈‘(𝑦 ∘f − 𝑧)) = 0 ) | 
| 88 | 87 | oveq2d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = ((𝑋‘𝑧)(.r‘𝑅) 0 )) | 
| 89 | 2, 18, 9 | ringrz 20291 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 90 | 41, 48, 89 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦}) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 91 | 62, 90 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅) 0 ) = 0 ) | 
| 92 | 88, 91 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 ∈ ({𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ∖ {𝑦})) → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = 0 ) | 
| 93 | 92, 40 | suppss2 8225 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {𝑦}) | 
| 94 | 40 | mptexd 7244 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∈ V) | 
| 95 |  | funmpt 6604 | . . . . . . 7
⊢ Fun
(𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) | 
| 96 | 95 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) | 
| 97 | 67 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 0 ∈ V) | 
| 98 |  | snfi 9083 | . . . . . . 7
⊢ {𝑦} ∈ Fin | 
| 99 | 98 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → {𝑦} ∈ Fin) | 
| 100 |  | suppssfifsupp 9420 | . . . . . 6
⊢ ((((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∈ V ∧ Fun (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ∧ 0 ∈ V) ∧ ({𝑦} ∈ Fin ∧ ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) supp 0 ) ⊆ {𝑦})) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) finSupp 0 ) | 
| 101 | 94, 96, 97, 99, 93, 100 | syl32anc 1380 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) finSupp 0 ) | 
| 102 | 2, 9, 37, 40, 61, 93, 101 | gsumres 19931 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg ((𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))) ↾ {𝑦})) = (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧)))))) | 
| 103 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Ring) | 
| 104 |  | ringmnd 20240 | . . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 105 | 103, 104 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Mnd) | 
| 106 |  | eqid 2737 | . . . . . . . . . . 11
⊢ 𝑦 = 𝑦 | 
| 107 |  | ofsubeq0 12263 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑦:𝐼⟶ℂ ∧ 𝑦:𝐼⟶ℂ) → ((𝑦 ∘f − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦)) | 
| 108 | 24, 77, 77, 107 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑦 ∘f − 𝑦) = (𝐼 × {0}) ↔ 𝑦 = 𝑦)) | 
| 109 | 106, 108 | mpbiri 258 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑦 ∘f − 𝑦) = (𝐼 × {0})) | 
| 110 | 109 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘f − 𝑦)) = (𝑈‘(𝐼 × {0}))) | 
| 111 |  | fconstmpt 5747 | . . . . . . . . . . . 12
⊢ (𝐼 × {0}) = (𝑤 ∈ 𝐼 ↦ 0) | 
| 112 | 3 | fczpsrbag 21941 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈ 𝑉 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷) | 
| 113 | 8, 112 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ 𝐼 ↦ 0) ∈ 𝐷) | 
| 114 | 111, 113 | eqeltrid 2845 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷) | 
| 115 | 114 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐼 × {0}) ∈ 𝐷) | 
| 116 |  | iftrue 4531 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐼 × {0}) → if(𝑥 = (𝐼 × {0}), 1 , 0 ) = 1 ) | 
| 117 | 116, 11, 66 | fvmpt 7016 | . . . . . . . . . 10
⊢ ((𝐼 × {0}) ∈ 𝐷 → (𝑈‘(𝐼 × {0})) = 1 ) | 
| 118 | 115, 117 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝐼 × {0})) = 1 ) | 
| 119 | 110, 118 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑈‘(𝑦 ∘f − 𝑦)) = 1 ) | 
| 120 | 119 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) = ((𝑋‘𝑦)(.r‘𝑅) 1 )) | 
| 121 | 16 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅)) | 
| 122 | 2, 18, 10 | ringridm 20267 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑦) ∈ (Base‘𝑅)) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦)) | 
| 123 | 103, 121,
122 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅) 1 ) = (𝑋‘𝑦)) | 
| 124 | 120, 123 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) = (𝑋‘𝑦)) | 
| 125 | 124, 121 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) ∈ (Base‘𝑅)) | 
| 126 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑋‘𝑧) = (𝑋‘𝑦)) | 
| 127 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑦 ∘f − 𝑧) = (𝑦 ∘f − 𝑦)) | 
| 128 | 127 | fveq2d 6910 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑈‘(𝑦 ∘f − 𝑧)) = (𝑈‘(𝑦 ∘f − 𝑦))) | 
| 129 | 126, 128 | oveq12d 7449 | . . . . . 6
⊢ (𝑧 = 𝑦 → ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦)))) | 
| 130 | 2, 129 | gsumsn 19972 | . . . . 5
⊢ ((𝑅 ∈ Mnd ∧ 𝑦 ∈ 𝐷 ∧ ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦)))) | 
| 131 | 105, 21, 125, 130 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦)))) | 
| 132 | 34, 102, 131 | 3eqtr3d 2785 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝑅 Σg (𝑧 ∈ {𝑔 ∈ 𝐷 ∣ 𝑔 ∘r ≤ 𝑦} ↦ ((𝑋‘𝑧)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑧))))) = ((𝑋‘𝑦)(.r‘𝑅)(𝑈‘(𝑦 ∘f − 𝑦)))) | 
| 133 | 22, 132, 124 | 3eqtrd 2781 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝑋 · 𝑈)‘𝑦) = (𝑋‘𝑦)) | 
| 134 | 15, 17, 133 | eqfnfvd 7054 | 1
⊢ (𝜑 → (𝑋 · 𝑈) = 𝑋) |