Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ply1mulgsumlem2 Structured version   Visualization version   GIF version

Theorem ply1mulgsumlem2 46458
Description: Lemma 2 for ply1mulgsum 46461. (Contributed by AV, 19-Oct-2019.)
Hypotheses
Ref Expression
ply1mulgsum.p 𝑃 = (Poly1𝑅)
ply1mulgsum.b 𝐵 = (Base‘𝑃)
ply1mulgsum.a 𝐴 = (coe1𝐾)
ply1mulgsum.c 𝐶 = (coe1𝐿)
ply1mulgsum.x 𝑋 = (var1𝑅)
ply1mulgsum.pm × = (.r𝑃)
ply1mulgsum.sm · = ( ·𝑠𝑃)
ply1mulgsum.rm = (.r𝑅)
ply1mulgsum.m 𝑀 = (mulGrp‘𝑃)
ply1mulgsum.e = (.g𝑀)
Assertion
Ref Expression
ply1mulgsumlem2 ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → ∃𝑠 ∈ ℕ0𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)))
Distinct variable groups:   𝐴,𝑛,𝑠   𝐵,𝑛,𝑠   𝐶,𝑛,𝑠   𝑛,𝐾,𝑠   𝑛,𝐿,𝑠   𝑅,𝑛,𝑠   𝐴,𝑙,𝑛   𝐵,𝑙   𝐶,𝑙   𝐾,𝑙   𝐿,𝑙   𝑅,𝑙,𝑠   ,𝑠
Allowed substitution hints:   𝑃(𝑛,𝑠,𝑙)   · (𝑛,𝑠,𝑙)   × (𝑛,𝑠,𝑙)   (𝑛,𝑠,𝑙)   (𝑛,𝑙)   𝑀(𝑛,𝑠,𝑙)   𝑋(𝑛,𝑠,𝑙)

Proof of Theorem ply1mulgsumlem2
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ply1mulgsum.p . . 3 𝑃 = (Poly1𝑅)
2 ply1mulgsum.b . . 3 𝐵 = (Base‘𝑃)
3 ply1mulgsum.a . . 3 𝐴 = (coe1𝐾)
4 ply1mulgsum.c . . 3 𝐶 = (coe1𝐿)
5 ply1mulgsum.x . . 3 𝑋 = (var1𝑅)
6 ply1mulgsum.pm . . 3 × = (.r𝑃)
7 ply1mulgsum.sm . . 3 · = ( ·𝑠𝑃)
8 ply1mulgsum.rm . . 3 = (.r𝑅)
9 ply1mulgsum.m . . 3 𝑀 = (mulGrp‘𝑃)
10 ply1mulgsum.e . . 3 = (.g𝑀)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10ply1mulgsumlem1 46457 . 2 ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → ∃𝑧 ∈ ℕ0𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))))
12 2nn0 12430 . . . . . . . 8 2 ∈ ℕ0
1312a1i 11 . . . . . . 7 (𝑧 ∈ ℕ0 → 2 ∈ ℕ0)
14 id 22 . . . . . . 7 (𝑧 ∈ ℕ0𝑧 ∈ ℕ0)
1513, 14nn0mulcld 12478 . . . . . 6 (𝑧 ∈ ℕ0 → (2 · 𝑧) ∈ ℕ0)
1615ad2antrr 724 . . . . 5 (((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) → (2 · 𝑧) ∈ ℕ0)
17 breq1 5108 . . . . . . . 8 (𝑠 = (2 · 𝑧) → (𝑠 < 𝑛 ↔ (2 · 𝑧) < 𝑛))
1817imbi1d 341 . . . . . . 7 (𝑠 = (2 · 𝑧) → ((𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)) ↔ ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))))
1918ralbidv 3174 . . . . . 6 (𝑠 = (2 · 𝑧) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)) ↔ ∀𝑛 ∈ ℕ0 ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))))
2019adantl 482 . . . . 5 ((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑠 = (2 · 𝑧)) → (∀𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)) ↔ ∀𝑛 ∈ ℕ0 ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))))
21 2re 12227 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
2221a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℕ0 → 2 ∈ ℝ)
23 nn0re 12422 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ℕ0𝑧 ∈ ℝ)
2422, 23remulcld 11185 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ ℕ0 → (2 · 𝑧) ∈ ℝ)
2524ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (2 · 𝑧) ∈ ℝ)
26 nn0re 12422 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
2726adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) → 𝑛 ∈ ℝ)
2827adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑛 ∈ ℝ)
29 elfznn0 13534 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℕ0)
30 nn0re 12422 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 ∈ ℕ0𝑙 ∈ ℝ)
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ (0...𝑛) → 𝑙 ∈ ℝ)
3231adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑙 ∈ ℝ)
3325, 28, 32ltsub1d 11764 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) < 𝑛 ↔ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)))
3423ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → 𝑧 ∈ ℝ)
3532, 34, 25lesub2d 11763 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑙𝑧 ↔ ((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙)))
3635adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → (𝑙𝑧 ↔ ((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙)))
3724, 23resubcld 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ ℕ0 → ((2 · 𝑧) − 𝑧) ∈ ℝ)
3837ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑧) ∈ ℝ)
3924adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑧) ∈ ℝ)
40 resubcl 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑧) ∈ ℝ ∧ 𝑙 ∈ ℝ) → ((2 · 𝑧) − 𝑙) ∈ ℝ)
4139, 31, 40syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑙) ∈ ℝ)
42 resubcl 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑛𝑙) ∈ ℝ)
4327, 31, 42syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (𝑛𝑙) ∈ ℝ)
44 lelttr 11245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((2 · 𝑧) − 𝑧) ∈ ℝ ∧ ((2 · 𝑧) − 𝑙) ∈ ℝ ∧ (𝑛𝑙) ∈ ℝ) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → ((2 · 𝑧) − 𝑧) < (𝑛𝑙)))
4538, 41, 43, 44syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → ((2 · 𝑧) − 𝑧) < (𝑛𝑙)))
46 nn0cn 12423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ ℕ0𝑧 ∈ ℂ)
47 2txmxeqx 12293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ ℂ → ((2 · 𝑧) − 𝑧) = 𝑧)
4846, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ ℕ0 → ((2 · 𝑧) − 𝑧) = 𝑧)
4948ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) − 𝑧) = 𝑧)
5049breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑧) < (𝑛𝑙) ↔ 𝑧 < (𝑛𝑙)))
5145, 50sylibd 238 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → 𝑧 < (𝑛𝑙)))
5251expcomd 417 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑙) < (𝑛𝑙) → (((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) → 𝑧 < (𝑛𝑙))))
5352imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → (((2 · 𝑧) − 𝑧) ≤ ((2 · 𝑧) − 𝑙) → 𝑧 < (𝑛𝑙)))
5436, 53sylbid 239 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) ∧ ((2 · 𝑧) − 𝑙) < (𝑛𝑙)) → (𝑙𝑧𝑧 < (𝑛𝑙)))
5554ex 413 . . . . . . . . . . . . . . . . . . . . 21 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → (((2 · 𝑧) − 𝑙) < (𝑛𝑙) → (𝑙𝑧𝑧 < (𝑛𝑙))))
5633, 55sylbid 239 . . . . . . . . . . . . . . . . . . . 20 (((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑛)) → ((2 · 𝑧) < 𝑛 → (𝑙𝑧𝑧 < (𝑛𝑙))))
5756ex 413 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) → (𝑙 ∈ (0...𝑛) → ((2 · 𝑧) < 𝑛 → (𝑙𝑧𝑧 < (𝑛𝑙)))))
5857com23 86 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ ℕ0𝑛 ∈ ℕ0) → ((2 · 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙𝑧𝑧 < (𝑛𝑙)))))
5958ex 413 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0 → (𝑛 ∈ ℕ0 → ((2 · 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙𝑧𝑧 < (𝑛𝑙))))))
6059ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) → (𝑛 ∈ ℕ0 → ((2 · 𝑧) < 𝑛 → (𝑙 ∈ (0...𝑛) → (𝑙𝑧𝑧 < (𝑛𝑙))))))
6160imp41 426 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑙𝑧𝑧 < (𝑛𝑙)))
6261impcom 408 . . . . . . . . . . . . . 14 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑧 < (𝑛𝑙))
63 fznn0sub2 13548 . . . . . . . . . . . . . . . . . . 19 (𝑙 ∈ (0...𝑛) → (𝑛𝑙) ∈ (0...𝑛))
64 elfznn0 13534 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑙) ∈ (0...𝑛) → (𝑛𝑙) ∈ ℕ0)
65 breq2 5109 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑛𝑙) → (𝑧 < 𝑥𝑧 < (𝑛𝑙)))
66 fveqeq2 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑛𝑙) → ((𝐴𝑥) = (0g𝑅) ↔ (𝐴‘(𝑛𝑙)) = (0g𝑅)))
67 fveqeq2 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑛𝑙) → ((𝐶𝑥) = (0g𝑅) ↔ (𝐶‘(𝑛𝑙)) = (0g𝑅)))
6866, 67anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑛𝑙) → (((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)) ↔ ((𝐴‘(𝑛𝑙)) = (0g𝑅) ∧ (𝐶‘(𝑛𝑙)) = (0g𝑅))))
6965, 68imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑛𝑙) → ((𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) ↔ (𝑧 < (𝑛𝑙) → ((𝐴‘(𝑛𝑙)) = (0g𝑅) ∧ (𝐶‘(𝑛𝑙)) = (0g𝑅)))))
7069rspcva 3579 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛𝑙) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) → (𝑧 < (𝑛𝑙) → ((𝐴‘(𝑛𝑙)) = (0g𝑅) ∧ (𝐶‘(𝑛𝑙)) = (0g𝑅))))
71 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴‘(𝑛𝑙)) = (0g𝑅) ∧ (𝐶‘(𝑛𝑙)) = (0g𝑅)) → (𝐶‘(𝑛𝑙)) = (0g𝑅))
7270, 71syl6 35 . . . . . . . . . . . . . . . . . . . 20 (((𝑛𝑙) ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅)))
7372ex 413 . . . . . . . . . . . . . . . . . . 19 ((𝑛𝑙) ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅))))
7463, 64, 733syl 18 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ (0...𝑛) → (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅))))
7574com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → (𝑙 ∈ (0...𝑛) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅))))
7675ad4antlr 731 . . . . . . . . . . . . . . . 16 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅))))
7776imp 407 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅)))
7877adantl 482 . . . . . . . . . . . . . 14 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝑧 < (𝑛𝑙) → (𝐶‘(𝑛𝑙)) = (0g𝑅)))
7962, 78mpd 15 . . . . . . . . . . . . 13 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐶‘(𝑛𝑙)) = (0g𝑅))
8079oveq2d 7373 . . . . . . . . . . . 12 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴𝑙) (𝐶‘(𝑛𝑙))) = ((𝐴𝑙) (0g𝑅)))
81 simplr1 1215 . . . . . . . . . . . . . . 15 ((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring)
8281ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → 𝑅 ∈ Ring)
8382adantl 482 . . . . . . . . . . . . 13 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑅 ∈ Ring)
84 simplr2 1216 . . . . . . . . . . . . . . . . 17 ((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐾𝐵)
8584adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → 𝐾𝐵)
8685, 29anim12i 613 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝐾𝐵𝑙 ∈ ℕ0))
8786adantl 482 . . . . . . . . . . . . . 14 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐾𝐵𝑙 ∈ ℕ0))
88 eqid 2736 . . . . . . . . . . . . . . 15 (Base‘𝑅) = (Base‘𝑅)
893, 2, 1, 88coe1fvalcl 21583 . . . . . . . . . . . . . 14 ((𝐾𝐵𝑙 ∈ ℕ0) → (𝐴𝑙) ∈ (Base‘𝑅))
9087, 89syl 17 . . . . . . . . . . . . 13 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐴𝑙) ∈ (Base‘𝑅))
91 eqid 2736 . . . . . . . . . . . . . 14 (0g𝑅) = (0g𝑅)
9288, 8, 91ringrz 20012 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝐴𝑙) ∈ (Base‘𝑅)) → ((𝐴𝑙) (0g𝑅)) = (0g𝑅))
9383, 90, 92syl2anc 584 . . . . . . . . . . . 12 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴𝑙) (0g𝑅)) = (0g𝑅))
9480, 93eqtrd 2776 . . . . . . . . . . 11 ((𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴𝑙) (𝐶‘(𝑛𝑙))) = (0g𝑅))
95 ltnle 11234 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑧 < 𝑙 ↔ ¬ 𝑙𝑧))
9623, 30, 95syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ ℕ0𝑙 ∈ ℕ0) → (𝑧 < 𝑙 ↔ ¬ 𝑙𝑧))
9796bicomd 222 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ ℕ0𝑙 ∈ ℕ0) → (¬ 𝑙𝑧𝑧 < 𝑙))
9897expcom 414 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ ℕ0 → (𝑧 ∈ ℕ0 → (¬ 𝑙𝑧𝑧 < 𝑙)))
9998, 29syl11 33 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0 → (𝑙 ∈ (0...𝑛) → (¬ 𝑙𝑧𝑧 < 𝑙)))
10099ad4antr 730 . . . . . . . . . . . . . . . 16 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (¬ 𝑙𝑧𝑧 < 𝑙)))
101100imp 407 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (¬ 𝑙𝑧𝑧 < 𝑙))
102 breq2 5109 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑙 → (𝑧 < 𝑥𝑧 < 𝑙))
103 fveqeq2 6851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑙 → ((𝐴𝑥) = (0g𝑅) ↔ (𝐴𝑙) = (0g𝑅)))
104 fveqeq2 6851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑙 → ((𝐶𝑥) = (0g𝑅) ↔ (𝐶𝑙) = (0g𝑅)))
105103, 104anbi12d 631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑙 → (((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)) ↔ ((𝐴𝑙) = (0g𝑅) ∧ (𝐶𝑙) = (0g𝑅))))
106102, 105imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑙 → ((𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) ↔ (𝑧 < 𝑙 → ((𝐴𝑙) = (0g𝑅) ∧ (𝐶𝑙) = (0g𝑅)))))
107106rspcva 3579 . . . . . . . . . . . . . . . . . . . 20 ((𝑙 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) → (𝑧 < 𝑙 → ((𝐴𝑙) = (0g𝑅) ∧ (𝐶𝑙) = (0g𝑅))))
108 simpl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑙) = (0g𝑅) ∧ (𝐶𝑙) = (0g𝑅)) → (𝐴𝑙) = (0g𝑅))
109107, 108syl6 35 . . . . . . . . . . . . . . . . . . 19 ((𝑙 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) → (𝑧 < 𝑙 → (𝐴𝑙) = (0g𝑅)))
110109ex 413 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ ℕ0 → (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → (𝑧 < 𝑙 → (𝐴𝑙) = (0g𝑅))))
111110, 29syl11 33 . . . . . . . . . . . . . . . . 17 (∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → (𝑙 ∈ (0...𝑛) → (𝑧 < 𝑙 → (𝐴𝑙) = (0g𝑅))))
112111ad4antlr 731 . . . . . . . . . . . . . . . 16 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) → (𝑧 < 𝑙 → (𝐴𝑙) = (0g𝑅))))
113112imp 407 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝑧 < 𝑙 → (𝐴𝑙) = (0g𝑅)))
114101, 113sylbid 239 . . . . . . . . . . . . . 14 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (¬ 𝑙𝑧 → (𝐴𝑙) = (0g𝑅)))
115114impcom 408 . . . . . . . . . . . . 13 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐴𝑙) = (0g𝑅))
116115oveq1d 7372 . . . . . . . . . . . 12 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴𝑙) (𝐶‘(𝑛𝑙))) = ((0g𝑅) (𝐶‘(𝑛𝑙))))
11782adantl 482 . . . . . . . . . . . . 13 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → 𝑅 ∈ Ring)
118 simplr3 1217 . . . . . . . . . . . . . . . . 17 ((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) → 𝐿𝐵)
119118adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → 𝐿𝐵)
120 fznn0sub 13473 . . . . . . . . . . . . . . . 16 (𝑙 ∈ (0...𝑛) → (𝑛𝑙) ∈ ℕ0)
121119, 120anim12i 613 . . . . . . . . . . . . . . 15 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → (𝐿𝐵 ∧ (𝑛𝑙) ∈ ℕ0))
122121adantl 482 . . . . . . . . . . . . . 14 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐿𝐵 ∧ (𝑛𝑙) ∈ ℕ0))
1234, 2, 1, 88coe1fvalcl 21583 . . . . . . . . . . . . . 14 ((𝐿𝐵 ∧ (𝑛𝑙) ∈ ℕ0) → (𝐶‘(𝑛𝑙)) ∈ (Base‘𝑅))
124122, 123syl 17 . . . . . . . . . . . . 13 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → (𝐶‘(𝑛𝑙)) ∈ (Base‘𝑅))
12588, 8, 91ringlz 20011 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝐶‘(𝑛𝑙)) ∈ (Base‘𝑅)) → ((0g𝑅) (𝐶‘(𝑛𝑙))) = (0g𝑅))
126117, 124, 125syl2anc 584 . . . . . . . . . . . 12 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((0g𝑅) (𝐶‘(𝑛𝑙))) = (0g𝑅))
127116, 126eqtrd 2776 . . . . . . . . . . 11 ((¬ 𝑙𝑧 ∧ (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛))) → ((𝐴𝑙) (𝐶‘(𝑛𝑙))) = (0g𝑅))
12894, 127pm2.61ian 810 . . . . . . . . . 10 ((((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) ∧ 𝑙 ∈ (0...𝑛)) → ((𝐴𝑙) (𝐶‘(𝑛𝑙))) = (0g𝑅))
129128mpteq2dva 5205 . . . . . . . . 9 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙)))) = (𝑙 ∈ (0...𝑛) ↦ (0g𝑅)))
130129oveq2d 7373 . . . . . . . 8 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ (0g𝑅))))
131 ringmnd 19974 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
1321313ad2ant1 1133 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → 𝑅 ∈ Mnd)
133 ovex 7390 . . . . . . . . . . 11 (0...𝑛) ∈ V
134132, 133jctir 521 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → (𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V))
135134ad3antlr 729 . . . . . . . . 9 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V))
13691gsumz 18646 . . . . . . . . 9 ((𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ (0g𝑅))) = (0g𝑅))
137135, 136syl 17 . . . . . . . 8 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ (0g𝑅))) = (0g𝑅))
138130, 137eqtrd 2776 . . . . . . 7 (((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) ∧ (2 · 𝑧) < 𝑛) → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))
139138ex 413 . . . . . 6 ((((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)))
140139ralrimiva 3143 . . . . 5 (((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) → ∀𝑛 ∈ ℕ0 ((2 · 𝑧) < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)))
14116, 20, 140rspcedvd 3583 . . . 4 (((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) ∧ (𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵)) → ∃𝑠 ∈ ℕ0𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)))
142141ex 413 . . 3 ((𝑧 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅)))) → ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → ∃𝑠 ∈ ℕ0𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))))
143142rexlimiva 3144 . 2 (∃𝑧 ∈ ℕ0𝑥 ∈ ℕ0 (𝑧 < 𝑥 → ((𝐴𝑥) = (0g𝑅) ∧ (𝐶𝑥) = (0g𝑅))) → ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → ∃𝑠 ∈ ℕ0𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅))))
14411, 143mpcom 38 1 ((𝑅 ∈ Ring ∧ 𝐾𝐵𝐿𝐵) → ∃𝑠 ∈ ℕ0𝑛 ∈ ℕ0 (𝑠 < 𝑛 → (𝑅 Σg (𝑙 ∈ (0...𝑛) ↦ ((𝐴𝑙) (𝐶‘(𝑛𝑙))))) = (0g𝑅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  Vcvv 3445   class class class wbr 5105  cmpt 5188  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051   · cmul 11056   < clt 11189  cle 11190  cmin 11385  2c2 12208  0cn0 12413  ...cfz 13424  Basecbs 17083  .rcmulr 17134   ·𝑠 cvsca 17137  0gc0g 17321   Σg cgsu 17322  Mndcmnd 18556  .gcmg 18872  mulGrpcmgp 19896  Ringcrg 19964  var1cv1 21547  Poly1cpl1 21548  coe1cco1 21549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-seq 13907  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-tset 17152  df-ple 17153  df-0g 17323  df-gsum 17324  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751  df-minusg 18752  df-mgp 19897  df-ring 19966  df-psr 21311  df-mpl 21313  df-opsr 21315  df-psr1 21551  df-ply1 21553  df-coe1 21554
This theorem is referenced by:  ply1mulgsumlem3  46459  ply1mulgsumlem4  46460
  Copyright terms: Public domain W3C validator