MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsummoncoe1 Structured version   Visualization version   GIF version

Theorem gsummoncoe1 21810
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.)
Hypotheses
Ref Expression
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
Ref Expression
gsummoncoe1 (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴)
Distinct variable groups:   𝐵,𝑘   𝑘,𝐾   𝜑,𝑘   ,𝑘   𝑘,𝐿   𝑃,𝑘   𝑅,𝑘   0 ,𝑘   ,𝑘
Allowed substitution hints:   𝐴(𝑘)   𝑋(𝑘)

Proof of Theorem gsummoncoe1
Dummy variables 𝑛 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsummonply1.f . . 3 (𝜑 → (𝑘 ∈ ℕ0𝐴) finSupp 0 )
2 gsummonply1.a . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ0 𝐴𝐾)
32r19.21bi 3249 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → 𝐴𝐾)
43fmpttd 7110 . . . . 5 (𝜑 → (𝑘 ∈ ℕ0𝐴):ℕ0𝐾)
5 gsummonply1.k . . . . . . . 8 𝐾 = (Base‘𝑅)
65fvexi 6902 . . . . . . 7 𝐾 ∈ V
76a1i 11 . . . . . 6 (𝜑𝐾 ∈ V)
8 nn0ex 12474 . . . . . 6 0 ∈ V
9 elmapg 8829 . . . . . 6 ((𝐾 ∈ V ∧ ℕ0 ∈ V) → ((𝑘 ∈ ℕ0𝐴) ∈ (𝐾m0) ↔ (𝑘 ∈ ℕ0𝐴):ℕ0𝐾))
107, 8, 9sylancl 587 . . . . 5 (𝜑 → ((𝑘 ∈ ℕ0𝐴) ∈ (𝐾m0) ↔ (𝑘 ∈ ℕ0𝐴):ℕ0𝐾))
114, 10mpbird 257 . . . 4 (𝜑 → (𝑘 ∈ ℕ0𝐴) ∈ (𝐾m0))
12 gsummonply1.0 . . . . 5 0 = (0g𝑅)
1312fvexi 6902 . . . 4 0 ∈ V
14 fsuppmapnn0ub 13956 . . . 4 (((𝑘 ∈ ℕ0𝐴) ∈ (𝐾m0) ∧ 0 ∈ V) → ((𝑘 ∈ ℕ0𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 )))
1511, 13, 14sylancl 587 . . 3 (𝜑 → ((𝑘 ∈ ℕ0𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 )))
161, 15mpd 15 . 2 (𝜑 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ))
17 simpr 486 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℕ0)
182ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 𝐴𝐾)
19 rspcsbela 4434 . . . . . . . . . 10 ((𝑥 ∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 𝐴𝐾) → 𝑥 / 𝑘𝐴𝐾)
2017, 18, 19syl2anc 585 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 / 𝑘𝐴𝐾)
21 eqid 2733 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝐴) = (𝑘 ∈ ℕ0𝐴)
2221fvmpts 6997 . . . . . . . . 9 ((𝑥 ∈ ℕ0𝑥 / 𝑘𝐴𝐾) → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 𝑥 / 𝑘𝐴)
2317, 20, 22syl2anc 585 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 𝑥 / 𝑘𝐴)
2423eqeq1d 2735 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0𝑥 / 𝑘𝐴 = 0 ))
2524imbi2d 341 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) ↔ (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
2625biimpd 228 . . . . 5 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
2726ralimdva 3168 . . . 4 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
28 gsummonply1.b . . . . . . . . 9 𝐵 = (Base‘𝑃)
29 eqid 2733 . . . . . . . . 9 (0g𝑃) = (0g𝑃)
30 gsummonply1.r . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
31 gsummonply1.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
3231ply1ring 21752 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
33 ringcmn 20089 . . . . . . . . . . 11 (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
3430, 32, 333syl 18 . . . . . . . . . 10 (𝜑𝑃 ∈ CMnd)
3534ad2antrr 725 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑃 ∈ CMnd)
36303ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝑅 ∈ Ring)
37 simp3 1139 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝐴𝐾)
38 simp2 1138 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝑘 ∈ ℕ0)
39 gsummonply1.x . . . . . . . . . . . . . . 15 𝑋 = (var1𝑅)
40 gsummonply1.m . . . . . . . . . . . . . . 15 = ( ·𝑠𝑃)
41 eqid 2733 . . . . . . . . . . . . . . 15 (mulGrp‘𝑃) = (mulGrp‘𝑃)
42 gsummonply1.e . . . . . . . . . . . . . . 15 = (.g‘(mulGrp‘𝑃))
435, 31, 39, 40, 41, 42, 28ply1tmcl 21776 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐴𝐾𝑘 ∈ ℕ0) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
4436, 37, 38, 43syl3anc 1372 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
45443expia 1122 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝐾 → (𝐴 (𝑘 𝑋)) ∈ 𝐵))
4645ralimdva 3168 . . . . . . . . . . 11 (𝜑 → (∀𝑘 ∈ ℕ0 𝐴𝐾 → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵))
472, 46mpd 15 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵)
4847ad2antrr 725 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵)
49 simplr 768 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑠 ∈ ℕ0)
50 nfv 1918 . . . . . . . . . . . . 13 𝑘 𝑠 < 𝑥
51 nfcsb1v 3917 . . . . . . . . . . . . . 14 𝑘𝑥 / 𝑘𝐴
5251nfeq1 2919 . . . . . . . . . . . . 13 𝑘𝑥 / 𝑘𝐴 = 0
5350, 52nfim 1900 . . . . . . . . . . . 12 𝑘(𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )
54 nfv 1918 . . . . . . . . . . . 12 𝑥(𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 )
55 breq2 5151 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (𝑠 < 𝑥𝑠 < 𝑘))
56 csbeq1 3895 . . . . . . . . . . . . . 14 (𝑥 = 𝑘𝑥 / 𝑘𝐴 = 𝑘 / 𝑘𝐴)
5756eqeq1d 2735 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (𝑥 / 𝑘𝐴 = 0𝑘 / 𝑘𝐴 = 0 ))
5855, 57imbi12d 345 . . . . . . . . . . . 12 (𝑥 = 𝑘 → ((𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 )))
5953, 54, 58cbvralw 3304 . . . . . . . . . . 11 (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ))
60 csbid 3905 . . . . . . . . . . . . . . 15 𝑘 / 𝑘𝐴 = 𝐴
6160eqeq1i 2738 . . . . . . . . . . . . . 14 (𝑘 / 𝑘𝐴 = 0𝐴 = 0 )
62 oveq1 7411 . . . . . . . . . . . . . . . 16 (𝐴 = 0 → (𝐴 (𝑘 𝑋)) = ( 0 (𝑘 𝑋)))
6331ply1sca 21757 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
6430, 63syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 = (Scalar‘𝑃))
6564fveq2d 6892 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑃)))
6612, 65eqtrid 2785 . . . . . . . . . . . . . . . . . . 19 (𝜑0 = (0g‘(Scalar‘𝑃)))
6766ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 0 = (0g‘(Scalar‘𝑃)))
6867oveq1d 7419 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ( 0 (𝑘 𝑋)) = ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)))
6931ply1lmod 21756 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ Ring → 𝑃 ∈ LMod)
7030, 69syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃 ∈ LMod)
7170ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod)
72 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (Base‘𝑃) = (Base‘𝑃)
7341, 72mgpbas 19985 . . . . . . . . . . . . . . . . . . 19 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
7441ringmgp 20053 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
7530, 32, 743syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
7675ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘𝑃) ∈ Mnd)
77 simpr 486 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
7839, 31, 72vr1cl 21723 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
7930, 78syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋 ∈ (Base‘𝑃))
8079ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ (Base‘𝑃))
8173, 42, 76, 77, 80mulgnn0cld 18969 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 𝑋) ∈ (Base‘𝑃))
82 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (Scalar‘𝑃) = (Scalar‘𝑃)
83 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
8472, 82, 40, 83, 29lmod0vs 20493 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ LMod ∧ (𝑘 𝑋) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)) = (0g𝑃))
8571, 81, 84syl2anc 585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)) = (0g𝑃))
8668, 85eqtrd 2773 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ( 0 (𝑘 𝑋)) = (0g𝑃))
8762, 86sylan9eqr 2795 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) ∧ 𝐴 = 0 ) → (𝐴 (𝑘 𝑋)) = (0g𝑃))
8887ex 414 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝐴 = 0 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
8961, 88biimtrid 241 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 / 𝑘𝐴 = 0 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
9089imim2d 57 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ) → (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9190ralimdva 3168 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → (∀𝑘 ∈ ℕ0 (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9259, 91biimtrid 241 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9392imp 408 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
9428, 29, 35, 48, 49, 93gsummptnn0fz 19846 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))
9594fveq2d 6892 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋))))) = (coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋))))))
9695fveq1d 6890 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))‘𝐿))
9730ad2antrr 725 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑅 ∈ Ring)
98 gsummonply1.l . . . . . . . 8 (𝜑𝐿 ∈ ℕ0)
9998ad2antrr 725 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝐿 ∈ ℕ0)
100 elfznn0 13590 . . . . . . . . . . 11 (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0)
101 simpll 766 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝜑)
1023adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴𝐾)
103101, 77, 1023jca 1129 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝜑𝑘 ∈ ℕ0𝐴𝐾))
104100, 103sylan2 594 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝜑𝑘 ∈ ℕ0𝐴𝐾))
105104, 44syl 17 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
106105ralrimiva 3147 . . . . . . . 8 ((𝜑𝑠 ∈ ℕ0) → ∀𝑘 ∈ (0...𝑠)(𝐴 (𝑘 𝑋)) ∈ 𝐵)
107106adantr 482 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ (0...𝑠)(𝐴 (𝑘 𝑋)) ∈ 𝐵)
108 fzfid 13934 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (0...𝑠) ∈ Fin)
10931, 28, 97, 99, 107, 108coe1fzgsumd 21808 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))))
110 nfv 1918 . . . . . . . . . 10 𝑘(𝜑𝑠 ∈ ℕ0)
111 nfcv 2904 . . . . . . . . . . 11 𝑘0
112111, 53nfralw 3309 . . . . . . . . . 10 𝑘𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )
113110, 112nfan 1903 . . . . . . . . 9 𝑘((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ))
11430ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
1153expcom 415 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (𝜑𝐴𝐾))
116115, 100syl11 33 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝑠) → 𝐴𝐾))
117116ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) → 𝐴𝐾))
118117imp 408 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴𝐾)
119100adantl 483 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0)
12012, 5, 31, 39, 40, 41, 42coe1tm 21777 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ 𝐴𝐾𝑘 ∈ ℕ0) → (coe1‘(𝐴 (𝑘 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 )))
121114, 118, 119, 120syl3anc 1372 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘(𝐴 (𝑘 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 )))
122 eqeq1 2737 . . . . . . . . . . . 12 (𝑛 = 𝐿 → (𝑛 = 𝑘𝐿 = 𝑘))
123122ifbid 4550 . . . . . . . . . . 11 (𝑛 = 𝐿 → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 ))
124123adantl 483 . . . . . . . . . 10 (((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑛 = 𝐿) → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 ))
12598ad3antrrr 729 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐿 ∈ ℕ0)
1265, 12ring0cl 20074 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 0𝐾)
12730, 126syl 17 . . . . . . . . . . . 12 (𝜑0𝐾)
128127ad3antrrr 729 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 0𝐾)
129118, 128ifcld 4573 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) ∈ 𝐾)
130121, 124, 125, 129fvmptd 7001 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿) = if(𝐿 = 𝑘, 𝐴, 0 ))
131113, 130mpteq2da 5245 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )))
132131oveq2d 7420 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))))
133 breq2 5151 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐿 → (𝑠 < 𝑥𝑠 < 𝐿))
134 csbeq1 3895 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐿𝑥 / 𝑘𝐴 = 𝐿 / 𝑘𝐴)
135134eqeq1d 2735 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐿 → (𝑥 / 𝑘𝐴 = 0𝐿 / 𝑘𝐴 = 0 ))
136133, 135imbi12d 345 . . . . . . . . . . . . . . 15 (𝑥 = 𝐿 → ((𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ (𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 )))
137136rspcva 3610 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ))
138 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿))
139 nfcsb1v 3917 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝐿 / 𝑘𝐴
140139nfeq1 2919 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝐿 / 𝑘𝐴 = 0
141138, 140nfan 1903 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 )
142 elfz2nn0 13588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0𝑠 ∈ ℕ0𝑘𝑠))
143 nn0re 12477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
144143ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑘 ∈ ℝ)
145 nn0re 12477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ∈ ℕ0𝑠 ∈ ℝ)
146145adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → 𝑠 ∈ ℝ)
147146adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑠 ∈ ℝ)
148 nn0re 12477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
149148adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
150 lelttr 11300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑘𝑠𝑠 < 𝐿) → 𝑘 < 𝐿))
151144, 147, 149, 150syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘𝑠𝑠 < 𝐿) → 𝑘 < 𝐿))
152 animorr 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 < 𝑘𝑘 < 𝐿))
153 df-ne 2942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐿𝑘 ↔ ¬ 𝐿 = 𝑘)
154143adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → 𝑘 ∈ ℝ)
155 lttri2 11292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
156148, 154, 155syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
157156adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
158153, 157bitr3id 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (¬ 𝐿 = 𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
159152, 158mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → ¬ 𝐿 = 𝑘)
160159ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑘 < 𝐿 → ¬ 𝐿 = 𝑘))
161151, 160syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘𝑠𝑠 < 𝐿) → ¬ 𝐿 = 𝑘))
162161exp4b 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → (𝐿 ∈ ℕ0 → (𝑘𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
163162expimpd 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ0 → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑘𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
164163com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ0 → (𝑘𝑠 → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
165164imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘 ∈ ℕ0𝑘𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
1661653adant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0𝑘𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
167142, 166sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
168167expd 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝐿 ∈ ℕ0 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
16998, 168syl7 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
170169com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ ℕ0 → (𝑘 ∈ (0...𝑠) → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
171170com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ℕ0 → (𝑠 < 𝐿 → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))))
172171imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℕ0𝑠 < 𝐿) → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)))
173172impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))
174173adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))
175174imp 408 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐿 = 𝑘)
176175iffalsed 4538 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) = 0 )
177141, 176mpteq2da 5245 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ 0 ))
178177oveq2d 7420 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )))
179 ringmnd 20057 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
18030, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ∈ Mnd)
181180adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → 𝑅 ∈ Mnd)
182 ovex 7437 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝑠) ∈ V
18312gsumz 18713 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
184181, 182, 183sylancl 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
185184adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
186 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 / 𝑘𝐴 = 0𝐿 / 𝑘𝐴 = 0 )
187186eqcomd 2739 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 / 𝑘𝐴 = 00 = 𝐿 / 𝑘𝐴)
188187adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → 0 = 𝐿 / 𝑘𝐴)
189178, 185, 1883eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
190189ex 414 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝐿 / 𝑘𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
191190expr 458 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ ℕ0) → (𝑠 < 𝐿 → (𝐿 / 𝑘𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))
192191a2d 29 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ ℕ0) → ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))
193192ex 414 . . . . . . . . . . . . . . 15 (𝜑 → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
194193com13 88 . . . . . . . . . . . . . 14 ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
195137, 194syl 17 . . . . . . . . . . . . 13 ((𝐿 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
196195ex 414 . . . . . . . . . . . 12 (𝐿 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))))
197196com24 95 . . . . . . . . . . 11 (𝐿 ∈ ℕ0 → (𝜑 → (𝑠 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))))
19898, 197mpcom 38 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
199198imp31 419 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
200199com12 32 . . . . . . . 8 (𝑠 < 𝐿 → (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
201 pm3.2 471 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ0) → (¬ 𝑠 < 𝐿 → ((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿)))
202201adantr 482 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (¬ 𝑠 < 𝐿 → ((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿)))
203180ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → 𝑅 ∈ Mnd)
204182a1i 11 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → (0...𝑠) ∈ V)
20598nn0red 12529 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℝ)
206 lenlt 11288 . . . . . . . . . . . . 13 ((𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐿𝑠 ↔ ¬ 𝑠 < 𝐿))
207205, 145, 206syl2an 597 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ0) → (𝐿𝑠 ↔ ¬ 𝑠 < 𝐿))
20898ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿 ∈ ℕ0)
209 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝑠 ∈ ℕ0)
210 simpr 486 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿𝑠)
211 elfz2nn0 13588 . . . . . . . . . . . . . 14 (𝐿 ∈ (0...𝑠) ↔ (𝐿 ∈ ℕ0𝑠 ∈ ℕ0𝐿𝑠))
212208, 209, 210, 211syl3anbrc 1344 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿 ∈ (0...𝑠))
213212ex 414 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ0) → (𝐿𝑠𝐿 ∈ (0...𝑠)))
214207, 213sylbird 260 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → (¬ 𝑠 < 𝐿𝐿 ∈ (0...𝑠)))
215214imp 408 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → 𝐿 ∈ (0...𝑠))
216 eqcom 2740 . . . . . . . . . . . 12 (𝐿 = 𝑘𝑘 = 𝐿)
217 ifbi 4549 . . . . . . . . . . . 12 ((𝐿 = 𝑘𝑘 = 𝐿) → if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 ))
218216, 217ax-mp 5 . . . . . . . . . . 11 if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 )
219218mpteq2i 5252 . . . . . . . . . 10 (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐿, 𝐴, 0 ))
2203, 5eleqtrdi 2844 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅))
221220ex 414 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ ℕ0𝐴 ∈ (Base‘𝑅)))
222221adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ ℕ0) → (𝑘 ∈ ℕ0𝐴 ∈ (Base‘𝑅)))
223222, 100impel 507 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ (Base‘𝑅))
224223ralrimiva 3147 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅))
225224adantr 482 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅))
22612, 203, 204, 215, 219, 225gsummpt1n0 19825 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
227202, 226syl6com 37 . . . . . . . 8 𝑠 < 𝐿 → (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
228200, 227pm2.61i 182 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
229132, 228eqtrd 2773 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))) = 𝐿 / 𝑘𝐴)
23096, 109, 2293eqtrd 2777 . . . . 5 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴)
231230ex 414 . . . 4 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
23227, 231syld 47 . . 3 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
233232rexlimdva 3156 . 2 (𝜑 → (∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
23416, 233mpd 15 1 (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  wrex 3071  Vcvv 3475  csb 3892  ifcif 4527   class class class wbr 5147  cmpt 5230  wf 6536  cfv 6540  (class class class)co 7404  m cmap 8816   finSupp cfsupp 9357  cr 11105  0cc0 11106   < clt 11244  cle 11245  0cn0 12468  ...cfz 13480  Basecbs 17140  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381   Σg cgsu 17382  Mndcmnd 18621  .gcmg 18944  CMndccmn 19641  mulGrpcmgp 19979  Ringcrg 20047  LModclmod 20459  var1cv1 21682  Poly1cpl1 21683  coe1cco1 21684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-ofr 7666  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19643  df-abl 19644  df-mgp 19980  df-ur 19997  df-ring 20049  df-subrg 20349  df-lmod 20461  df-lss 20531  df-psr 21444  df-mvr 21445  df-mpl 21446  df-opsr 21448  df-psr1 21686  df-vr1 21687  df-ply1 21688  df-coe1 21689
This theorem is referenced by:  gsumply1eq  21811  pm2mpf1lem  22278  pm2mpcoe1  22284  pm2mpmhmlem2  22303  cayleyhamilton1  22376  gsummoncoe1fzo  32615  ply1mulgsum  46973
  Copyright terms: Public domain W3C validator