Theorem evlslem3 19875

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

Hypotheses

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

Assertion

Ref	Expression
evlslem3	⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))

Distinct variable groups:   𝑝,𝑏,𝑥, 0   𝐵,𝑝   𝐶,𝑏   𝐷,𝑏,𝑝,𝑥   𝐹,𝑏,𝑝   ↑ ,𝑏,𝑝   ℎ,𝑏,𝐴,𝑝,𝑥   ℎ,𝐼   𝑥,𝐾   𝜑,𝑏,𝑥   𝐺,𝑏,𝑝   𝐻,𝑏,𝑝,𝑥   𝑆,𝑏,𝑝   𝑇,𝑏,𝑝   · ,𝑏,𝑝   𝑥,𝑅

Allowed substitution hints:   𝜑(ℎ,𝑝)   𝐵(𝑥,ℎ,𝑏)   𝐶(𝑥,ℎ,𝑝)   𝐷(ℎ)   𝑃(𝑥,ℎ,𝑝,𝑏)   𝑅(ℎ,𝑝,𝑏)   𝑆(𝑥,ℎ)   𝑇(𝑥,ℎ)   · (𝑥,ℎ)   𝐸(𝑥,ℎ,𝑝,𝑏)   ↑ (𝑥,ℎ)   𝐹(𝑥,ℎ)   𝐺(𝑥,ℎ)   𝐻(ℎ)   𝐼(𝑥,𝑝,𝑏)   𝐾(ℎ,𝑝,𝑏)   𝑉(𝑥,ℎ,𝑝,𝑏)   0 (ℎ)

Proof of Theorem evlslem3

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlslem1.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		evlslem1.d	. . . 4 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
3		evlslem3.z	. . . 4 ⊢ 0 = (0g‘𝑅)
4		evlslem1.k	. . . 4 ⊢ 𝐾 = (Base‘𝑅)
5		evlslem1.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
6		evlslem1.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
7		crngring 18913	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
9		evlslem1.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
10		evlslem3.q	. . . 4 ⊢ (𝜑 → 𝐻 ∈ 𝐾)
11		evlslem3.k	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
12	1, 2, 3, 4, 5, 8, 9, 10, 11	mplmon2cl 19861	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵)
13		fveq1 6433	. . . . . . . 8 ⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑝‘𝑏) = ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏))
14	13	fveq2d 6438	. . . . . . 7 ⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)))
15	14	oveq1d 6921	. . . . . 6 ⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))
16	15	mpteq2dv 4969	. . . . 5 ⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))))
17	16	oveq2d 6922	. . . 4 ⊢ (𝑝 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))
18		evlslem1.e	. . . 4 ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))
19		ovex 6938	. . . 4 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))) ∈ V
20	17, 18, 19	fvmpt 6530	. . 3 ⊢ ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) ∈ 𝐵 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))
21	12, 20	syl 17	. 2 ⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))
22		eqid 2826	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 )) = (𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))
23		eqeq1 2830	. . . . . . . . 9 ⊢ (𝑥 = 𝑏 → (𝑥 = 𝐴 ↔ 𝑏 = 𝐴))
24	23	ifbid 4329	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → if(𝑥 = 𝐴, 𝐻, 0 ) = if(𝑏 = 𝐴, 𝐻, 0 ))
25		simpr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
26	3	fvexi 6448	. . . . . . . . . . 11 ⊢ 0 ∈ V
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ V)
28		ifexg 4354	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝐾 ∧ 0 ∈ V) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ V)
29	10, 27, 28	syl2anc 581	. . . . . . . . 9 ⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ V)
30	29	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ V)
31	22, 24, 25, 30	fvmptd3 6551	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏) = if(𝑏 = 𝐴, 𝐻, 0 ))
32	31	fveq2d 6438	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) = (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )))
33	32	oveq1d 6921	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))
34	33	mpteq2dva 4968	. . . 4 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))))
35	34	oveq2d 6922	. . 3 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))))
36		evlslem1.c	. . . 4 ⊢ 𝐶 = (Base‘𝑆)
37		eqid 2826	. . . 4 ⊢ (0g‘𝑆) = (0g‘𝑆)
38		evlslem1.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ CRing)
39		crngring 18913	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
40	38, 39	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Ring)
41		ringmnd 18911	. . . . 5 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ Mnd)
42	40, 41	syl 17	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Mnd)
43		ovex 6938	. . . . . 6 ⊢ (ℕ0 ↑𝑚 𝐼) ∈ V
44	2, 43	rabex2 5040	. . . . 5 ⊢ 𝐷 ∈ V
45	44	a1i 11	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
46	40	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
47		evlslem1.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
48	4, 36	rhmf 19083	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾⟶𝐶)
49	47, 48	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐾⟶𝐶)
50	4, 3	ring0cl 18924	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐾)
51	8, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐾)
52	10, 51	ifcld 4352	. . . . . . . 8 ⊢ (𝜑 → if(𝑏 = 𝐴, 𝐻, 0 ) ∈ 𝐾)
53	49, 52	ffvelrnd 6610	. . . . . . 7 ⊢ (𝜑 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶)
54	53	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶)
55		evlslem1.t	. . . . . . . 8 ⊢ 𝑇 = (mulGrp‘𝑆)
56	55, 36	mgpbas 18850	. . . . . . 7 ⊢ 𝐶 = (Base‘𝑇)
57		eqid 2826	. . . . . . 7 ⊢ (0g‘𝑇) = (0g‘𝑇)
58	55	crngmgp 18910	. . . . . . . . 9 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
59	38, 58	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ CMnd)
60	59	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
61	5	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V)
62		cmnmnd 18562	. . . . . . . . . . 11 ⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd)
63	59, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ Mnd)
64	63	ad2antrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑇 ∈ Mnd)
65		simprl 789	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ ℕ0)
66		simprr 791	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶)
67		evlslem1.x	. . . . . . . . . 10 ⊢ ↑ = (.g‘𝑇)
68	56, 67	mulgnn0cl 17912	. . . . . . . . 9 ⊢ ((𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶) → (𝑦 ↑ 𝑧) ∈ 𝐶)
69	64, 65, 66, 68	syl3anc 1496	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶)) → (𝑦 ↑ 𝑧) ∈ 𝐶)
70	2	psrbagf 19727	. . . . . . . . 9 ⊢ ((𝐼 ∈ V ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0)
71	5, 70	sylan 577	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0)
72		evlslem1.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
73	72	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
74		inidm 4048	. . . . . . . 8 ⊢ (𝐼 ∩ 𝐼) = 𝐼
75	69, 71, 73, 61, 61, 74	off 7173	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺):𝐼⟶𝐶)
76		ovex 6938	. . . . . . . . 9 ⊢ (𝑏 ∘𝑓 ↑ 𝐺) ∈ V
77	76	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) ∈ V)
78	75	ffund 6283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑏 ∘𝑓 ↑ 𝐺))
79		fvex 6447	. . . . . . . . 9 ⊢ (0g‘𝑇) ∈ V
80	79	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (0g‘𝑇) ∈ V)
81	2	psrbag 19726	. . . . . . . . . 10 ⊢ (𝐼 ∈ V → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈ Fin)))
82	5, 81	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↔ (𝑏:𝐼⟶ℕ0 ∧ (◡𝑏 “ ℕ) ∈ Fin)))
83	82	simplbda 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (◡𝑏 “ ℕ) ∈ Fin)
84	71	ffnd 6280	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼)
85	84	adantr 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑏 Fn 𝐼)
86	72	ffnd 6280	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 Fn 𝐼)
87	86	ad2antrr 719	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐺 Fn 𝐼)
88	5	ad2antrr 719	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝐼 ∈ V)
89		eldifi 3960	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → 𝑦 ∈ 𝐼)
90	89	adantl 475	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → 𝑦 ∈ 𝐼)
91		fnfvof 7172	. . . . . . . . . . 11 ⊢ (((𝑏 Fn 𝐼 ∧ 𝐺 Fn 𝐼) ∧ (𝐼 ∈ V ∧ 𝑦 ∈ 𝐼)) → ((𝑏 ∘𝑓 ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦)))
92	85, 87, 88, 90, 91	syl22anc 874	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓 ↑ 𝐺)‘𝑦) = ((𝑏‘𝑦) ↑ (𝐺‘𝑦)))
93		eldifn 3961	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ)) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ))
94	93	adantl 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ 𝑦 ∈ (◡𝑏 “ ℕ))
95	89	ad2antlr 720	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ 𝐼)
96		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑏‘𝑦) ∈ ℕ)
97	84	ad2antrr 719	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑏 Fn 𝐼)
98		elpreima 6587	. . . . . . . . . . . . . . 15 ⊢ (𝑏 Fn 𝐼 → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ)))
99	97, 98	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → (𝑦 ∈ (◡𝑏 “ ℕ) ↔ (𝑦 ∈ 𝐼 ∧ (𝑏‘𝑦) ∈ ℕ)))
100	95, 96, 99	mpbir2and 706	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) ∧ (𝑏‘𝑦) ∈ ℕ) → 𝑦 ∈ (◡𝑏 “ ℕ))
101	94, 100	mtand 852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ¬ (𝑏‘𝑦) ∈ ℕ)
102		ffvelrn 6607	. . . . . . . . . . . . . 14 ⊢ ((𝑏:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑏‘𝑦) ∈ ℕ0)
103	71, 89, 102	syl2an 591	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) ∈ ℕ0)
104		elnn0 11621	. . . . . . . . . . . . 13 ⊢ ((𝑏‘𝑦) ∈ ℕ0 ↔ ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0))
105	103, 104	sylib 210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0))
106		orel1 919	. . . . . . . . . . . 12 ⊢ (¬ (𝑏‘𝑦) ∈ ℕ → (((𝑏‘𝑦) ∈ ℕ ∨ (𝑏‘𝑦) = 0) → (𝑏‘𝑦) = 0))
107	101, 105, 106	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝑏‘𝑦) = 0)
108	107	oveq1d 6921	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏‘𝑦) ↑ (𝐺‘𝑦)) = (0 ↑ (𝐺‘𝑦)))
109		ffvelrn 6607	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐼⟶𝐶 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ 𝐶)
110	73, 89, 109	syl2an 591	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (𝐺‘𝑦) ∈ 𝐶)
111	56, 57, 67	mulg0 17901	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑦) ∈ 𝐶 → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇))
112	110, 111	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → (0 ↑ (𝐺‘𝑦)) = (0g‘𝑇))
113	92, 108, 112	3eqtrd 2866	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑦 ∈ (𝐼 ∖ (◡𝑏 “ ℕ))) → ((𝑏 ∘𝑓 ↑ 𝐺)‘𝑦) = (0g‘𝑇))
114	75, 113	suppss 7591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑏 ∘𝑓 ↑ 𝐺) supp (0g‘𝑇)) ⊆ (◡𝑏 “ ℕ))
115		suppssfifsupp 8560	. . . . . . . 8 ⊢ ((((𝑏 ∘𝑓 ↑ 𝐺) ∈ V ∧ Fun (𝑏 ∘𝑓 ↑ 𝐺) ∧ (0g‘𝑇) ∈ V) ∧ ((◡𝑏 “ ℕ) ∈ Fin ∧ ((𝑏 ∘𝑓 ↑ 𝐺) supp (0g‘𝑇)) ⊆ (◡𝑏 “ ℕ))) → (𝑏 ∘𝑓 ↑ 𝐺) finSupp (0g‘𝑇))
116	77, 78, 80, 83, 114, 115	syl32anc 1503	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘𝑓 ↑ 𝐺) finSupp (0g‘𝑇))
117	56, 57, 60, 61, 75, 116	gsumcl 18670	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)) ∈ 𝐶)
118		evlslem1.m	. . . . . . 7 ⊢ · = (.r‘𝑆)
119	36, 118	ringcl 18916	. . . . . 6 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)) ∈ 𝐶) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) ∈ 𝐶)
120	46, 54, 117, 119	syl3anc 1496	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) ∈ 𝐶)
121	120	fmpttd 6635	. . . 4 ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))):𝐷⟶𝐶)
122		eldifsni 4541	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ≠ 𝐴)
123	122	neneqd 3005	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → ¬ 𝑏 = 𝐴)
124	123	iffalsed 4318	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 )
125	124	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → if(𝑏 = 𝐴, 𝐻, 0 ) = 0 )
126	125	fveq2d 6438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘ 0 ))
127		rhmghm 19082	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
128	47, 127	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))
129	3, 37	ghmid 18018	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹‘ 0 ) = (0g‘𝑆))
130	128, 129	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘ 0 ) = (0g‘𝑆))
131	130	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘ 0 ) = (0g‘𝑆))
132	126, 131	eqtrd 2862	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (0g‘𝑆))
133	132	oveq1d 6921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))
134	40	adantr 474	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → 𝑆 ∈ Ring)
135		eldifi 3960	. . . . . . . 8 ⊢ (𝑏 ∈ (𝐷 ∖ {𝐴}) → 𝑏 ∈ 𝐷)
136	135, 117	sylan2 588	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)) ∈ 𝐶)
137	36, 118, 37	ringlz 18942	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)) ∈ 𝐶) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = (0g‘𝑆))
138	134, 136, 137	syl2anc 581	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((0g‘𝑆) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = (0g‘𝑆))
139	133, 138	eqtrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ {𝐴})) → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = (0g‘𝑆))
140	139, 45	suppss2 7595	. . . 4 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))) supp (0g‘𝑆)) ⊆ {𝐴})
141	36, 37, 42, 45, 11, 121, 140	gsumpt 18715	. . 3 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))‘𝐴))
142	35, 141	eqtrd 2862	. 2 ⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))‘𝑏)) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))‘𝐴))
143		iftrue 4313	. . . . . 6 ⊢ (𝑏 = 𝐴 → if(𝑏 = 𝐴, 𝐻, 0 ) = 𝐻)
144	143	fveq2d 6438	. . . . 5 ⊢ (𝑏 = 𝐴 → (𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) = (𝐹‘𝐻))
145		oveq1 6913	. . . . . 6 ⊢ (𝑏 = 𝐴 → (𝑏 ∘𝑓 ↑ 𝐺) = (𝐴 ∘𝑓 ↑ 𝐺))
146	145	oveq2d 6922	. . . . 5 ⊢ (𝑏 = 𝐴 → (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)) = (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺)))
147	144, 146	oveq12d 6924	. . . 4 ⊢ (𝑏 = 𝐴 → ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))
148		eqid 2826	. . . 4 ⊢ (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))
149		ovex 6938	. . . 4 ⊢ ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))) ∈ V
150	147, 148, 149	fvmpt 6530	. . 3 ⊢ (𝐴 ∈ 𝐷 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))
151	11, 150	syl 17	. 2 ⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘if(𝑏 = 𝐴, 𝐻, 0 )) · (𝑇 Σg (𝑏 ∘𝑓 ↑ 𝐺))))‘𝐴) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))
152	21, 142, 151	3eqtrd 2866	1 ⊢ (𝜑 → (𝐸‘(𝑥 ∈ 𝐷 ↦ if(𝑥 = 𝐴, 𝐻, 0 ))) = ((𝐹‘𝐻) · (𝑇 Σg (𝐴 ∘𝑓 ↑ 𝐺))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880   = wceq 1658   ∈ wcel 2166  {crab 3122  Vcvv 3415   ∖ cdif 3796   ⊆ wss 3799  ifcif 4307  {csn 4398   class class class wbr 4874   ↦ cmpt 4953  ^◡ccnv 5342   “ cima 5346  Fun wfun 6118   Fn wfn 6119  ⟶wf 6120  ‘cfv 6124  (class class class)co 6906   ∘_𝑓 cof 7156   supp csupp 7560   ↑_𝑚 cmap 8123  Fincfn 8223   finSupp cfsupp 8545  0cc0 10253  ℕcn 11351  ℕ₀cn0 11619  Basecbs 16223  ._rcmulr 16307  0_gc0g 16454   Σ_g cgsu 16455  Mndcmnd 17648  ._gcmg 17895   GrpHom cghm 18009  CMndccmn 18547  mulGrpcmgp 18844  Ringcrg 18902  CRingccrg 18903   RingHom crh 19069   mVar cmvr 19714   mPoly cmpl 19715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-inf2 8816  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-iin 4744  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-of 7158  df-om 7328  df-1st 7429  df-2nd 7430  df-supp 7561  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-oadd 7831  df-er 8010  df-map 8125  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-fsupp 8546  df-oi 8685  df-card 9079  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-nn 11352  df-2 11415  df-3 11416  df-4 11417  df-5 11418  df-6 11419  df-7 11420  df-8 11421  df-9 11422  df-n0 11620  df-z 11706  df-uz 11970  df-fz 12621  df-fzo 12762  df-seq 13097  df-hash 13412  df-struct 16225  df-ndx 16226  df-slot 16227  df-base 16229  df-sets 16230  df-ress 16231  df-plusg 16319  df-mulr 16320  df-sca 16322  df-vsca 16323  df-tset 16325  df-0g 16456  df-gsum 16457  df-mre 16600  df-mrc 16601  df-acs 16603  df-mgm 17596  df-sgrp 17638  df-mnd 17649  df-mhm 17689  df-submnd 17690  df-grp 17780  df-minusg 17781  df-sbg 17782  df-mulg 17896  df-subg 17943  df-ghm 18010  df-cntz 18101  df-cmn 18549  df-mgp 18845  df-ur 18857  df-ring 18904  df-cring 18905  df-rnghom 19072  df-lmod 19222  df-lss 19290  df-psr 19718  df-mpl 19720

This theorem is referenced by:  evlslem1  19876