This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 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 67 68 69 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 ↑ 𝑧 ) ∈ 𝐶 )
71 5 psrbagf ⊢ ( 𝑏 ∈ 𝐷 → 𝑏 : 𝐼 ⟶ ℕ0 )
72 71 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 : 𝐼 ⟶ ℕ0 )
73 15 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐺 : 𝐼 ⟶ 𝐶 )
74 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
75 70 72 73 64 64 74 off ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) : 𝐼 ⟶ 𝐶 )
76 ovex ⊢ ( 𝑏 ∘f ↑ 𝐺 ) ∈ V
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) ∈ V )
78 75 ffund ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → Fun ( 𝑏 ∘f ↑ 𝐺 ) )
79 fvexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 0g ‘ 𝑇 ) ∈ V )
80 5 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) )
81 11 80 syl ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↔ ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑏 “ ℕ ) ∈ Fin ) ) )
82 81 simplbda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ◡ 𝑏 “ ℕ ) ∈ Fin )
83 72 ffnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 Fn 𝐼 )
84 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑏 Fn 𝐼 )
85 15 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
86 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐺 Fn 𝐼 )
87 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝐼 ∈ 𝑊 )
88 eldifi ⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → 𝑦 ∈ 𝐼 )
89 88 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → 𝑦 ∈ 𝐼 )
90 fnfvof ⊢ ( ( ( 𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑊 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) )
91 84 86 87 89 90 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) )
92 ffvelcdm ⊢ ( ( 𝑏 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 )
93 72 88 92 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 )
94 elnn0 ⊢ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ0 ↔ ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) )
95 93 94 sylib ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ∈ ℕ ∨ ( 𝑏 ‘ 𝑦 ) = 0 ) )
96 eldifn ⊢ ( 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
97 96 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
98 83 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑏 Fn 𝐼 )
99 88 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ 𝐼 )
100 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → ( 𝑏 ‘ 𝑦 ) ∈ ℕ )
101 98 99 100 elpreimad ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ℕ ) → 𝑦 ∈ ( ◡ 𝑏 “ ℕ ) )
102 97 101 mtand ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ¬ ( 𝑏 ‘ 𝑦 ) ∈ ℕ )
103 95 102 orcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ‘ 𝑦 ) = 0 )
104 103 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ‘ 𝑦 ) ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) )
105 ffvelcdm ⊢ ( ( 𝐺 : 𝐼 ⟶ 𝐶 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 )
106 73 88 105 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 )
107 59 60 7 mulg0 ⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐶 → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) )
108 106 107 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( 0 ↑ ( 𝐺 ‘ 𝑦 ) ) = ( 0g ‘ 𝑇 ) )
109 91 104 108 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐼 ∖ ( ◡ 𝑏 “ ℕ ) ) ) → ( ( 𝑏 ∘f ↑ 𝐺 ) ‘ 𝑦 ) = ( 0g ‘ 𝑇 ) )
110 75 109 suppss ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) )
111 suppssfifsupp ⊢ ( ( ( ( 𝑏 ∘f ↑ 𝐺 ) ∈ V ∧ Fun ( 𝑏 ∘f ↑ 𝐺 ) ∧ ( 0g ‘ 𝑇 ) ∈ V ) ∧ ( ( ◡ 𝑏 “ ℕ ) ∈ Fin ∧ ( ( 𝑏 ∘f ↑ 𝐺 ) supp ( 0g ‘ 𝑇 ) ) ⊆ ( ◡ 𝑏 “ ℕ ) ) ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
112 77 78 79 82 110 111 syl32anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑏 ∘f ↑ 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
113 59 60 63 64 75 112 gsumcl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
114 3 8 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) ∈ 𝐶 ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
115 51 58 113 114 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ∈ 𝐶 )
116 115 fmpttd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) : 𝐷 ⟶ 𝐶 )
117 eldifsnneq ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → ¬ 𝑏 = 𝐴 )
118 117 iffalsed ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 )
119 118 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 0 )
120 119 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 0 ) )
121 rhmghm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
122 14 121 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
123 16 43 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
124 122 123 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑆 ) )
126 120 125 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 0g ‘ 𝑆 ) )
127 126 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
128 45 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → 𝑆 ∈ Ring )
129 eldifi ⊢ ( 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) → 𝑏 ∈ 𝐷 )
130 129 113 sylan2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 )
131 3 8 43 ringlz ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ∈ 𝐶 ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
132 128 130 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
133 127 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ { 𝐴 } ) ) → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( 0g ‘ 𝑆 ) )
134 133 50 suppss2 ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ { 𝐴 } )
135 3 43 47 50 17 116 134 gsumpt ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) )
136 42 135 eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ ( ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ‘ 𝑏 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ) = ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) )
137 iftrue ⊢ ( 𝑏 = 𝐴 → if ( 𝑏 = 𝐴 , 𝐻 , 0 ) = 𝐻 )
138 137 fveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) = ( 𝐹 ‘ 𝐻 ) )
139 oveq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 ∘f ↑ 𝐺 ) = ( 𝐴 ∘f ↑ 𝐺 ) )
140 139 oveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) = ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) )
141 138 140 oveq12d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
142 eqid ⊢ ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) )
143 ovex ⊢ ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) ∈ V
144 141 142 143 fvmpt ⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
145 17 144 syl ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ if ( 𝑏 = 𝐴 , 𝐻 , 0 ) ) · ( 𝑇 Σg ( 𝑏 ∘f ↑ 𝐺 ) ) ) ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )
146 29 136 145 3eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 = 𝐴 , 𝐻 , 0 ) ) ) = ( ( 𝐹 ‘ 𝐻 ) · ( 𝑇 Σg ( 𝐴 ∘f ↑ 𝐺 ) ) ) )