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 43 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
74 5 36 73 3syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
75 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
76 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
77 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
78 3 1 77 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
79 5 78 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
81 43 77 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
82 81 4 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
83 75 76 80 82 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
84 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
85 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
86 77 84 7 85 35 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
87 72 83 86 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
88 69 87 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
89 63 88 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝐴 = 0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
90 89 ex ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
91 62 90 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
92 91 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
93 92 ralimdva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
94 60 93 syl5bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) )
95 94 imp ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) )
96 2 35 39 49 50 95 gsummptnn0fz ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
97 96 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
98 97 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) )
99 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑅 ∈ Ring )
100 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝐿 ∈ ℕ0 )
101 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝑘 ∈ ℕ0 )
102 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝜑 )
103 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 )
104 102 76 103 3jca ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) )
105 101 104 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) )
106 105 45 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
107 106 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
109 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 0 ... 𝑠 ) ∈ Fin )
110 1 2 99 100 108 109 coe1fzgsumd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) )
111 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑠 ∈ ℕ0 )
112 nfcv ⊢ Ⅎ 𝑘 ℕ0
113 112 54 nfralw ⊢ Ⅎ 𝑘 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 )
114 111 113 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) )
115 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring )
116 12 expcom ⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → 𝐴 ∈ 𝐾 ) )
117 116 101 syl11 ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) )
118 117 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) )
119 118 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ 𝐾 )
120 101 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑘 ∈ ℕ0 )
121 8 6 1 3 7 43 4 coe1tm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) )
122 115 119 120 121 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) )
123 eqeq1 ⊢ ( 𝑛 = 𝐿 → ( 𝑛 = 𝑘 ↔ 𝐿 = 𝑘 ) )
124 123 ifbid ⊢ ( 𝑛 = 𝐿 → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
125 124 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) ∧ 𝑛 = 𝐿 ) → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
126 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐿 ∈ ℕ0 )
127 6 8 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
128 5 127 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
129 128 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 0 ∈ 𝐾 )
130 119 129 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ∈ 𝐾 )
131 122 125 126 130 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) )
132 114 131 mpteq2da ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) )
133 132 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) )
134 breq2 ⊢ ( 𝑥 = 𝐿 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝐿 ) )
135 csbeq1 ⊢ ( 𝑥 = 𝐿 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
136 135 eqeq1d ⊢ ( 𝑥 = 𝐿 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ↔ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) )
137 134 136 imbi12d ⊢ ( 𝑥 = 𝐿 → ( ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ) )
138 137 rspcva ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) )
139 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) )
140 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴
141 140 nfeq1 ⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0
142 139 141 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 )
143 elfz2nn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) )
144 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
145 144 ad2antrr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
146 nn0re ⊢ ( 𝑠 ∈ ℕ0 → 𝑠 ∈ ℝ )
147 146 adantl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑠 ∈ ℝ )
148 147 adantr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑠 ∈ ℝ )
149 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
150 149 adantl ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℝ )
151 lelttr ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) )
152 145 148 150 151 syl3anc ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) )
153 animorr ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) )
154 df-ne ⊢ ( 𝐿 ≠ 𝑘 ↔ ¬ 𝐿 = 𝑘 )
155 144 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
156 lttri2 ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
157 149 155 156 syl2anr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
158 157 adantr ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
159 154 158 bitr3id ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( ¬ 𝐿 = 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) )
160 153 159 mpbird ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ¬ 𝐿 = 𝑘 )
161 160 ex ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 < 𝐿 → ¬ 𝐿 = 𝑘 ) )
162 152 161 syld ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → ¬ 𝐿 = 𝑘 ) )
163 162 exp4b ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
164 163 expimpd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
165 164 com23 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
166 165 imp ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
167 166 3adant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
168 143 167 sylbi ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) )
169 168 expd ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
170 11 169 syl7 ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
171 170 com12 ⊢ ( 𝑠 ∈ ℕ0 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) )
172 171 com24 ⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 < 𝐿 → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) ) )
173 172 imp ⊢ ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) )
174 173 impcom ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) )
175 174 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) )
176 175 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ¬ 𝐿 = 𝑘 )
177 176 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = 0 )
178 142 177 mpteq2da ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) )
179 178 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) )
180 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
181 5 180 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
182 181 adantr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → 𝑅 ∈ Mnd )
183 ovex ⊢ ( 0 ... 𝑠 ) ∈ V
184 8 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑠 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
185 182 183 184 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
186 185 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 )
187 id ⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 )
188 187 eqcomd ⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
189 188 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
190 179 186 189 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
191 190 ex ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
192 191 expr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) )
193 192 a2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) )
194 193 ex ⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
195 194 com13 ⊢ ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
196 138 195 syl ⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
197 196 ex ⊢ ( 𝐿 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) )
198 197 com24 ⊢ ( 𝐿 ∈ ℕ0 → ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) )
199 11 198 mpcom ⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) )
200 199 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
201 200 com12 ⊢ ( 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
202 pm3.2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) )
203 202 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) )
204 181 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝑅 ∈ Mnd )
205 183 a1i ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 0 ... 𝑠 ) ∈ V )
206 11 nn0red ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
207 lenlt ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) )
208 206 146 207 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) )
209 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ℕ0 )
210 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝑠 ∈ ℕ0 )
211 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ≤ 𝑠 )
212 elfz2nn0 ⊢ ( 𝐿 ∈ ( 0 ... 𝑠 ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝐿 ≤ 𝑠 ) )
213 209 210 211 212 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ( 0 ... 𝑠 ) )
214 213 ex ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 → 𝐿 ∈ ( 0 ... 𝑠 ) ) )
215 208 214 sylbird ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → 𝐿 ∈ ( 0 ... 𝑠 ) ) )
216 215 imp ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝐿 ∈ ( 0 ... 𝑠 ) )
217 eqcom ⊢ ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 )
218 ifbi ⊢ ( ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 ) )
219 217 218 ax-mp ⊢ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 )
220 219 mpteq2i ⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝑘 = 𝐿 , 𝐴 , 0 ) )
221 12 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
222 221 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) )
223 222 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) )
224 223 101 impel ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
225 224 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
226 225 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
227 8 204 205 216 220 226 gsummpt1n0 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
228 203 227 syl6com ⊢ ( ¬ 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
229 201 228 pm2.61i ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
230 133 229 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
231 98 110 230 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )
232 231 ex ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
233 34 232 syld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
234 233 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) )
235 23 234 mpd ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 )