| Step | Hyp | Ref
| Expression |
| 1 | | fconst6g 6797 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (1o × {𝑘}):1o⟶ℕ0) |
| 2 | | nn0ex 12532 |
. . . . . 6
⊢
ℕ0 ∈ V |
| 3 | | 1on 8518 |
. . . . . . 7
⊢
1o ∈ On |
| 4 | 3 | elexi 3503 |
. . . . . 6
⊢
1o ∈ V |
| 5 | 2, 4 | elmap 8911 |
. . . . 5
⊢
((1o × {𝑘}) ∈ (ℕ0
↑m 1o) ↔ (1o × {𝑘}):1o⟶ℕ0) |
| 6 | 1, 5 | sylibr 234 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (1o × {𝑘}) ∈ (ℕ0
↑m 1o)) |
| 7 | 6 | adantl 481 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(1o × {𝑘})
∈ (ℕ0 ↑m 1o)) |
| 8 | | eqidd 2738 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦
(1o × {𝑘})) = (𝑘 ∈ ℕ0 ↦
(1o × {𝑘}))) |
| 9 | | eqid 2737 |
. . . 4
⊢
(1o mPwSer 𝑅) = (1o mPwSer 𝑅) |
| 10 | | coe1mul2.s |
. . . . 5
⊢ 𝑆 =
(PwSer1‘𝑅) |
| 11 | | coe1mul2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑆) |
| 12 | 10, 11, 9 | psr1bas2 22191 |
. . . 4
⊢ 𝐵 = (Base‘(1o
mPwSer 𝑅)) |
| 13 | | coe1mul2.u |
. . . 4
⊢ · =
(.r‘𝑅) |
| 14 | | coe1mul2.t |
. . . . 5
⊢ ∙ =
(.r‘𝑆) |
| 15 | 10, 9, 14 | psr1mulr 22224 |
. . . 4
⊢ ∙ =
(.r‘(1o mPwSer 𝑅)) |
| 16 | | psr1baslem 22186 |
. . . 4
⊢
(ℕ0 ↑m 1o) = {𝑎 ∈ (ℕ0
↑m 1o) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
| 17 | | simp2 1138 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
| 18 | | simp3 1139 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
| 19 | 9, 12, 13, 15, 16, 17, 18 | psrmulfval 21963 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) = (𝑏 ∈ (ℕ0
↑m 1o) ↦ (𝑅 Σg (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐) · (𝐺‘(𝑏 ∘f − 𝑐))))))) |
| 20 | | breq2 5147 |
. . . . . 6
⊢ (𝑏 = (1o × {𝑘}) → (𝑑 ∘r ≤ 𝑏 ↔ 𝑑 ∘r ≤ (1o
× {𝑘}))) |
| 21 | 20 | rabbidv 3444 |
. . . . 5
⊢ (𝑏 = (1o × {𝑘}) → {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ 𝑏} = {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) |
| 22 | | fvoveq1 7454 |
. . . . . 6
⊢ (𝑏 = (1o × {𝑘}) → (𝐺‘(𝑏 ∘f − 𝑐)) = (𝐺‘((1o × {𝑘}) ∘f −
𝑐))) |
| 23 | 22 | oveq2d 7447 |
. . . . 5
⊢ (𝑏 = (1o × {𝑘}) → ((𝐹‘𝑐) · (𝐺‘(𝑏 ∘f − 𝑐))) = ((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐)))) |
| 24 | 21, 23 | mpteq12dv 5233 |
. . . 4
⊢ (𝑏 = (1o × {𝑘}) → (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐) · (𝐺‘(𝑏 ∘f − 𝑐)))) = (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐))))) |
| 25 | 24 | oveq2d 7447 |
. . 3
⊢ (𝑏 = (1o × {𝑘}) → (𝑅 Σg (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ 𝑏} ↦ ((𝐹‘𝑐) · (𝐺‘(𝑏 ∘f − 𝑐))))) = (𝑅 Σg (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐)))))) |
| 26 | 7, 8, 19, 25 | fmptco 7149 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐹 ∙ 𝐺) ∘ (𝑘 ∈ ℕ0 ↦
(1o × {𝑘}))) = (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐))))))) |
| 27 | 10 | psr1ring 22248 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑆 ∈ Ring) |
| 28 | 11, 14 | ringcl 20247 |
. . . 4
⊢ ((𝑆 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) ∈ 𝐵) |
| 29 | 27, 28 | syl3an1 1164 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 ∙ 𝐺) ∈ 𝐵) |
| 30 | | eqid 2737 |
. . . 4
⊢
(coe1‘(𝐹 ∙ 𝐺)) = (coe1‘(𝐹 ∙ 𝐺)) |
| 31 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈ ℕ0
↦ (1o × {𝑘})) = (𝑘 ∈ ℕ0 ↦
(1o × {𝑘})) |
| 32 | 30, 11, 10, 31 | coe1fval3 22210 |
. . 3
⊢ ((𝐹 ∙ 𝐺) ∈ 𝐵 → (coe1‘(𝐹 ∙ 𝐺)) = ((𝐹 ∙ 𝐺) ∘ (𝑘 ∈ ℕ0 ↦
(1o × {𝑘})))) |
| 33 | 29, 32 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 ∙ 𝐺)) = ((𝐹 ∙ 𝐺) ∘ (𝑘 ∈ ℕ0 ↦
(1o × {𝑘})))) |
| 34 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 35 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 36 | | simpl1 1192 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 37 | | ringcmn 20279 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 38 | 36, 37 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ CMnd) |
| 39 | | fzfi 14013 |
. . . . . 6
⊢
(0...𝑘) ∈
Fin |
| 40 | 39 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
| 41 | | simpll1 1213 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → 𝑅 ∈ Ring) |
| 42 | | simpll2 1214 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → 𝐹 ∈ 𝐵) |
| 43 | | eqid 2737 |
. . . . . . . . . 10
⊢
(coe1‘𝐹) = (coe1‘𝐹) |
| 44 | 43, 11, 10, 34 | coe1f2 22211 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐵 → (coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
| 45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → (coe1‘𝐹):ℕ0⟶(Base‘𝑅)) |
| 46 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℕ0) |
| 47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → 𝑥 ∈ ℕ0) |
| 48 | 45, 47 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → ((coe1‘𝐹)‘𝑥) ∈ (Base‘𝑅)) |
| 49 | | simpll3 1215 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → 𝐺 ∈ 𝐵) |
| 50 | | eqid 2737 |
. . . . . . . . . 10
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
| 51 | 50, 11, 10, 34 | coe1f2 22211 |
. . . . . . . . 9
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶(Base‘𝑅)) |
| 52 | 49, 51 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → (coe1‘𝐺):ℕ0⟶(Base‘𝑅)) |
| 53 | | fznn0sub 13596 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑘) → (𝑘 − 𝑥) ∈
ℕ0) |
| 54 | 53 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → (𝑘 − 𝑥) ∈
ℕ0) |
| 55 | 52, 54 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → ((coe1‘𝐺)‘(𝑘 − 𝑥)) ∈ (Base‘𝑅)) |
| 56 | 34, 13 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐹)‘𝑥) ∈ (Base‘𝑅) ∧ ((coe1‘𝐺)‘(𝑘 − 𝑥)) ∈ (Base‘𝑅)) → (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))) ∈ (Base‘𝑅)) |
| 57 | 41, 48, 55, 56 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ (0...𝑘)) → (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))) ∈ (Base‘𝑅)) |
| 58 | 57 | fmpttd 7135 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))):(0...𝑘)⟶(Base‘𝑅)) |
| 59 | 39 | elexi 3503 |
. . . . . . . . 9
⊢
(0...𝑘) ∈
V |
| 60 | 59 | mptex 7243 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∈ V |
| 61 | | funmpt 6604 |
. . . . . . . 8
⊢ Fun
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) |
| 62 | | fvex 6919 |
. . . . . . . 8
⊢
(0g‘𝑅) ∈ V |
| 63 | 60, 61, 62 | 3pm3.2i 1340 |
. . . . . . 7
⊢ ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∧ (0g‘𝑅) ∈ V) |
| 64 | | suppssdm 8202 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) supp (0g‘𝑅)) ⊆ dom (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) |
| 65 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) = (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) |
| 66 | 65 | dmmptss 6261 |
. . . . . . . . 9
⊢ dom
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ⊆ (0...𝑘) |
| 67 | 64, 66 | sstri 3993 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) supp (0g‘𝑅)) ⊆ (0...𝑘) |
| 68 | 39, 67 | pm3.2i 470 |
. . . . . . 7
⊢
((0...𝑘) ∈ Fin
∧ ((𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) supp (0g‘𝑅)) ⊆ (0...𝑘)) |
| 69 | | suppssfifsupp 9420 |
. . . . . . 7
⊢ ((((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∈ V ∧ Fun (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∧ (0g‘𝑅) ∈ V) ∧ ((0...𝑘) ∈ Fin ∧ ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) supp (0g‘𝑅)) ⊆ (0...𝑘))) → (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) finSupp (0g‘𝑅)) |
| 70 | 63, 68, 69 | mp2an 692 |
. . . . . 6
⊢ (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) finSupp (0g‘𝑅) |
| 71 | 70 | a1i 11 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) finSupp (0g‘𝑅)) |
| 72 | | eqid 2737 |
. . . . . . 7
⊢ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} = {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} |
| 73 | 72 | coe1mul2lem2 22271 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅)):{𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}–1-1-onto→(0...𝑘)) |
| 74 | 73 | adantl 481 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅)):{𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}–1-1-onto→(0...𝑘)) |
| 75 | 34, 35, 38, 40, 58, 71, 74 | gsumf1o 19934 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))))) = (𝑅 Σg ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∘ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅))))) |
| 76 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑐 → (𝑑 ∘r ≤ (1o
× {𝑘}) ↔ 𝑐 ∘r ≤
(1o × {𝑘}))) |
| 77 | 76 | elrab 3692 |
. . . . . . . . . 10
⊢ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↔ (𝑐 ∈ (ℕ0
↑m 1o) ∧ 𝑐 ∘r ≤ (1o
× {𝑘}))) |
| 78 | 77 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} → 𝑐 ∘r ≤
(1o × {𝑘})) |
| 79 | 78 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝑐 ∘r ≤
(1o × {𝑘})) |
| 80 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝑘 ∈
ℕ0) |
| 81 | | elrabi 3687 |
. . . . . . . . . 10
⊢ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} → 𝑐 ∈ (ℕ0
↑m 1o)) |
| 82 | 81 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝑐 ∈ (ℕ0
↑m 1o)) |
| 83 | | coe1mul2lem1 22270 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑐 ∈
(ℕ0 ↑m 1o)) → (𝑐 ∘r ≤
(1o × {𝑘})
↔ (𝑐‘∅)
∈ (0...𝑘))) |
| 84 | 80, 82, 83 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝑐 ∘r ≤
(1o × {𝑘})
↔ (𝑐‘∅)
∈ (0...𝑘))) |
| 85 | 79, 84 | mpbid 232 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝑐‘∅) ∈
(0...𝑘)) |
| 86 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅)) = (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅))) |
| 87 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) = (𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))))) |
| 88 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝑐‘∅) →
((coe1‘𝐹)‘𝑥) = ((coe1‘𝐹)‘(𝑐‘∅))) |
| 89 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = (𝑐‘∅) → (𝑘 − 𝑥) = (𝑘 − (𝑐‘∅))) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑥 = (𝑐‘∅) →
((coe1‘𝐺)‘(𝑘 − 𝑥)) = ((coe1‘𝐺)‘(𝑘 − (𝑐‘∅)))) |
| 91 | 88, 90 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑥 = (𝑐‘∅) →
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))) = (((coe1‘𝐹)‘(𝑐‘∅)) ·
((coe1‘𝐺)‘(𝑘 − (𝑐‘∅))))) |
| 92 | 85, 86, 87, 91 | fmptco 7149 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∘ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅))) =
(𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(((coe1‘𝐹)‘(𝑐‘∅)) ·
((coe1‘𝐺)‘(𝑘 − (𝑐‘∅)))))) |
| 93 | | simpll2 1214 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝐹 ∈ 𝐵) |
| 94 | 43 | fvcoe1 22209 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐵 ∧ 𝑐 ∈ (ℕ0
↑m 1o)) → (𝐹‘𝑐) = ((coe1‘𝐹)‘(𝑐‘∅))) |
| 95 | 93, 82, 94 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝐹‘𝑐) = ((coe1‘𝐹)‘(𝑐‘∅))) |
| 96 | | df1o2 8513 |
. . . . . . . . . . . . . 14
⊢
1o = {∅} |
| 97 | | 0ex 5307 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
| 98 | 96, 2, 97 | mapsnconst 8932 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (ℕ0
↑m 1o) → 𝑐 = (1o × {(𝑐‘∅)})) |
| 99 | 82, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝑐 = (1o ×
{(𝑐‘∅)})) |
| 100 | 99 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
((1o × {𝑘}) ∘f − 𝑐) = ((1o ×
{𝑘}) ∘f
− (1o × {(𝑐‘∅)}))) |
| 101 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
1o ∈ On) |
| 102 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑘 ∈ V |
| 103 | 102 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝑘 ∈ V) |
| 104 | | fvexd 6921 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝑐‘∅) ∈
V) |
| 105 | 101, 103,
104 | ofc12 7727 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
((1o × {𝑘}) ∘f − (1o
× {(𝑐‘∅)})) = (1o ×
{(𝑘 − (𝑐‘∅))})) |
| 106 | 100, 105 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
((1o × {𝑘}) ∘f − 𝑐) = (1o ×
{(𝑘 − (𝑐‘∅))})) |
| 107 | 106 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝐺‘((1o
× {𝑘})
∘f − 𝑐)) = (𝐺‘(1o × {(𝑘 − (𝑐‘∅))}))) |
| 108 | | simpll3 1215 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) → 𝐺 ∈ 𝐵) |
| 109 | | fznn0sub 13596 |
. . . . . . . . . . 11
⊢ ((𝑐‘∅) ∈
(0...𝑘) → (𝑘 − (𝑐‘∅)) ∈
ℕ0) |
| 110 | 85, 109 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝑘 − (𝑐‘∅)) ∈
ℕ0) |
| 111 | 50 | coe1fv 22208 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐵 ∧ (𝑘 − (𝑐‘∅)) ∈ ℕ0)
→ ((coe1‘𝐺)‘(𝑘 − (𝑐‘∅))) = (𝐺‘(1o × {(𝑘 − (𝑐‘∅))}))) |
| 112 | 108, 110,
111 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
((coe1‘𝐺)‘(𝑘 − (𝑐‘∅))) = (𝐺‘(1o × {(𝑘 − (𝑐‘∅))}))) |
| 113 | 107, 112 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
(𝐺‘((1o
× {𝑘})
∘f − 𝑐)) = ((coe1‘𝐺)‘(𝑘 − (𝑐‘∅)))) |
| 114 | 95, 113 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) ∧ 𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})}) →
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐))) =
(((coe1‘𝐹)‘(𝑐‘∅)) ·
((coe1‘𝐺)‘(𝑘 − (𝑐‘∅))))) |
| 115 | 114 | mpteq2dva 5242 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐)))) = (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(((coe1‘𝐹)‘(𝑐‘∅)) ·
((coe1‘𝐺)‘(𝑘 − (𝑐‘∅)))))) |
| 116 | 92, 115 | eqtr4d 2780 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑥 ∈ (0...𝑘) ↦ (((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∘ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅))) =
(𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐))))) |
| 117 | 116 | oveq2d 7447 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
((𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))) ∘ (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
(𝑐‘∅)))) =
(𝑅
Σg (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐)))))) |
| 118 | 75, 117 | eqtrd 2777 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (𝑅 Σg
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))))) = (𝑅 Σg (𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐)))))) |
| 119 | 118 | mpteq2dva 5242 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥)))))) = (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑐 ∈ {𝑑 ∈ (ℕ0
↑m 1o) ∣ 𝑑 ∘r ≤ (1o
× {𝑘})} ↦
((𝐹‘𝑐) · (𝐺‘((1o × {𝑘}) ∘f −
𝑐))))))) |
| 120 | 26, 33, 119 | 3eqtr4d 2787 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 ∙ 𝐺)) = (𝑘 ∈ ℕ0 ↦ (𝑅 Σg
(𝑥 ∈ (0...𝑘) ↦
(((coe1‘𝐹)‘𝑥) ·
((coe1‘𝐺)‘(𝑘 − 𝑥))))))) |