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 ↑ 𝐺 ) ) ) )