Metamath Proof Explorer

Theorem evlslem3

Description: Lemma for evlseu . Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem3.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
evlslem3.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlslem3.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
evlslem3.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
evlslem3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlslem3.t ⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
evlslem3.x ⊢ ↑ = ( .g ‘ 𝑇 )
evlslem3.m ⊢ · = ( .r ‘ 𝑆 )
evlslem3.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
evlslem3.e ⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
evlslem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
evlslem3.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evlslem3.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlslem3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
evlslem3.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
evlslem3.z ⊢ 0 = ( 0g ‘ 𝑅 )
evlslem3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
evlslem3.q ⊢ ( 𝜑 → 𝐻 ∈ 𝐾 )
Assertion evlslem3 ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 evlslem3.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 evlslem3.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 evlslem3.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
4 evlslem3.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 evlslem3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
6 evlslem3.t ⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
7 evlslem3.x ⊢ ↑ = ( .g ‘ 𝑇 )
8 evlslem3.m ⊢ · = ( .r ‘ 𝑆 )
9 evlslem3.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
10 evlslem3.e ⊢ 𝐸 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
11 evlslem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
12 evlslem3.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 evlslem3.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
14 evlslem3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
15 evlslem3.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
16 evlslem3.z ⊢ 0 = ( 0g ‘ 𝑅 )
17 evlslem3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
18 evlslem3.q ⊢ ( 𝜑 → 𝐻 ∈ 𝐾 )
19 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20 12 19 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
21 1 5 16 4 11 20 2 18 17 mplmon2cl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐵 )
22 fveq1 ⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑝 ‘ 𝑏 ) = ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) )
23 22 fveq2d ⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) )
24 23 oveq1d ⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
25 24 mpteq2dv ⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) )
26 25 oveq2d ⊢ ( 𝑝 = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( 𝑝 ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
27 ovex ⊢ ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) ∈ V
28 26 10 27 fvmpt ⊢ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
29 21 28 syl ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
30 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) )
31 eqeq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 = 𝐴 ↔ 𝑏 = 𝐴 ) )
32 31 ifbid ⊢ ( 𝑥 = 𝑏 → if ( 𝑥 = 𝐴 , 𝐻 , 0 ) = if ( 𝑏 = 𝐴 , 𝐻 , 0 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 )
34 16 fvexi ⊢ 0 ∈ V
35 34 a1i ⊢ ( 𝜑 → 0 ∈ V )
36 18 35 ifexd ⊢ ( 𝜑 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ V )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ V )
38 30 32 33 37 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) = if ( 𝑏 = 𝐴 , 𝐻 , 0 ) )
39 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) = ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) )
40 39 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
41 40 mpteq2dva ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) )
43 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
44 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
45 13 44 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
46 ringmnd ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Mnd )
47 45 46 syl ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
48 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
49 5 48 rabex2 ⊢ 𝐷 ∈ V
50 49 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
51 45 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring )
52 4 3 rhmf ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝐾 ⟶ 𝐶 )
53 14 52 syl ⊢ ( 𝜑 → 𝐹 : 𝐾 ⟶ 𝐶 )
54 4 16 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
55 20 54 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
56 18 55 ifcld ⊢ ( 𝜑 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ∈ 𝐾 )
57 53 56 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 )
59 6 3 mgpbas ⊢ 𝐶 = ( Base ‘ 𝑇 )
60 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
61 6 crngmgp ⊢ ( 𝑆 ∈ CRing → 𝑇 ∈ CMnd )
62 13 61 syl ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑇 ∈ CMnd )
64 11 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
65 cmnmnd ⊢ ( 𝑇 ∈ CMnd → 𝑇 ∈ Mnd )
66 62 65 syl ⊢ ( 𝜑 → 𝑇 ∈ Mnd )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑇 ∈ Mnd )
68 simprl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑦 ∈ ℕ0 )
69 simprr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑧 ∈ 𝐶 )
70 59 7 mulgnn0cl ⊢ ( ( 𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 ↑ 𝑧 ) ∈ 𝐶 )
71 67 68 69 70 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 ↑ 𝑧 ) ∈ 𝐶 )
72 5 psrbagf ⊢ ( 𝑏 ∈ 𝐷 → 𝑏 : 𝐼 ⟶ ℕ0 )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 : 𝐼 ⟶ ℕ0 )
74 15 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ 𝐶 )
75 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
76 71 73 74 64 64 75 off ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) : 𝐼 ⟶ 𝐶 )
77 ovex ⊢ ( 𝑏 ∘f ↑ 𝐺 ) ∈ V
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) ∈ V )
79 76 ffund ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → Fun ( 𝑏 ∘f ↑ 𝐺 ) )
80 fvexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 0g ‘ 𝑇 ) ∈ V )
81 5 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) )
82 11 81 syl ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) )
83 82 simplbda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ◡ 𝑏 “ ℕ ) ∈ Fin )
84 73 ffnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 Fn 𝐼 )
85 84 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑏 Fn 𝐼 )
86 15 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
87 86 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐺 Fn 𝐼 )
88 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐼 ∈ 𝑊 )
89 eldifi ⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → 𝑦 ∈ 𝐼 )
90 89 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑦 ∈ 𝐼 )
91 fnfvof ⊢ ( ( ( 𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑊 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) )
92 85 87 88 90 91 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) )
93 ffvelrn ⊢ ( ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 )
94 73 89 93 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 )
95 elnn0 ⊢ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 ↔ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) )
96 94 95 sylib ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) )
97 eldifn ⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
98 97 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
99 84 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑏 Fn 𝐼 )
100 89 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ 𝐼 )
101 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ )
102 99 100 101 elpreimad ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
103 98 102 mtand ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ ( 𝑏 ‘ 𝑦 ) ∈ ℕ )
104 96 103 orcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) = 0 )
105 104 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) )
106 ffvelrn ⊢ ( ( 𝐺 : 𝐼 ⟶ 𝐶 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 )
107 74 89 106 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 )
108 59 60 7 mulg0 ⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) )
109 107 108 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) )
110 92 105 109 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) )
111 76 110 suppss ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) )
112 suppssfifsupp ⊢ ( ( ( ( 𝑏 ∘f ↑ 𝐺 ) ∈ V ∧ Fun ( 𝑏 ∘f ↑ 𝐺 ) ∧ ( 0g ‘ 𝑇 ) ∈ V ) ∧ ( ( ◡ 𝑏 “ ℕ ) ∈ Fin ∧ ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
113 78 79 80 83 111 112 syl32anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
114 59 60 63 64 76 113 gsumcl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
115 3 8 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
116 51 58 114 115 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
117 116 fmpttd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 )
118 eldifsnneq ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → ¬ 𝑏 = 𝐴 )
119 118 iffalsed ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 )
120 119 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 )
121 120 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 0 ) )
122 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
123 14 122 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
124 16 43 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
125 123 124 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
127 121 126 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 0g ‘ 𝑆 ) )
128 127 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
129 45 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → 𝑆 ∈ Ring )
130 eldifi ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → 𝑏 ∈ 𝐷 )
131 130 114 sylan2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
132 3 8 43 ringlz ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
133 129 131 132 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
134 128 133 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
135 134 50 suppss2 ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ { 𝐴 } )
136 3 43 47 50 17 117 135 gsumpt ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) )
137 42 136 eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) )
138 iftrue ⊢ ( 𝑏 = 𝐴 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 𝐻 )
139 138 fveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 𝐻 ) )
140 oveq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 ∘f ↑ 𝐺 ) = ( 𝐴 ∘f ↑ 𝐺 ) )
141 140 oveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) = ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) )
142 139 141 oveq12d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
143 eqid ⊢ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
144 ovex ⊢ ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ∈ V
145 142 143 144 fvmpt ⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
146 17 145 syl ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
147 29 137 146 3eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )