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

Theorem gsummoncoe1 19947
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 3079 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → 𝐴𝐾)
43fmpttd 6575 . . . . 5 (𝜑 → (𝑘 ∈ ℕ0𝐴):ℕ0𝐾)
5 gsummonply1.k . . . . . . . 8 𝐾 = (Base‘𝑅)
65fvexi 6389 . . . . . . 7 𝐾 ∈ V
76a1i 11 . . . . . 6 (𝜑𝐾 ∈ V)
8 nn0ex 11545 . . . . . 6 0 ∈ V
9 elmapg 8073 . . . . . 6 ((𝐾 ∈ V ∧ ℕ0 ∈ V) → ((𝑘 ∈ ℕ0𝐴) ∈ (𝐾𝑚0) ↔ (𝑘 ∈ ℕ0𝐴):ℕ0𝐾))
107, 8, 9sylancl 580 . . . . 5 (𝜑 → ((𝑘 ∈ ℕ0𝐴) ∈ (𝐾𝑚0) ↔ (𝑘 ∈ ℕ0𝐴):ℕ0𝐾))
114, 10mpbird 248 . . . 4 (𝜑 → (𝑘 ∈ ℕ0𝐴) ∈ (𝐾𝑚0))
12 gsummonply1.0 . . . . 5 0 = (0g𝑅)
1312fvexi 6389 . . . 4 0 ∈ V
14 fsuppmapnn0ub 13002 . . . 4 (((𝑘 ∈ ℕ0𝐴) ∈ (𝐾𝑚0) ∧ 0 ∈ V) → ((𝑘 ∈ ℕ0𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 )))
1511, 13, 14sylancl 580 . . 3 (𝜑 → ((𝑘 ∈ ℕ0𝐴) finSupp 0 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 )))
161, 15mpd 15 . 2 (𝜑 → ∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ))
17 simpr 477 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℕ0)
182ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ∀𝑘 ∈ ℕ0 𝐴𝐾)
19 rspcsbela 4168 . . . . . . . . . 10 ((𝑥 ∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 𝐴𝐾) → 𝑥 / 𝑘𝐴𝐾)
2017, 18, 19syl2anc 579 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑥 / 𝑘𝐴𝐾)
21 eqid 2765 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝐴) = (𝑘 ∈ ℕ0𝐴)
2221fvmpts 6474 . . . . . . . . 9 ((𝑥 ∈ ℕ0𝑥 / 𝑘𝐴𝐾) → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 𝑥 / 𝑘𝐴)
2317, 20, 22syl2anc 579 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 𝑥 / 𝑘𝐴)
2423eqeq1d 2767 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0𝑥 / 𝑘𝐴 = 0 ))
2524imbi2d 331 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) ↔ (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
2625biimpd 220 . . . . 5 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
2726ralimdva 3109 . . . 4 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )))
28 gsummonply1.b . . . . . . . . 9 𝐵 = (Base‘𝑃)
29 eqid 2765 . . . . . . . . 9 (0g𝑃) = (0g𝑃)
30 gsummonply1.r . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
31 gsummonply1.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
3231ply1ring 19891 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
33 ringcmn 18848 . . . . . . . . . . 11 (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
3430, 32, 333syl 18 . . . . . . . . . 10 (𝜑𝑃 ∈ CMnd)
3534ad2antrr 717 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑃 ∈ CMnd)
36303ad2ant1 1163 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝑅 ∈ Ring)
37 simp3 1168 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝐴𝐾)
38 simp2 1167 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → 𝑘 ∈ ℕ0)
39 gsummonply1.x . . . . . . . . . . . . . . 15 𝑋 = (var1𝑅)
40 gsummonply1.m . . . . . . . . . . . . . . 15 = ( ·𝑠𝑃)
41 eqid 2765 . . . . . . . . . . . . . . 15 (mulGrp‘𝑃) = (mulGrp‘𝑃)
42 gsummonply1.e . . . . . . . . . . . . . . 15 = (.g‘(mulGrp‘𝑃))
435, 31, 39, 40, 41, 42, 28ply1tmcl 19915 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝐴𝐾𝑘 ∈ ℕ0) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
4436, 37, 38, 43syl3anc 1490 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0𝐴𝐾) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
45443expia 1150 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝐾 → (𝐴 (𝑘 𝑋)) ∈ 𝐵))
4645ralimdva 3109 . . . . . . . . . . 11 (𝜑 → (∀𝑘 ∈ ℕ0 𝐴𝐾 → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵))
472, 46mpd 15 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵)
4847ad2antrr 717 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ ℕ0 (𝐴 (𝑘 𝑋)) ∈ 𝐵)
49 simplr 785 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑠 ∈ ℕ0)
50 nfv 2009 . . . . . . . . . . . . 13 𝑘 𝑠 < 𝑥
51 nfcsb1v 3707 . . . . . . . . . . . . . 14 𝑘𝑥 / 𝑘𝐴
5251nfeq1 2921 . . . . . . . . . . . . 13 𝑘𝑥 / 𝑘𝐴 = 0
5350, 52nfim 1995 . . . . . . . . . . . 12 𝑘(𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )
54 nfv 2009 . . . . . . . . . . . 12 𝑥(𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 )
55 breq2 4813 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (𝑠 < 𝑥𝑠 < 𝑘))
56 csbeq1 3694 . . . . . . . . . . . . . 14 (𝑥 = 𝑘𝑥 / 𝑘𝐴 = 𝑘 / 𝑘𝐴)
5756eqeq1d 2767 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (𝑥 / 𝑘𝐴 = 0𝑘 / 𝑘𝐴 = 0 ))
5855, 57imbi12d 335 . . . . . . . . . . . 12 (𝑥 = 𝑘 → ((𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 )))
5953, 54, 58cbvral 3315 . . . . . . . . . . 11 (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ))
60 csbid 3699 . . . . . . . . . . . . . . 15 𝑘 / 𝑘𝐴 = 𝐴
6160eqeq1i 2770 . . . . . . . . . . . . . 14 (𝑘 / 𝑘𝐴 = 0𝐴 = 0 )
62 oveq1 6849 . . . . . . . . . . . . . . . 16 (𝐴 = 0 → (𝐴 (𝑘 𝑋)) = ( 0 (𝑘 𝑋)))
6331ply1sca 19896 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
6430, 63syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑅 = (Scalar‘𝑃))
6564fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (0g𝑅) = (0g‘(Scalar‘𝑃)))
6612, 65syl5eq 2811 . . . . . . . . . . . . . . . . . . 19 (𝜑0 = (0g‘(Scalar‘𝑃)))
6766ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 0 = (0g‘(Scalar‘𝑃)))
6867oveq1d 6857 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ( 0 (𝑘 𝑋)) = ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)))
6931ply1lmod 19895 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∈ Ring → 𝑃 ∈ LMod)
7030, 69syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃 ∈ LMod)
7170ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑃 ∈ LMod)
7241ringmgp 18820 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
7330, 32, 723syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
7473ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (mulGrp‘𝑃) ∈ Mnd)
75 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
76 eqid 2765 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝑃) = (Base‘𝑃)
7739, 31, 76vr1cl 19860 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
7830, 77syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑋 ∈ (Base‘𝑃))
7978ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈ (Base‘𝑃))
8041, 76mgpbas 18762 . . . . . . . . . . . . . . . . . . . 20 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
8180, 42mulgnn0cl 17824 . . . . . . . . . . . . . . . . . . 19 (((mulGrp‘𝑃) ∈ Mnd ∧ 𝑘 ∈ ℕ0𝑋 ∈ (Base‘𝑃)) → (𝑘 𝑋) ∈ (Base‘𝑃))
8274, 75, 79, 81syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 𝑋) ∈ (Base‘𝑃))
83 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (Scalar‘𝑃) = (Scalar‘𝑃)
84 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
8576, 83, 40, 84, 29lmod0vs 19165 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ LMod ∧ (𝑘 𝑋) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)) = (0g𝑃))
8671, 82, 85syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((0g‘(Scalar‘𝑃)) (𝑘 𝑋)) = (0g𝑃))
8768, 86eqtrd 2799 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ( 0 (𝑘 𝑋)) = (0g𝑃))
8862, 87sylan9eqr 2821 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) ∧ 𝐴 = 0 ) → (𝐴 (𝑘 𝑋)) = (0g𝑃))
8988ex 401 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝐴 = 0 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
9061, 89syl5bi 233 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 / 𝑘𝐴 = 0 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
9190imim2d 57 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ) → (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9291ralimdva 3109 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → (∀𝑘 ∈ ℕ0 (𝑠 < 𝑘𝑘 / 𝑘𝐴 = 0 ) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9359, 92syl5bi 233 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃))))
9493imp 395 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ ℕ0 (𝑠 < 𝑘 → (𝐴 (𝑘 𝑋)) = (0g𝑃)))
9528, 29, 35, 48, 49, 94gsummptnn0fz 18648 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))) = (𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))
9695fveq2d 6379 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋))))) = (coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋))))))
9796fveq1d 6377 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))‘𝐿))
9830ad2antrr 717 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝑅 ∈ Ring)
99 gsummonply1.l . . . . . . . 8 (𝜑𝐿 ∈ ℕ0)
10099ad2antrr 717 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → 𝐿 ∈ ℕ0)
101 elfznn0 12640 . . . . . . . . . . 11 (𝑘 ∈ (0...𝑠) → 𝑘 ∈ ℕ0)
102 simpll 783 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝜑)
1033adantlr 706 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴𝐾)
104102, 75, 1033jca 1158 . . . . . . . . . . 11 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝜑𝑘 ∈ ℕ0𝐴𝐾))
105101, 104sylan2 586 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝜑𝑘 ∈ ℕ0𝐴𝐾))
106105, 44syl 17 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → (𝐴 (𝑘 𝑋)) ∈ 𝐵)
107106ralrimiva 3113 . . . . . . . 8 ((𝜑𝑠 ∈ ℕ0) → ∀𝑘 ∈ (0...𝑠)(𝐴 (𝑘 𝑋)) ∈ 𝐵)
108107adantr 472 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ∀𝑘 ∈ (0...𝑠)(𝐴 (𝑘 𝑋)) ∈ 𝐵)
109 fzfid 12980 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (0...𝑠) ∈ Fin)
11031, 28, 98, 100, 108, 109coe1fzgsumd 19945 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ (0...𝑠) ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))))
111 nfv 2009 . . . . . . . . . 10 𝑘(𝜑𝑠 ∈ ℕ0)
112 nfcv 2907 . . . . . . . . . . 11 𝑘0
113112, 53nfral 3092 . . . . . . . . . 10 𝑘𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )
114111, 113nfan 1998 . . . . . . . . 9 𝑘((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ))
11530ad3antrrr 721 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑅 ∈ Ring)
1163expcom 402 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (𝜑𝐴𝐾))
117116, 101syl11 33 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝑠) → 𝐴𝐾))
118117ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) → 𝐴𝐾))
119118imp 395 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴𝐾)
120101adantl 473 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝑘 ∈ ℕ0)
12112, 5, 31, 39, 40, 41, 42coe1tm 19916 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ 𝐴𝐾𝑘 ∈ ℕ0) → (coe1‘(𝐴 (𝑘 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 )))
122115, 119, 120, 121syl3anc 1490 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → (coe1‘(𝐴 (𝑘 𝑋))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 𝑘, 𝐴, 0 )))
123 eqeq1 2769 . . . . . . . . . . . 12 (𝑛 = 𝐿 → (𝑛 = 𝑘𝐿 = 𝑘))
124123ifbid 4265 . . . . . . . . . . 11 (𝑛 = 𝐿 → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 ))
125124adantl 473 . . . . . . . . . 10 (((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) ∧ 𝑛 = 𝐿) → if(𝑛 = 𝑘, 𝐴, 0 ) = if(𝐿 = 𝑘, 𝐴, 0 ))
12699ad3antrrr 721 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 𝐿 ∈ ℕ0)
1275, 12ring0cl 18836 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → 0𝐾)
12830, 127syl 17 . . . . . . . . . . . 12 (𝜑0𝐾)
129128ad3antrrr 721 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → 0𝐾)
130119, 129ifcld 4288 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) ∈ 𝐾)
131122, 125, 126, 130fvmptd 6477 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) ∧ 𝑘 ∈ (0...𝑠)) → ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿) = if(𝐿 = 𝑘, 𝐴, 0 ))
132114, 131mpteq2da 4902 . . . . . . . 8 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿)) = (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )))
133132oveq2d 6858 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))))
134 breq2 4813 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐿 → (𝑠 < 𝑥𝑠 < 𝐿))
135 csbeq1 3694 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐿𝑥 / 𝑘𝐴 = 𝐿 / 𝑘𝐴)
136135eqeq1d 2767 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐿 → (𝑥 / 𝑘𝐴 = 0𝐿 / 𝑘𝐴 = 0 ))
137134, 136imbi12d 335 . . . . . . . . . . . . . . 15 (𝑥 = 𝐿 → ((𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) ↔ (𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 )))
138137rspcva 3459 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ))
139 nfv 2009 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘(𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿))
140 nfcsb1v 3707 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘𝐿 / 𝑘𝐴
141140nfeq1 2921 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝐿 / 𝑘𝐴 = 0
142139, 141nfan 1998 . . . . . . . . . . . . . . . . . . . . . 22 𝑘((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 )
143 elfz2nn0 12638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ (0...𝑠) ↔ (𝑘 ∈ ℕ0𝑠 ∈ ℕ0𝑘𝑠))
144 nn0re 11548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
145144ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑘 ∈ ℝ)
146 nn0re 11548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ∈ ℕ0𝑠 ∈ ℝ)
147146adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → 𝑠 ∈ ℝ)
148147adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑠 ∈ ℝ)
149 nn0re 11548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
150149adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
151 lelttr 10382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑘𝑠𝑠 < 𝐿) → 𝑘 < 𝐿))
152145, 148, 150, 151syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘𝑠𝑠 < 𝐿) → 𝑘 < 𝐿))
153 animorr 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿 < 𝑘𝑘 < 𝐿))
154 df-ne 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐿𝑘 ↔ ¬ 𝐿 = 𝑘)
155144adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → 𝑘 ∈ ℝ)
156 lttri2 10374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
157149, 155, 156syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
158157adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (𝐿𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
159154, 158syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → (¬ 𝐿 = 𝑘 ↔ (𝐿 < 𝑘𝑘 < 𝐿)))
160153, 159mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) ∧ 𝑘 < 𝐿) → ¬ 𝐿 = 𝑘)
161160ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑘 < 𝐿 → ¬ 𝐿 = 𝑘))
162152, 161syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑘𝑠𝑠 < 𝐿) → ¬ 𝐿 = 𝑘))
163162exp4b 421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0) → (𝐿 ∈ ℕ0 → (𝑘𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
164163expimpd 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ0 → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑘𝑠 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
165164com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ0 → (𝑘𝑠 → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
166165imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑘 ∈ ℕ0𝑘𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
1671663adant2 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑘 ∈ ℕ0𝑠 ∈ ℕ0𝑘𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
168143, 167sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ (0...𝑠) → ((𝑠 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘)))
169168expd 404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝐿 ∈ ℕ0 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
17099, 169syl7 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ (0...𝑠) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
171170com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ ℕ0 → (𝑘 ∈ (0...𝑠) → (𝜑 → (𝑠 < 𝐿 → ¬ 𝐿 = 𝑘))))
172171com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ℕ0 → (𝑠 < 𝐿 → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))))
173172imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 ∈ ℕ0𝑠 < 𝐿) → (𝜑 → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘)))
174173impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))
175174adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) → ¬ 𝐿 = 𝑘))
176175imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → ¬ 𝐿 = 𝑘)
177176iffalsed 4254 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) ∧ 𝑘 ∈ (0...𝑠)) → if(𝐿 = 𝑘, 𝐴, 0 ) = 0 )
178142, 177mpteq2da 4902 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ 0 ))
179178oveq2d 6858 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )))
180 ringmnd 18823 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
18130, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ∈ Mnd)
182181adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → 𝑅 ∈ Mnd)
183 ovex 6874 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝑠) ∈ V
18412gsumz 17640 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ Mnd ∧ (0...𝑠) ∈ V) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
185182, 183, 184sylancl 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
186185adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ 0 )) = 0 )
187 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 / 𝑘𝐴 = 0𝐿 / 𝑘𝐴 = 0 )
188187eqcomd 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 / 𝑘𝐴 = 00 = 𝐿 / 𝑘𝐴)
189188adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → 0 = 𝐿 / 𝑘𝐴)
190179, 186, 1893eqtrd 2803 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) ∧ 𝐿 / 𝑘𝐴 = 0 ) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
191190ex 401 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑠 ∈ ℕ0𝑠 < 𝐿)) → (𝐿 / 𝑘𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
192191expr 448 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ ℕ0) → (𝑠 < 𝐿 → (𝐿 / 𝑘𝐴 = 0 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))
193192a2d 29 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ ℕ0) → ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))
194193ex 401 . . . . . . . . . . . . . . 15 (𝜑 → (𝑠 ∈ ℕ0 → ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
195194com13 88 . . . . . . . . . . . . . 14 ((𝑠 < 𝐿𝐿 / 𝑘𝐴 = 0 ) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
196138, 195syl 17 . . . . . . . . . . . . 13 ((𝐿 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
197196ex 401 . . . . . . . . . . . 12 (𝐿 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 ∈ ℕ0 → (𝜑 → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))))
198197com24 95 . . . . . . . . . . 11 (𝐿 ∈ ℕ0 → (𝜑 → (𝑠 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)))))
19999, 198mpcom 38 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))))
200199imp31 408 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑠 < 𝐿 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
201200com12 32 . . . . . . . 8 (𝑠 < 𝐿 → (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
202 pm3.2 461 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ0) → (¬ 𝑠 < 𝐿 → ((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿)))
203202adantr 472 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (¬ 𝑠 < 𝐿 → ((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿)))
204181ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → 𝑅 ∈ Mnd)
205183a1i 11 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → (0...𝑠) ∈ V)
20699nn0red 11599 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ℝ)
207 lenlt 10370 . . . . . . . . . . . . 13 ((𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝐿𝑠 ↔ ¬ 𝑠 < 𝐿))
208206, 146, 207syl2an 589 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ0) → (𝐿𝑠 ↔ ¬ 𝑠 < 𝐿))
20999ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿 ∈ ℕ0)
210 simplr 785 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝑠 ∈ ℕ0)
211 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿𝑠)
212 elfz2nn0 12638 . . . . . . . . . . . . . 14 (𝐿 ∈ (0...𝑠) ↔ (𝐿 ∈ ℕ0𝑠 ∈ ℕ0𝐿𝑠))
213209, 210, 211, 212syl3anbrc 1443 . . . . . . . . . . . . 13 (((𝜑𝑠 ∈ ℕ0) ∧ 𝐿𝑠) → 𝐿 ∈ (0...𝑠))
214213ex 401 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ0) → (𝐿𝑠𝐿 ∈ (0...𝑠)))
215208, 214sylbird 251 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → (¬ 𝑠 < 𝐿𝐿 ∈ (0...𝑠)))
216215imp 395 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → 𝐿 ∈ (0...𝑠))
217 eqcom 2772 . . . . . . . . . . . 12 (𝐿 = 𝑘𝑘 = 𝐿)
218 ifbi 4264 . . . . . . . . . . . 12 ((𝐿 = 𝑘𝑘 = 𝐿) → if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 ))
219217, 218ax-mp 5 . . . . . . . . . . 11 if(𝐿 = 𝑘, 𝐴, 0 ) = if(𝑘 = 𝐿, 𝐴, 0 )
220219mpteq2i 4900 . . . . . . . . . 10 (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 )) = (𝑘 ∈ (0...𝑠) ↦ if(𝑘 = 𝐿, 𝐴, 0 ))
2213, 5syl6eleq 2854 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → 𝐴 ∈ (Base‘𝑅))
222221ex 401 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ ℕ0𝐴 ∈ (Base‘𝑅)))
223222adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ ℕ0) → (𝑘 ∈ ℕ0𝐴 ∈ (Base‘𝑅)))
224223, 101impel 501 . . . . . . . . . . . 12 (((𝜑𝑠 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑠)) → 𝐴 ∈ (Base‘𝑅))
225224ralrimiva 3113 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ0) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅))
226225adantr 472 . . . . . . . . . 10 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → ∀𝑘 ∈ (0...𝑠)𝐴 ∈ (Base‘𝑅))
22712, 204, 205, 216, 220, 226gsummpt1n0 18630 . . . . . . . . 9 (((𝜑𝑠 ∈ ℕ0) ∧ ¬ 𝑠 < 𝐿) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
228203, 227syl6com 37 . . . . . . . 8 𝑠 < 𝐿 → (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴))
229201, 228pm2.61i 176 . . . . . . 7 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ if(𝐿 = 𝑘, 𝐴, 0 ))) = 𝐿 / 𝑘𝐴)
230133, 229eqtrd 2799 . . . . . 6 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ ((coe1‘(𝐴 (𝑘 𝑋)))‘𝐿))) = 𝐿 / 𝑘𝐴)
23197, 110, 2303eqtrd 2803 . . . . 5 (((𝜑𝑠 ∈ ℕ0) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 )) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴)
232231ex 401 . . . 4 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥𝑥 / 𝑘𝐴 = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
23327, 232syld 47 . . 3 ((𝜑𝑠 ∈ ℕ0) → (∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
234233rexlimdva 3178 . 2 (𝜑 → (∃𝑠 ∈ ℕ0𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ((𝑘 ∈ ℕ0𝐴)‘𝑥) = 0 ) → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴))
23516, 234mpd 15 1 (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ (𝐴 (𝑘 𝑋)))))‘𝐿) = 𝐿 / 𝑘𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  csb 3691  ifcif 4243   class class class wbr 4809  cmpt 4888  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060   finSupp cfsupp 8482  cr 10188  0cc0 10189   < clt 10328  cle 10329  0cn0 11538  ...cfz 12533  Basecbs 16130  Scalarcsca 16217   ·𝑠 cvsca 16218  0gc0g 16366   Σg cgsu 16367  Mndcmnd 17560  .gcmg 17807  CMndccmn 18459  mulGrpcmgp 18756  Ringcrg 18814  LModclmod 19132  var1cv1 19819  Poly1cpl1 19820  coe1cco1 19821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-ofr 7096  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-fz 12534  df-fzo 12674  df-seq 13009  df-hash 13322  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-sca 16230  df-vsca 16231  df-tset 16233  df-ple 16234  df-0g 16368  df-gsum 16369  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-mhm 17601  df-submnd 17602  df-grp 17692  df-minusg 17693  df-sbg 17694  df-mulg 17808  df-subg 17855  df-ghm 17922  df-cntz 18013  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-subrg 19047  df-lmod 19134  df-lss 19202  df-psr 19630  df-mvr 19631  df-mpl 19632  df-opsr 19634  df-psr1 19823  df-vr1 19824  df-ply1 19825  df-coe1 19826
This theorem is referenced by:  gsumply1eq  19948  pm2mpf1lem  20878  pm2mpcoe1  20884  pm2mpmhmlem2  20903  cayleyhamilton1  20976  ply1mulgsum  42847
  Copyright terms: Public domain W3C validator