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

Metamath Proof Explorer

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 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )