Metamath Proof Explorer

Theorem ply1mulgsumlem2

Description: Lemma 2 for ply1mulgsum . (Contributed by AV, 19-Oct-2019)

Ref Expression
Hypotheses 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 ply1mulgsumlem2 ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 ply1mulgsum.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1mulgsum.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 ply1mulgsum.a ⊢ 𝐴 = ( coe1 ‘ 𝐾 )
4 ply1mulgsum.c ⊢ 𝐶 = ( coe1 ‘ 𝐿 )
5 ply1mulgsum.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 ply1mulgsum.pm ⊢ × = ( .r ‘ 𝑃 )
7 ply1mulgsum.sm ⊢ · = ( ·𝑠 ‘ 𝑃 )
8 ply1mulgsum.rm ⊢ ∗ = ( .r ‘ 𝑅 )
9 ply1mulgsum.m ⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
10 ply1mulgsum.e ⊢ ↑ = ( .g ‘ 𝑀 )
11 1 2 3 4 5 6 7 8 9 10 ply1mulgsumlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑧 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) )
12 2nn0 ⊢ 2 ∈ ℕ0
13 12 a1i ⊢ ( 𝑧 ∈ ℕ0 → 2 ∈ ℕ0 )
14 id ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℕ0 )
15 13 14 nn0mulcld ⊢ ( 𝑧 ∈ ℕ0 → ( 2 · 𝑧 ) ∈ ℕ0 )
16 15 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( 2 · 𝑧 ) ∈ ℕ0 )
17 breq1 ⊢ ( 𝑠 = ( 2 · 𝑧 ) → ( 𝑠 < 𝑛 ↔ ( 2 · 𝑧 ) < 𝑛 ) )
18 17 imbi1d ⊢ ( 𝑠 = ( 2 · 𝑧 ) → ( ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
19 18 ralbidv ⊢ ( 𝑠 = ( 2 · 𝑧 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
20 19 adantl ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑠 = ( 2 · 𝑧 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ ( 𝑧 ∈ ℕ0 → 2 ∈ ℝ )
23 nn0re ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℝ )
24 22 23 remulcld ⊢ ( 𝑧 ∈ ℕ0 → ( 2 · 𝑧 ) ∈ ℝ )
25 24 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 2 · 𝑧 ) ∈ ℝ )
26 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝑛 ∈ ℝ )
29 elfznn0 ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → 𝑙 ∈ ℕ0 )
30 nn0re ⊢ ( 𝑙 ∈ ℕ0 → 𝑙 ∈ ℝ )
31 29 30 syl ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → 𝑙 ∈ ℝ )
32 31 adantl ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝑙 ∈ ℝ )
33 25 28 32 ltsub1d ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 2 · 𝑧 ) < 𝑛 ↔ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) )
34 23 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝑧 ∈ ℝ )
35 32 34 25 lesub2d ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑙 ≤ 𝑧 ↔ ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) ) )
36 35 adantr ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → ( 𝑙 ≤ 𝑧 ↔ ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) ) )
37 24 23 resubcld ⊢ ( 𝑧 ∈ ℕ0 → ( ( 2 · 𝑧 ) − 𝑧 ) ∈ ℝ )
38 37 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 2 · 𝑧 ) − 𝑧 ) ∈ ℝ )
39 24 adantr ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑧 ) ∈ ℝ )
40 resubcl ⊢ ( ( ( 2 · 𝑧 ) ∈ ℝ ∧ 𝑙 ∈ ℝ ) → ( ( 2 · 𝑧 ) − 𝑙 ) ∈ ℝ )
41 39 31 40 syl2an ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 2 · 𝑧 ) − 𝑙 ) ∈ ℝ )
42 resubcl ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → ( 𝑛 − 𝑙 ) ∈ ℝ )
43 27 31 42 syl2an ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛 − 𝑙 ) ∈ ℝ )
44 lelttr ⊢ ( ( ( ( 2 · 𝑧 ) − 𝑧 ) ∈ ℝ ∧ ( ( 2 · 𝑧 ) − 𝑙 ) ∈ ℝ ∧ ( 𝑛 − 𝑙 ) ∈ ℝ ) → ( ( ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → ( ( 2 · 𝑧 ) − 𝑧 ) < ( 𝑛 − 𝑙 ) ) )
45 38 41 43 44 syl3anc ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → ( ( 2 · 𝑧 ) − 𝑧 ) < ( 𝑛 − 𝑙 ) ) )
46 nn0cn ⊢ ( 𝑧 ∈ ℕ0 → 𝑧 ∈ ℂ )
47 2txmxeqx ⊢ ( 𝑧 ∈ ℂ → ( ( 2 · 𝑧 ) − 𝑧 ) = 𝑧 )
48 46 47 syl ⊢ ( 𝑧 ∈ ℕ0 → ( ( 2 · 𝑧 ) − 𝑧 ) = 𝑧 )
49 48 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 2 · 𝑧 ) − 𝑧 ) = 𝑧 )
50 49 breq1d ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 2 · 𝑧 ) − 𝑧 ) < ( 𝑛 − 𝑙 ) ↔ 𝑧 < ( 𝑛 − 𝑙 ) ) )
51 45 50 sylibd ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → 𝑧 < ( 𝑛 − 𝑙 ) ) )
52 51 expcomd ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) → ( ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) → 𝑧 < ( 𝑛 − 𝑙 ) ) ) )
53 52 imp ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → ( ( ( 2 · 𝑧 ) − 𝑧 ) ≤ ( ( 2 · 𝑧 ) − 𝑙 ) → 𝑧 < ( 𝑛 − 𝑙 ) ) )
54 36 53 sylbid ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ∧ ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) )
55 54 ex ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( ( 2 · 𝑧 ) − 𝑙 ) < ( 𝑛 − 𝑙 ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) )
56 33 55 sylbid ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) )
57 56 ex ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) ) )
58 57 com23 ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) ) )
59 58 ex ⊢ ( 𝑧 ∈ ℕ0 → ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) ) ) )
60 59 ad2antrr ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) ) ) ) )
61 60 imp41 ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑙 ≤ 𝑧 → 𝑧 < ( 𝑛 − 𝑙 ) ) )
62 61 impcom ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → 𝑧 < ( 𝑛 − 𝑙 ) )
63 fznn0sub2 ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑙 ) ∈ ( 0 ... 𝑛 ) )
64 elfznn0 ⊢ ( ( 𝑛 − 𝑙 ) ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑙 ) ∈ ℕ0 )
65 breq2 ⊢ ( 𝑥 = ( 𝑛 − 𝑙 ) → ( 𝑧 < 𝑥 ↔ 𝑧 < ( 𝑛 − 𝑙 ) ) )
66 fveqeq2 ⊢ ( 𝑥 = ( 𝑛 − 𝑙 ) → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐴 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) )
67 fveqeq2 ⊢ ( 𝑥 = ( 𝑛 − 𝑙 ) → ( ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) )
68 66 67 anbi12d ⊢ ( 𝑥 = ( 𝑛 − 𝑙 ) → ( ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( 𝐴 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
69 65 68 imbi12d ⊢ ( 𝑥 = ( 𝑛 − 𝑙 ) → ( ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ( 𝑧 < ( 𝑛 − 𝑙 ) → ( ( 𝐴 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) ) )
70 69 rspcva ⊢ ( ( ( 𝑛 − 𝑙 ) ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( ( 𝐴 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
71 simpr ⊢ ( ( ( 𝐴 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) )
72 70 71 syl6 ⊢ ( ( ( 𝑛 − 𝑙 ) ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) )
73 72 ex ⊢ ( ( 𝑛 − 𝑙 ) ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
74 63 64 73 3syl ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
75 74 com12 ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
76 75 ad4antlr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) ) )
77 76 imp ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) )
78 77 adantl ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝑧 < ( 𝑛 − 𝑙 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) ) )
79 62 78 mpd ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 0g ‘ 𝑅 ) )
80 79 oveq2d ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( ( 𝐴 ‘ 𝑙 ) ∗ ( 0g ‘ 𝑅 ) ) )
81 simplr1 ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
82 81 ad2antrr ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → 𝑅 ∈ Ring )
83 82 adantl ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → 𝑅 ∈ Ring )
84 simplr2 ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐾 ∈ 𝐵 )
85 84 adantr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → 𝐾 ∈ 𝐵 )
86 85 29 anim12i ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0 ) )
87 86 adantl ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0 ) )
88 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
89 3 2 1 88 coe1fvalcl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
90 87 89 syl ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
91 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
92 88 8 91 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
93 83 90 92 syl2anc ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
94 80 93 eqtrd ⊢ ( ( 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( 0g ‘ 𝑅 ) )
95 ltnle ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑙 ∈ ℝ ) → ( 𝑧 < 𝑙 ↔ ¬ 𝑙 ≤ 𝑧 ) )
96 23 30 95 syl2an ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑙 ∈ ℕ0 ) → ( 𝑧 < 𝑙 ↔ ¬ 𝑙 ≤ 𝑧 ) )
97 96 bicomd ⊢ ( ( 𝑧 ∈ ℕ0 ∧ 𝑙 ∈ ℕ0 ) → ( ¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙 ) )
98 97 expcom ⊢ ( 𝑙 ∈ ℕ0 → ( 𝑧 ∈ ℕ0 → ( ¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙 ) ) )
99 98 29 syl11 ⊢ ( 𝑧 ∈ ℕ0 → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( ¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙 ) ) )
100 99 ad4antr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( ¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙 ) ) )
101 100 imp ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ¬ 𝑙 ≤ 𝑧 ↔ 𝑧 < 𝑙 ) )
102 breq2 ⊢ ( 𝑥 = 𝑙 → ( 𝑧 < 𝑥 ↔ 𝑧 < 𝑙 ) )
103 fveqeq2 ⊢ ( 𝑥 = 𝑙 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
104 fveqeq2 ⊢ ( 𝑥 = 𝑙 → ( ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐶 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
105 103 104 anbi12d ⊢ ( 𝑥 = 𝑙 → ( ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) )
106 102 105 imbi12d ⊢ ( 𝑥 = 𝑙 → ( ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ↔ ( 𝑧 < 𝑙 → ( ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) ) )
107 106 rspcva ⊢ ( ( 𝑙 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑧 < 𝑙 → ( ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) )
108 simpl ⊢ ( ( ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) )
109 107 108 syl6 ⊢ ( ( 𝑙 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑧 < 𝑙 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
110 109 ex ⊢ ( 𝑙 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑧 < 𝑙 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) )
111 110 29 syl11 ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑧 < 𝑙 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) )
112 111 ad4antlr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑧 < 𝑙 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) ) )
113 112 imp ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝑧 < 𝑙 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
114 101 113 sylbid ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ¬ 𝑙 ≤ 𝑧 → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) ) )
115 114 impcom ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐴 ‘ 𝑙 ) = ( 0g ‘ 𝑅 ) )
116 115 oveq1d ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( ( 0g ‘ 𝑅 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) )
117 82 adantl ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → 𝑅 ∈ Ring )
118 simplr3 ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐿 ∈ 𝐵 )
119 118 adantr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → 𝐿 ∈ 𝐵 )
120 fznn0sub ⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑙 ) ∈ ℕ0 )
121 119 120 anim12i ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( 𝐿 ∈ 𝐵 ∧ ( 𝑛 − 𝑙 ) ∈ ℕ0 ) )
122 121 adantl ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐿 ∈ 𝐵 ∧ ( 𝑛 − 𝑙 ) ∈ ℕ0 ) )
123 4 2 1 88 coe1fvalcl ⊢ ( ( 𝐿 ∈ 𝐵 ∧ ( 𝑛 − 𝑙 ) ∈ ℕ0 ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
124 122 123 syl ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
125 88 8 91 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( 0g ‘ 𝑅 ) )
126 117 124 125 syl2anc ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 0g ‘ 𝑅 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( 0g ‘ 𝑅 ) )
127 116 126 eqtrd ⊢ ( ( ¬ 𝑙 ≤ 𝑧 ∧ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( 0g ‘ 𝑅 ) )
128 94 127 pm2.61ian ⊢ ( ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) ∧ 𝑙 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( 0g ‘ 𝑅 ) )
129 128 mpteq2dva ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( 0g ‘ 𝑅 ) ) )
130 129 oveq2d ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( 0g ‘ 𝑅 ) ) ) )
131 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
132 131 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑅 ∈ Mnd )
133 ovex ⊢ ( 0 ... 𝑛 ) ∈ V
134 132 133 jctir ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑛 ) ∈ V ) )
135 134 ad3antlr ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑛 ) ∈ V ) )
136 91 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑛 ) ∈ V ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
137 135 136 syl ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
138 130 137 eqtrd ⊢ ( ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 2 · 𝑧 ) < 𝑛 ) → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) )
139 138 ex ⊢ ( ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
140 139 ralrimiva ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ∀ 𝑛 ∈ ℕ0 ( ( 2 · 𝑧 ) < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
141 16 20 140 rspcedvd ⊢ ( ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) ∧ ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )
142 141 ex ⊢ ( ( 𝑧 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
143 142 rexlimiva ⊢ ( ∃ 𝑧 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑧 < 𝑥 → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝐶 ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) ) )
144 11 143 mpcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑅 Σg ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 0g ‘ 𝑅 ) ) )