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𝐴 ) ∈ ( 𝐾m0 ) ↔ ( 𝑘 ∈ ℕ0𝐴 ) : ℕ0𝐾 ) )
18 15 16 17 sylancl ( 𝜑 → ( ( 𝑘 ∈ ℕ0𝐴 ) ∈ ( 𝐾m0 ) ↔ ( 𝑘 ∈ ℕ0𝐴 ) : ℕ0𝐾 ) )
19 13 18 mpbird ( 𝜑 → ( 𝑘 ∈ ℕ0𝐴 ) ∈ ( 𝐾m0 ) )
20 8 fvexi 0 ∈ V
21 fsuppmapnn0ub ( ( ( 𝑘 ∈ ℕ0𝐴 ) ∈ ( 𝐾m0 ) ∧ 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 syl5eq ( 𝜑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 ( 𝐿 / 𝑘 𝐴 = 00 = 𝐿 / 𝑘 𝐴 )
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 ↦ ( 𝐴 ( 𝑘 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐿 / 𝑘 𝐴 )