Theorem gsummoncoe1

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by AV, 13-Oct-2019)

	Ref	Expression
Hypotheses	gsummonply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	gsummonply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	gsummonply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	gsummonply1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	gsummonply1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	gsummonply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	gsummonply1.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
	gsummonply1.0	⊢ 0 = ( 0g ‘ 𝑅 )
	gsummonply1.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
	gsummonply1.f	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
	gsummonply1.l	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
Assertion	gsummoncoe1	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		gsummonply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		gsummonply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		gsummonply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
4		gsummonply1.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
5		gsummonply1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		gsummonply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
7		gsummonply1.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
8		gsummonply1.0	⊢ 0 = ( 0g ‘ 𝑅 )
9		gsummonply1.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
10		gsummonply1.f	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
11		gsummonply1.l	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
12	9	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 )
13	12	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 )
14	6	fvexi	⊢ 𝐾 ∈ V
15	14	a1i	⊢ ( 𝜑 → 𝐾 ∈ V )
16		nn0ex	⊢ ℕ0 ∈ V
17		elmapg	⊢ ( ( 𝐾 ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 ) )
18	15 16 17	sylancl	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 ) )
19	13 18	mpbird	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) )
20	8	fvexi	⊢ 0 ∈ V
21		fsuppmapnn0ub	⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ) )
22	19 20 21	sylancl	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ) )
23	10 22	mpd	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) )
24		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
25	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
26		rspcsbela	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
27	24 25 26	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
28		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐴 )
29	28	fvmpts	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐴 )
30	24 27 29	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐴 )
31	30	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) )
32	31	imbi2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) )
33	32	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) )
34	33	ralimdva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) )
35		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
36	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
37		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
38	5 36 37	3syl	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
39	38	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑃 ∈ CMnd )
40	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑅 ∈ Ring )
41		simp3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
42		simp2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑘 ∈ ℕ0 )
43		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
44	6 1 3 7 43 4 2	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
45	40 41 42 44	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
46	45	3expia	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∈ 𝐾 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) )
47	46	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) )
48	9 47	mpd	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
49	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
50		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑠 ∈ ℕ0 )
51		nfv	⊢ Ⅎ 𝑘 𝑠 < 𝑥
52		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐴
53	52	nfeq1	⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0
54	51 53	nfim	⊢ Ⅎ 𝑘 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 )
55		nfv	⊢ Ⅎ 𝑥 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 )
56		breq2	⊢ ( 𝑥 = 𝑘 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝑘 ) )
57		csbeq1	⊢ ( 𝑥 = 𝑘 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = ⦋ 𝑘 / 𝑘 ⦌ 𝐴 )
58	57	eqeq1d	⊢ ( 𝑥 = 𝑘 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ↔ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) )
59	56 58	imbi12d	⊢ ( 𝑥 = 𝑘 → ( ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) ) )
60	54 55 59	cbvralw	⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) )
61		csbid	⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 𝐴
62	61	eqeq1i	⊢ ( ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ↔ 𝐴 = 0 )
63		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) )
64	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
65	5 64	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
66	65	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
67	8 66	eqtrid	⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
68	67	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
69	68	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
70	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
71	5 70	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
72	71	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
73		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
74	43 73	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
75	43	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
76	5 36 75	3syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
77	76	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
78		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
79	3 1 73	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
80	5 79	syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
81	80	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
82	74 4 77 78 81	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
83		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
84		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
85	73 83 7 84 35	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
86	72 82 85	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
87	69 86	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
88	63 87	sylan9eqr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝐴 = 0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
89	88	ex	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
90	62 89	biimtrid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
91	90	imim2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
92	91	ralimdva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
93	60 92	biimtrid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
94	93	imp	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
95	2 35 39 49 50 94	gsummptnn0fz	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
96	95	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
97	96	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) )
98	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑅 ∈ Ring )
99	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝐿 ∈ ℕ0 )
100		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝑘 ∈ ℕ0 )
101		simpll	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝜑 )
102	12	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 )
103	101 78 102	3jca	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) )
104	100 103	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) )
105	104 45	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
106	105	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
107	106	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
108		fzfid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 0 ... 𝑠 ) ∈ Fin )
109	1 2 98 99 107 108	coe1fzgsumd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) )
110		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑠 ∈ ℕ0 )
111		nfcv	⊢ Ⅎ 𝑘 ℕ0
112	111 54	nfralw	⊢ Ⅎ 𝑘 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 )
113	110 112	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) )
114	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
115	12	expcom	⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → 𝐴 ∈ 𝐾 ) )
116	115 100	syl11	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) )
117	116	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) )
118	117	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ 𝐾 )
119	100	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑘 ∈ ℕ0 )
120	8 6 1 3 7 43 4	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) )
121	114 118 119 120	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) )
122		eqeq1	⊢ ( 𝑛 = 𝐿 → ( 𝑛 = 𝑘 ↔ 𝐿 = 𝑘 ) )
123	122	ifbid	⊢ ( 𝑛 = 𝐿 → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
124	123	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) ∧ 𝑛 = 𝐿 ) → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
125	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐿 ∈ ℕ0 )
126	6 8	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
127	5 126	syl	⊢ ( 𝜑 → 0 ∈ 𝐾 )
128	127	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 0 ∈ 𝐾 )
129	118 128	ifcld	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ∈ 𝐾 )
130	121 124 125 129	fvmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
131	113 130	mpteq2da	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) )
132	131	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) )
133		breq2	⊢ ( 𝑥 = 𝐿 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝐿 ) )
134		csbeq1	⊢ ( 𝑥 = 𝐿 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
135	134	eqeq1d	⊢ ( 𝑥 = 𝐿 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ↔ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) )
136	133 135	imbi12d	⊢ ( 𝑥 = 𝐿 → ( ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ) )
137	136	rspcva	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) )
138		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) )
139		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴
140	139	nfeq1	⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0
141	138 140	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 )
142		elfz2nn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) )
143		nn0re	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
144	143	ad2antrr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
145		nn0re	⊢ ( 𝑠 ∈ ℕ0 → 𝑠 ∈ ℝ )
146	145	adantl	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑠 ∈ ℝ )
147	146	adantr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑠 ∈ ℝ )
148		nn0re	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
149	148	adantl	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℝ )
150		lelttr	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) )
151	144 147 149 150	syl3anc	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) )
152		animorr	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) )
153		df-ne	⊢ ( 𝐿 ≠ 𝑘 ↔ ¬ 𝐿 = 𝑘 )
154	143	adantr	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
155		lttri2	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
156	148 154 155	syl2anr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
157	156	adantr	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
158	153 157	bitr3id	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( ¬ 𝐿 = 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
159	152 158	mpbird	⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ¬ 𝐿 = 𝑘 )
160	159	ex	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 < 𝐿 → ¬ 𝐿 = 𝑘 ) )
161	151 160	syld	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → ¬ 𝐿 = 𝑘 ) )
162	161	exp4b	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
163	162	expimpd	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
164	163	com23	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
165	164	imp	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
166	165	3adant2	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
167	142 166	sylbi	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
168	167	expd	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
169	11 168	syl7	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
170	169	com12	⊢ ( 𝑠 ∈ ℕ0 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
171	170	com24	⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 < 𝐿 → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) ) )
172	171	imp	⊢ ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) )
173	172	impcom	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) )
174	173	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) )
175	174	imp	⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ¬ 𝐿 = 𝑘 )
176	175	iffalsed	⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = 0 )
177	141 176	mpteq2da	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) )
178	177	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) )
179		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
180	5 179	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
181	180	adantr	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → 𝑅 ∈ Mnd )
182		ovex	⊢ ( 0 ... 𝑠 ) ∈ V
183	8	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑠 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
184	181 182 183	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
185	184	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
186		id	⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 )
187	186	eqcomd	⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
188	187	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
189	178 185 188	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
190	189	ex	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
191	190	expr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) )
192	191	a2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) )
193	192	ex	⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
194	193	com13	⊢ ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
195	137 194	syl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
196	195	ex	⊢ ( 𝐿 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) )
197	196	com24	⊢ ( 𝐿 ∈ ℕ0 → ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) )
198	11 197	mpcom	⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
199	198	imp31	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
200	199	com12	⊢ ( 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
201		pm3.2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) )
202	201	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) )
203	180	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝑅 ∈ Mnd )
204	182	a1i	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 0 ... 𝑠 ) ∈ V )
205	11	nn0red	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
206		lenlt	⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) )
207	205 145 206	syl2an	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) )
208	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ℕ0 )
209		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝑠 ∈ ℕ0 )
210		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ≤ 𝑠 )
211		elfz2nn0	⊢ ( 𝐿 ∈ ( 0 ... 𝑠 ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝐿 ≤ 𝑠 ) )
212	208 209 210 211	syl3anbrc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ( 0 ... 𝑠 ) )
213	212	ex	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 → 𝐿 ∈ ( 0 ... 𝑠 ) ) )
214	207 213	sylbird	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → 𝐿 ∈ ( 0 ... 𝑠 ) ) )
215	214	imp	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝐿 ∈ ( 0 ... 𝑠 ) )
216		eqcom	⊢ ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 )
217		ifbi	⊢ ( ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 ) )
218	216 217	ax-mp	⊢ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 )
219	218	mpteq2i	⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝑘 = 𝐿 , 𝐴 , 0 ) )
220	12 6	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
221	220	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) )
222	221	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) )
223	222 100	impel	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
224	223	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
225	224	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
226	8 203 204 215 219 225	gsummpt1n0	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
227	202 226	syl6com	⊢ ( ¬ 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
228	200 227	pm2.61i	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
229	132 228	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
230	97 109 229	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
231	230	ex	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
232	34 231	syld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
233	232	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
234	23 233	mpd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )