Step |
Hyp |
Ref |
Expression |
1 |
|
gsummonply1.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
gsummonply1.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
gsummonply1.x |
⊢ 𝑋 = ( var1 ‘ 𝑅 ) |
4 |
|
gsummonply1.e |
⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) ) |
5 |
|
gsummonply1.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
6 |
|
gsummonply1.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
7 |
|
gsummonply1.m |
⊢ ∗ = ( ·𝑠 ‘ 𝑃 ) |
8 |
|
gsummonply1.0 |
⊢ 0 = ( 0g ‘ 𝑅 ) |
9 |
|
gsummonply1.a |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ) |
10 |
|
gsummonply1.f |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 ) |
11 |
|
gsummonply1.l |
⊢ ( 𝜑 → 𝐿 ∈ ℕ0 ) |
12 |
9
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 ) |
13 |
12
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 ) |
14 |
6
|
fvexi |
⊢ 𝐾 ∈ V |
15 |
14
|
a1i |
⊢ ( 𝜑 → 𝐾 ∈ V ) |
16 |
|
nn0ex |
⊢ ℕ0 ∈ V |
17 |
|
elmapg |
⊢ ( ( 𝐾 ∈ V ∧ ℕ0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 ) ) |
18 |
15 16 17
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ↔ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) : ℕ0 ⟶ 𝐾 ) ) |
19 |
13 18
|
mpbird |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ) |
20 |
8
|
fvexi |
⊢ 0 ∈ V |
21 |
|
fsuppmapnn0ub |
⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ∈ ( 𝐾 ↑m ℕ0 ) ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ) ) |
22 |
19 20 21
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ) ) |
23 |
10 22
|
mpd |
⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ) |
24 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 ) |
25 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ) |
26 |
|
rspcsbela |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) |
27 |
24 25 26
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) |
28 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) |
29 |
28
|
fvmpts |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ) |
30 |
24 27 29
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐴 ) |
31 |
30
|
eqeq1d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) |
32 |
31
|
imbi2d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ) |
33 |
32
|
biimpd |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ) |
34 |
33
|
ralimdva |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ) |
35 |
|
eqid |
⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) |
36 |
1
|
ply1ring |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
37 |
|
ringcmn |
⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd ) |
38 |
5 36 37
|
3syl |
⊢ ( 𝜑 → 𝑃 ∈ CMnd ) |
39 |
38
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑃 ∈ CMnd ) |
40 |
5
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑅 ∈ Ring ) |
41 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 ) |
42 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → 𝑘 ∈ ℕ0 ) |
43 |
|
eqid |
⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 ) |
44 |
6 1 3 7 43 4 2
|
ply1tmcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
45 |
40 41 42 44
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
46 |
45
|
3expia |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ∈ 𝐾 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) ) |
47 |
46
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) ) |
48 |
9 47
|
mpd |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
50 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑠 ∈ ℕ0 ) |
51 |
|
nfv |
⊢ Ⅎ 𝑘 𝑠 < 𝑥 |
52 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐴 |
53 |
52
|
nfeq1 |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 |
54 |
51 53
|
nfim |
⊢ Ⅎ 𝑘 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) |
55 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) |
56 |
|
breq2 |
⊢ ( 𝑥 = 𝑘 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝑘 ) ) |
57 |
|
csbeq1 |
⊢ ( 𝑥 = 𝑘 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = ⦋ 𝑘 / 𝑘 ⦌ 𝐴 ) |
58 |
57
|
eqeq1d |
⊢ ( 𝑥 = 𝑘 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ↔ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) ) |
59 |
56 58
|
imbi12d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) ) ) |
60 |
54 55 59
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) ) |
61 |
|
csbid |
⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 𝐴 |
62 |
61
|
eqeq1i |
⊢ ( ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ↔ 𝐴 = 0 ) |
63 |
|
oveq1 |
⊢ ( 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) ) |
64 |
1
|
ply1sca |
⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
65 |
5 64
|
syl |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
66 |
65
|
fveq2d |
⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) |
67 |
8 66
|
syl5eq |
⊢ ( 𝜑 → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) |
68 |
67
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) |
69 |
68
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) |
70 |
1
|
ply1lmod |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod ) |
71 |
5 70
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ LMod ) |
72 |
71
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod ) |
73 |
43
|
ringmgp |
⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd ) |
74 |
5 36 73
|
3syl |
⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd ) |
75 |
74
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd ) |
76 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 ) |
77 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
78 |
3 1 77
|
vr1cl |
⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
79 |
5 78
|
syl |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
80 |
79
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
81 |
43 77
|
mgpbas |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) ) |
82 |
81 4
|
mulgnn0cl |
⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
83 |
75 76 80 82
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
84 |
|
eqid |
⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 ) |
85 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) |
86 |
77 84 7 85 35
|
lmod0vs |
⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) |
87 |
72 83 86
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) |
88 |
69 87
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) |
89 |
63 88
|
sylan9eqr |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝐴 = 0 ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) |
90 |
89
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) |
91 |
62 90
|
syl5bi |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) |
92 |
91
|
imim2d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) |
93 |
92
|
ralimdva |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) |
94 |
60 93
|
syl5bi |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) ) |
95 |
94
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑠 < 𝑘 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) ) ) |
96 |
2 35 39 49 50 95
|
gsummptnn0fz |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) |
97 |
96
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ) |
98 |
97
|
fveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) ) |
99 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝑅 ∈ Ring ) |
100 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → 𝐿 ∈ ℕ0 ) |
101 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝑘 ∈ ℕ0 ) |
102 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝜑 ) |
103 |
12
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐾 ) |
104 |
102 76 103
|
3jca |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ) |
105 |
101 104
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝐾 ) ) |
106 |
105 45
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
107 |
106
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
108 |
107
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 ) |
109 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 0 ... 𝑠 ) ∈ Fin ) |
110 |
1 2 99 100 108 109
|
coe1fzgsumd |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) ) |
111 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) |
112 |
|
nfcv |
⊢ Ⅎ 𝑘 ℕ0 |
113 |
112 54
|
nfralw |
⊢ Ⅎ 𝑘 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) |
114 |
111 113
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) |
115 |
5
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑅 ∈ Ring ) |
116 |
12
|
expcom |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → 𝐴 ∈ 𝐾 ) ) |
117 |
116 101
|
syl11 |
⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) ) |
118 |
117
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → 𝐴 ∈ 𝐾 ) ) |
119 |
118
|
imp |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ 𝐾 ) |
120 |
101
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝑘 ∈ ℕ0 ) |
121 |
8 6 1 3 7 43 4
|
coe1tm |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) ) |
122 |
115 119 120 121
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑘 , 𝐴 , 0 ) ) ) |
123 |
|
eqeq1 |
⊢ ( 𝑛 = 𝐿 → ( 𝑛 = 𝑘 ↔ 𝐿 = 𝑘 ) ) |
124 |
123
|
ifbid |
⊢ ( 𝑛 = 𝐿 → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) |
125 |
124
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) ∧ 𝑛 = 𝐿 ) → if ( 𝑛 = 𝑘 , 𝐴 , 0 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) |
126 |
11
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐿 ∈ ℕ0 ) |
127 |
6 8
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 ) |
128 |
5 127
|
syl |
⊢ ( 𝜑 → 0 ∈ 𝐾 ) |
129 |
128
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 0 ∈ 𝐾 ) |
130 |
119 129
|
ifcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ∈ 𝐾 ) |
131 |
122 125 126 130
|
fvmptd |
⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) = if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) |
132 |
114 131
|
mpteq2da |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) |
133 |
132
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) ) |
134 |
|
breq2 |
⊢ ( 𝑥 = 𝐿 → ( 𝑠 < 𝑥 ↔ 𝑠 < 𝐿 ) ) |
135 |
|
csbeq1 |
⊢ ( 𝑥 = 𝐿 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
136 |
135
|
eqeq1d |
⊢ ( 𝑥 = 𝐿 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ↔ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ) |
137 |
134 136
|
imbi12d |
⊢ ( 𝑥 = 𝐿 → ( ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ↔ ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ) ) |
138 |
137
|
rspcva |
⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ) |
139 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) |
140 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴 |
141 |
140
|
nfeq1 |
⊢ Ⅎ 𝑘 ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 |
142 |
139 141
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) |
143 |
|
elfz2nn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) ) |
144 |
|
nn0re |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ ) |
145 |
144
|
ad2antrr |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑘 ∈ ℝ ) |
146 |
|
nn0re |
⊢ ( 𝑠 ∈ ℕ0 → 𝑠 ∈ ℝ ) |
147 |
146
|
adantl |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑠 ∈ ℝ ) |
148 |
147
|
adantr |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑠 ∈ ℝ ) |
149 |
|
nn0re |
⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ ) |
150 |
149
|
adantl |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℝ ) |
151 |
|
lelttr |
⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) ) |
152 |
145 148 150 151
|
syl3anc |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → 𝑘 < 𝐿 ) ) |
153 |
|
animorr |
⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) |
154 |
|
df-ne |
⊢ ( 𝐿 ≠ 𝑘 ↔ ¬ 𝐿 = 𝑘 ) |
155 |
144
|
adantr |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → 𝑘 ∈ ℝ ) |
156 |
|
lttri2 |
⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) ) |
157 |
149 155 156
|
syl2anr |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) ) |
158 |
157
|
adantr |
⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( 𝐿 ≠ 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) ) |
159 |
154 158
|
bitr3id |
⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ( ¬ 𝐿 = 𝑘 ↔ ( 𝐿 < 𝑘 ∨ 𝑘 < 𝐿 ) ) ) |
160 |
153 159
|
mpbird |
⊢ ( ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 < 𝐿 ) → ¬ 𝐿 = 𝑘 ) |
161 |
160
|
ex |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) |
162 |
152 161
|
syld |
⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑘 ≤ 𝑠 ∧ 𝑠 < 𝐿 ) → ¬ 𝐿 = 𝑘 ) ) |
163 |
162
|
exp4b |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
164 |
163
|
expimpd |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑘 ≤ 𝑠 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
165 |
164
|
com23 |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 ≤ 𝑠 → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
166 |
165
|
imp |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) |
167 |
166
|
3adant2 |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑘 ≤ 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) |
168 |
143 167
|
sylbi |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( ( 𝑠 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) |
169 |
168
|
expd |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
170 |
11 169
|
syl7 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
171 |
170
|
com12 |
⊢ ( 𝑠 ∈ ℕ0 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ( 𝜑 → ( 𝑠 < 𝐿 → ¬ 𝐿 = 𝑘 ) ) ) ) |
172 |
171
|
com24 |
⊢ ( 𝑠 ∈ ℕ0 → ( 𝑠 < 𝐿 → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) ) ) |
173 |
172
|
imp |
⊢ ( ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) → ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) ) |
174 |
173
|
impcom |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) |
175 |
174
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) → ¬ 𝐿 = 𝑘 ) ) |
176 |
175
|
imp |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → ¬ 𝐿 = 𝑘 ) |
177 |
176
|
iffalsed |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = 0 ) |
178 |
142 177
|
mpteq2da |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) |
179 |
178
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) ) |
180 |
|
ringmnd |
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd ) |
181 |
5 180
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Mnd ) |
182 |
181
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → 𝑅 ∈ Mnd ) |
183 |
|
ovex |
⊢ ( 0 ... 𝑠 ) ∈ V |
184 |
8
|
gsumz |
⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑠 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 ) |
185 |
182 183 184
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 ) |
186 |
185
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ 0 ) ) = 0 ) |
187 |
|
id |
⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) |
188 |
187
|
eqcomd |
⊢ ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
189 |
188
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → 0 = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
190 |
179 186 189
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) ∧ ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
191 |
190
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ0 ∧ 𝑠 < 𝐿 ) ) → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
192 |
191
|
expr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑠 < 𝐿 → ( ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) |
193 |
192
|
a2d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) |
194 |
193
|
ex |
⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) |
195 |
194
|
com13 |
⊢ ( ( 𝑠 < 𝐿 → ⦋ 𝐿 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) |
196 |
138 195
|
syl |
⊢ ( ( 𝐿 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) |
197 |
196
|
ex |
⊢ ( 𝐿 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 ∈ ℕ0 → ( 𝜑 → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) ) |
198 |
197
|
com24 |
⊢ ( 𝐿 ∈ ℕ0 → ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) ) |
199 |
11 198
|
mpcom |
⊢ ( 𝜑 → ( 𝑠 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) ) ) |
200 |
199
|
imp31 |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑠 < 𝐿 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
201 |
200
|
com12 |
⊢ ( 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
202 |
|
pm3.2 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) ) |
203 |
202
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ¬ 𝑠 < 𝐿 → ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) ) ) |
204 |
181
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝑅 ∈ Mnd ) |
205 |
183
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 0 ... 𝑠 ) ∈ V ) |
206 |
11
|
nn0red |
⊢ ( 𝜑 → 𝐿 ∈ ℝ ) |
207 |
|
lenlt |
⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) ) |
208 |
206 146 207
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 ↔ ¬ 𝑠 < 𝐿 ) ) |
209 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ℕ0 ) |
210 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝑠 ∈ ℕ0 ) |
211 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ≤ 𝑠 ) |
212 |
|
elfz2nn0 |
⊢ ( 𝐿 ∈ ( 0 ... 𝑠 ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝐿 ≤ 𝑠 ) ) |
213 |
209 210 211 212
|
syl3anbrc |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝐿 ≤ 𝑠 ) → 𝐿 ∈ ( 0 ... 𝑠 ) ) |
214 |
213
|
ex |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑠 → 𝐿 ∈ ( 0 ... 𝑠 ) ) ) |
215 |
208 214
|
sylbird |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ¬ 𝑠 < 𝐿 → 𝐿 ∈ ( 0 ... 𝑠 ) ) ) |
216 |
215
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → 𝐿 ∈ ( 0 ... 𝑠 ) ) |
217 |
|
eqcom |
⊢ ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 ) |
218 |
|
ifbi |
⊢ ( ( 𝐿 = 𝑘 ↔ 𝑘 = 𝐿 ) → if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 ) ) |
219 |
217 218
|
ax-mp |
⊢ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) = if ( 𝑘 = 𝐿 , 𝐴 , 0 ) |
220 |
219
|
mpteq2i |
⊢ ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) = ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝑘 = 𝐿 , 𝐴 , 0 ) ) |
221 |
12 6
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
222 |
221
|
ex |
⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) ) |
223 |
222
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 → 𝐴 ∈ ( Base ‘ 𝑅 ) ) ) |
224 |
223 101
|
impel |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑠 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
225 |
224
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
226 |
225
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ∀ 𝑘 ∈ ( 0 ... 𝑠 ) 𝐴 ∈ ( Base ‘ 𝑅 ) ) |
227 |
8 204 205 216 220 226
|
gsummpt1n0 |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ¬ 𝑠 < 𝐿 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
228 |
203 227
|
syl6com |
⊢ ( ¬ 𝑠 < 𝐿 → ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
229 |
201 228
|
pm2.61i |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ if ( 𝐿 = 𝑘 , 𝐴 , 0 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
230 |
133 229
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( coe1 ‘ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ‘ 𝐿 ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
231 |
98 110 230
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |
232 |
231
|
ex |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐴 = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
233 |
34 232
|
syld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
234 |
233
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) ‘ 𝑥 ) = 0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) ) |
235 |
23 234
|
mpd |
⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ 𝐴 ) |