| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evlslem3.p | . . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 2 |  | evlslem3.d | . . . 4
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 3 |  | evlslem3.z | . . . 4
⊢  0 =
(0g‘𝑅) | 
| 4 |  | evlslem3.k | . . . 4
⊢ 𝐾 = (Base‘𝑅) | 
| 5 |  | evlslem3.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 6 |  | evlslem3.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 7 |  | crngring 20242 | . . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 8 | 6, 7 | syl 17 | . . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 9 |  | evlslem3.b | . . . 4
⊢ 𝐵 = (Base‘𝑃) | 
| 10 |  | evlslem3.q | . . . 4
⊢ (𝜑 → 𝐻 ∈ 𝐾) | 
| 11 |  | evlslem3.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐷) | 
| 12 | 1, 2, 3, 4, 5, 8, 9, 10, 11 | mplmon2cl 22092 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵) | 
| 13 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑝‘𝑏) = ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) | 
| 14 | 13 | fveq2d 6910 | . . . . . . 7
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏))) | 
| 15 | 14 | oveq1d 7446 | . . . . . 6
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 16 | 15 | mpteq2dv 5244 | . . . . 5
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 17 | 16 | oveq2d 7447 | . . . 4
⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 18 |  | evlslem3.e | . . . 4
⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 19 |  | ovex 7464 | . . . 4
⊢ (𝑆 Σg
(𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V | 
| 20 | 17, 18, 19 | fvmpt 7016 | . . 3
⊢ ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 21 | 12, 20 | syl 17 | . 2
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 22 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) | 
| 23 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴)) | 
| 24 | 23 | ifbid 4549 | . . . . . . . 8
⊢ (𝑥 = 𝑏 → if(𝑥 = 𝐴, 𝐻, 0 ) = if(𝑏 = 𝐴, 𝐻, 0 )) | 
| 25 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷) | 
| 26 | 3 | fvexi 6920 | . . . . . . . . . . 11
⊢  0 ∈
V | 
| 27 | 26 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈ V) | 
| 28 | 10, 27 | ifexd 4574 | . . . . . . . . 9
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) | 
| 29 | 28 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈
V) | 
| 30 | 22, 24, 25, 29 | fvmptd3 7039 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 )) | 
| 31 | 30 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) = (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 ))) | 
| 32 | 31 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 33 | 32 | mpteq2dva 5242 | . . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) | 
| 34 | 33 | oveq2d 7447 | . . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) | 
| 35 |  | evlslem3.c | . . . 4
⊢ 𝐶 = (Base‘𝑆) | 
| 36 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 37 |  | evlslem3.s | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 38 |  | crngring 20242 | . . . . . 6
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) | 
| 39 | 37, 38 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 40 |  | ringmnd 20240 | . . . . 5
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Mnd) | 
| 41 | 39, 40 | syl 17 | . . . 4
⊢ (𝜑 → 𝑆 ∈ Mnd) | 
| 42 |  | ovex 7464 | . . . . . 6
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 43 | 2, 42 | rabex2 5341 | . . . . 5
⊢ 𝐷 ∈ V | 
| 44 | 43 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐷 ∈ V) | 
| 45 | 39 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring) | 
| 46 |  | evlslem3.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) | 
| 47 | 4, 35 | rhmf 20485 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶) | 
| 48 | 46, 47 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝐾⟶𝐶) | 
| 49 | 4, 3 | ring0cl 20264 | . . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾) | 
| 50 | 8, 49 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 0 ∈ 𝐾) | 
| 51 | 10, 50 | ifcld 4572 | . . . . . . . 8
⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ 𝐾) | 
| 52 | 48, 51 | ffvelcdmd 7105 | . . . . . . 7
⊢ (𝜑 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) | 
| 53 | 52 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶) | 
| 54 |  | evlslem3.t | . . . . . . . 8
⊢ 𝑇 = (mulGrp‘𝑆) | 
| 55 | 54, 35 | mgpbas 20142 | . . . . . . 7
⊢ 𝐶 = (Base‘𝑇) | 
| 56 |  | eqid 2737 | . . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) | 
| 57 | 54 | crngmgp 20238 | . . . . . . . . 9
⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd) | 
| 58 | 37, 57 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ CMnd) | 
| 59 | 58 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd) | 
| 60 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ 𝑊) | 
| 61 |  | evlslem3.x | . . . . . . . . 9
⊢  ↑ =
(.g‘𝑇) | 
| 62 |  | cmnmnd 19815 | . . . . . . . . . . 11
⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd) | 
| 63 | 58, 62 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ Mnd) | 
| 64 | 63 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑇 ∈ Mnd) | 
| 65 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ ℕ0) | 
| 66 |  | simprr 773 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) | 
| 67 | 55, 61, 64, 65, 66 | mulgnn0cld 19113 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → (𝑦 ↑ 𝑧) ∈ 𝐶) | 
| 68 | 2 | psrbagf 21938 | . . . . . . . . 9
⊢ (𝑏 ∈ 𝐷 → 𝑏:𝐼⟶ℕ0) | 
| 69 | 68 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) | 
| 70 |  | evlslem3.g | . . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) | 
| 71 | 70 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶) | 
| 72 |  | inidm 4227 | . . . . . . . 8
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 73 | 67, 69, 71, 60, 60, 72 | off 7715 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺):𝐼⟶𝐶) | 
| 74 |  | ovex 7464 | . . . . . . . . 9
⊢ (𝑏 ∘f ↑ 𝐺) ∈ V | 
| 75 | 74 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺) ∈ V) | 
| 76 | 73 | ffund 6740 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑏 ∘f ↑ 𝐺)) | 
| 77 |  | fvexd 6921 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (0g‘𝑇) ∈ V) | 
| 78 | 2 | psrbag 21937 | . . . . . . . . . 10
⊢ (𝐼 ∈ 𝑊 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) | 
| 79 | 5, 78 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈
Fin))) | 
| 80 | 79 | simplbda 499 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (◡𝑏 “ ℕ) ∈
Fin) | 
| 81 | 69 | ffnd 6737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑏 Fn 𝐼) | 
| 83 | 70 | ffnd 6737 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 Fn 𝐼) | 
| 84 | 83 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐺 Fn 𝐼) | 
| 85 | 5 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐼 ∈ 𝑊) | 
| 86 |  | eldifi 4131 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → 𝑦 ∈ 𝐼) | 
| 87 | 86 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑦 ∈ 𝐼) | 
| 88 |  | fnfvof 7714 | . . . . . . . . . . 11
⊢ (((𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼) ∧ (𝐼 ∈ 𝑊 ∧ 𝑦 ∈ 𝐼)) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) | 
| 89 | 82, 84, 85, 87, 88 | syl22anc 839 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦))) | 
| 90 |  | ffvelcdm 7101 | . . . . . . . . . . . . . 14
⊢ ((𝑏:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈
ℕ0) | 
| 91 | 69, 86, 90 | syl2an 596 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) ∈
ℕ0) | 
| 92 |  | elnn0 12528 | . . . . . . . . . . . . 13
⊢ ((𝑏‘𝑦) ∈ ℕ0 ↔ ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) | 
| 93 | 91, 92 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0)) | 
| 94 |  | eldifn 4132 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) | 
| 95 | 94 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ)) | 
| 96 | 81 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑏 Fn 𝐼) | 
| 97 | 86 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ 𝐼) | 
| 98 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑏‘𝑦) ∈ ℕ) | 
| 99 | 96, 97, 98 | elpreimad 7079 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ (◡𝑏 “ ℕ)) | 
| 100 | 95, 99 | mtand 816 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ (𝑏‘𝑦) ∈ ℕ) | 
| 101 | 93, 100 | orcnd 879 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) = 0) | 
| 102 | 101 | oveq1d 7446 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ↑ (𝐺‘𝑦)) = (0 ↑ (𝐺‘𝑦))) | 
| 103 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝐺:𝐼⟶𝐶 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ 𝐶) | 
| 104 | 71, 86, 103 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝐺‘𝑦) ∈ 𝐶) | 
| 105 | 55, 56, 61 | mulg0 19092 | . . . . . . . . . . 11
⊢ ((𝐺‘𝑦) ∈ 𝐶 → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇)) | 
| 107 | 89, 102, 106 | 3eqtrd 2781 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘f ↑ 𝐺)‘𝑦) = (0g‘𝑇)) | 
| 108 | 73, 107 | suppss 8219 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑏 ∘f ↑ 𝐺) supp (0g‘𝑇)) ⊆ (◡𝑏 “ ℕ)) | 
| 109 |  | suppssfifsupp 9420 | . . . . . . . 8
⊢ ((((𝑏 ∘f ↑ 𝐺) ∈ V ∧ Fun (𝑏 ∘f ↑ 𝐺) ∧
(0g‘𝑇)
∈ V) ∧ ((◡𝑏 “ ℕ) ∈ Fin ∧ ((𝑏 ∘f ↑ 𝐺) supp
(0g‘𝑇))
⊆ (◡𝑏 “ ℕ))) → (𝑏 ∘f ↑ 𝐺) finSupp
(0g‘𝑇)) | 
| 110 | 75, 76, 77, 80, 108, 109 | syl32anc 1380 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f ↑ 𝐺) finSupp (0g‘𝑇)) | 
| 111 | 55, 56, 59, 60, 73, 110 | gsumcl 19933 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 112 |  | evlslem3.m | . . . . . . 7
⊢  · =
(.r‘𝑆) | 
| 113 | 35, 112 | ringcl 20247 | . . . . . 6
⊢ ((𝑆 ∈ Ring ∧ (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ 𝐶) | 
| 114 | 45, 53, 111, 113 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ 𝐶) | 
| 115 | 114 | fmpttd 7135 | . . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶) | 
| 116 |  | eldifsnneq 4791 | . . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → ¬ 𝑏 = 𝐴) | 
| 117 | 116 | iffalsed 4536 | . . . . . . . . . 10
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) | 
| 118 | 117 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 ) | 
| 119 | 118 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘ 0 )) | 
| 120 |  | rhmghm 20484 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | 
| 121 | 46, 120 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | 
| 122 | 3, 36 | ghmid 19240 | . . . . . . . . . 10
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘ 0 ) =
(0g‘𝑆)) | 
| 123 | 121, 122 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑆)) | 
| 124 | 123 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘ 0 ) =
(0g‘𝑆)) | 
| 125 | 119, 124 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) =
(0g‘𝑆)) | 
| 126 | 125 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) =
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 127 | 39 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → 𝑆 ∈ Ring) | 
| 128 |  | eldifi 4131 | . . . . . . . 8
⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ∈ 𝐷) | 
| 129 | 128, 111 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶) | 
| 130 | 35, 112, 36 | ringlz 20290 | . . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ (𝑇 Σg
(𝑏 ∘f
↑
𝐺)) ∈ 𝐶) →
((0g‘𝑆)
·
(𝑇
Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) | 
| 131 | 127, 129,
130 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) | 
| 132 | 126, 131 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (0g‘𝑆)) | 
| 133 | 132, 44 | suppss2 8225 | . . . 4
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) supp
(0g‘𝑆))
⊆ {𝐴}) | 
| 134 | 35, 36, 41, 44, 11, 115, 133 | gsumpt 19980 | . . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴)) | 
| 135 | 34, 134 | eqtrd 2777 | . 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴)) | 
| 136 |  | iftrue 4531 | . . . . . 6
⊢ (𝑏 = 𝐴 → if(𝑏 = 𝐴, 𝐻, 0 ) = 𝐻) | 
| 137 | 136 | fveq2d 6910 | . . . . 5
⊢ (𝑏 = 𝐴 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘𝐻)) | 
| 138 |  | oveq1 7438 | . . . . . 6
⊢ (𝑏 = 𝐴 → (𝑏 ∘f ↑ 𝐺) = (𝐴 ∘f ↑ 𝐺)) | 
| 139 | 138 | oveq2d 7447 | . . . . 5
⊢ (𝑏 = 𝐴 → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) = (𝑇 Σg (𝐴 ∘f ↑ 𝐺))) | 
| 140 | 137, 139 | oveq12d 7449 | . . . 4
⊢ (𝑏 = 𝐴 → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) | 
| 141 |  | eqid 2737 | . . . 4
⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) | 
| 142 |  | ovex 7464 | . . . 4
⊢ ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺))) ∈ V | 
| 143 | 140, 141,
142 | fvmpt 7016 | . . 3
⊢ (𝐴 ∈ 𝐷 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) | 
| 144 | 11, 143 | syl 17 | . 2
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) | 
| 145 | 21, 135, 144 | 3eqtrd 2781 | 1
⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘f ↑ 𝐺)))) |