| Step | Hyp | Ref
| Expression |
| 1 | | cply1mul.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
| 2 | | cply1mul.m |
. . . . . . . . . 10
⊢ × =
(.r‘𝑃) |
| 3 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 4 | | cply1mul.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑃) |
| 5 | 1, 2, 3, 4 | coe1mul 22273 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (coe1‘(𝐹 × 𝐺)) = (𝑠 ∈ ℕ0 ↦ (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))))) |
| 6 | 5 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (coe1‘(𝐹 × 𝐺)) = (𝑠 ∈ ℕ0 ↦ (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))))) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) →
(coe1‘(𝐹
×
𝐺)) = (𝑠 ∈ ℕ0 ↦ (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))))) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) →
(coe1‘(𝐹
×
𝐺)) = (𝑠 ∈ ℕ0 ↦ (𝑅 Σg
(𝑘 ∈ (0...𝑠) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))))) |
| 9 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑠 = 𝑛 → (0...𝑠) = (0...𝑛)) |
| 10 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑛 → ((coe1‘𝐺)‘(𝑠 − 𝑘)) = ((coe1‘𝐺)‘(𝑛 − 𝑘))) |
| 11 | 10 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑠 = 𝑛 → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))) = (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))) |
| 12 | 9, 11 | mpteq12dv 5233 |
. . . . . . . 8
⊢ (𝑠 = 𝑛 → (𝑘 ∈ (0...𝑠) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))))) |
| 13 | 12 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑠 = 𝑛 → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))))) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢
(((((𝑅 ∈ Ring
∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) ∧ 𝑠 = 𝑛) → (𝑅 Σg (𝑘 ∈ (0...𝑠) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑠 − 𝑘))))) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))))) |
| 15 | | nnnn0 12533 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 16 | 15 | adantl 481 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ0) |
| 17 | | ovexd 7466 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))))) ∈ V) |
| 18 | 8, 14, 16, 17 | fvmptd 7023 |
. . . . 5
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) →
((coe1‘(𝐹
×
𝐺))‘𝑛) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))))) |
| 19 | | r19.26 3111 |
. . . . . . . . . 10
⊢
(∀𝑐 ∈
ℕ (((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 ) ↔ (∀𝑐 ∈ ℕ
((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 )) |
| 20 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (𝑛 − 𝑘) = (𝑛 − 0)) |
| 21 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
| 22 | 21 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → (𝑛 − 0) = 𝑛) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (𝑛 − 0) = 𝑛) |
| 24 | 20, 23 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → (𝑛 − 𝑘) = 𝑛) |
| 25 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → 𝑛 ∈ ℕ) |
| 26 | 24, 25 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → (𝑛 − 𝑘) ∈ ℕ) |
| 27 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑛 − 𝑘) → (((coe1‘𝐺)‘𝑐) = 0 ↔
((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 )) |
| 28 | 27 | rspcv 3618 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 𝑘) ∈ ℕ → (∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 →
((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 )) |
| 29 | 26, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → (∀𝑐 ∈ ℕ ((coe1‘𝐺)‘𝑐) = 0 →
((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 )) |
| 30 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = (((coe1‘𝐹)‘𝑘)(.r‘𝑅) 0 )) |
| 31 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0)) → 𝑅 ∈ Ring) |
| 32 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐹 ∈ 𝐵) |
| 33 | | elfznn0 13660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
| 34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → 𝑘 ∈ ℕ0) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(coe1‘𝐹) = (coe1‘𝐹) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 38 | 36, 4, 1, 37 | coe1fvalcl 22214 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝐹)‘𝑘) ∈ (Base‘𝑅)) |
| 39 | 32, 35, 38 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0)) → ((coe1‘𝐹)‘𝑘) ∈ (Base‘𝑅)) |
| 40 | | cply1mul.0 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 =
(0g‘𝑅) |
| 41 | 37, 3, 40 | ringrz 20291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐹)‘𝑘) ∈ (Base‘𝑅)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅) 0 ) = 0 ) |
| 42 | 31, 39, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅) 0 ) = 0 ) |
| 43 | 30, 42 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0)) ∧ ((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 ) →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ) |
| 44 | 43 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0)) → (((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )) |
| 45 | 44 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 46 | 45 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → (((coe1‘𝐺)‘(𝑛 − 𝑘)) = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 47 | 29, 46 | syldc 48 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑐 ∈
ℕ ((coe1‘𝐺)‘𝑐) = 0 → (((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) ∧ 𝑘 = 0) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 48 | 47 | expd 415 |
. . . . . . . . . . . . . 14
⊢
(∀𝑐 ∈
ℕ ((coe1‘𝐺)‘𝑐) = 0 → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (𝑘 = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 49 | 48 | com24 95 |
. . . . . . . . . . . . 13
⊢
(∀𝑐 ∈
ℕ ((coe1‘𝐺)‘𝑐) = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑘 = 0 → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . 12
⊢
((∀𝑐 ∈
ℕ ((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑘 = 0 → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 51 | 50 | com13 88 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 52 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑘 = 0 → 𝑘 ≠ 0) |
| 53 | 52, 33 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → (𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0)) |
| 54 | | elnnne0 12540 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0
∧ 𝑘 ≠
0)) |
| 55 | 53, 54 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ) |
| 56 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 𝑘 → (((coe1‘𝐹)‘𝑐) = 0 ↔
((coe1‘𝐹)‘𝑘) = 0 )) |
| 57 | 56 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ →
(∀𝑐 ∈ ℕ
((coe1‘𝐹)‘𝑐) = 0 →
((coe1‘𝐹)‘𝑘) = 0 )) |
| 58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → (∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 →
((coe1‘𝐹)‘𝑘) = 0 )) |
| 59 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((coe1‘𝐹)‘𝑘) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = ( 0 (.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))) |
| 60 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑘 ∈ (0...𝑛)) → 𝑅 ∈ Ring) |
| 61 | 4 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐺 ∈ 𝐵 ↔ 𝐺 ∈ (Base‘𝑃)) |
| 62 | 61 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐺 ∈ 𝐵 → 𝐺 ∈ (Base‘𝑃)) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (Base‘𝑃)) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → 𝐺 ∈ (Base‘𝑃)) |
| 65 | | fznn0sub 13596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ (0...𝑛) → (𝑛 − 𝑘) ∈
ℕ0) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
| 67 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 68 | 66, 67, 1, 37 | coe1fvalcl 22214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ∈ (Base‘𝑃) ∧ (𝑛 − 𝑘) ∈ ℕ0) →
((coe1‘𝐺)‘(𝑛 − 𝑘)) ∈ (Base‘𝑅)) |
| 69 | 64, 65, 68 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑘 ∈ (0...𝑛)) → ((coe1‘𝐺)‘(𝑛 − 𝑘)) ∈ (Base‘𝑅)) |
| 70 | 37, 3, 40 | ringlz 20290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝐺)‘(𝑛 − 𝑘)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ) |
| 71 | 60, 69, 70 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑘 ∈ (0...𝑛)) → ( 0 (.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ) |
| 72 | 59, 71 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑘 ∈ (0...𝑛)) ∧ ((coe1‘𝐹)‘𝑘) = 0 ) →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ) |
| 73 | 72 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )) |
| 74 | 73 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑘 ∈ (0...𝑛) → (((coe1‘𝐹)‘𝑘) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 75 | 74 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘) = 0 → (𝑘 ∈ (0...𝑛) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 76 | 75 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘) = 0 → (𝑛 ∈ ℕ → (𝑘 ∈ (0...𝑛) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 77 | 76 | com14 96 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (0...𝑛) → (((coe1‘𝐹)‘𝑘) = 0 → (𝑛 ∈ ℕ → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘) = 0 → (𝑛 ∈ ℕ → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 79 | 58, 78 | syld 47 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → (∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 → (𝑛 ∈ ℕ → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 80 | 79 | com24 95 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑘 = 0 ∧ 𝑘 ∈ (0...𝑛)) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑛 ∈ ℕ → (∀𝑐 ∈ ℕ
((coe1‘𝐹)‘𝑐) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 81 | 80 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑘 = 0 → (𝑘 ∈ (0...𝑛) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑛 ∈ ℕ → (∀𝑐 ∈ ℕ
((coe1‘𝐹)‘𝑐) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))))) |
| 82 | 81 | com14 96 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑘 ∈ (0...𝑛) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (¬ 𝑘 = 0 → (∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))))) |
| 83 | 82 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (¬ 𝑘 = 0 → (∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 →
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 84 | 83 | com14 96 |
. . . . . . . . . . . . 13
⊢
(∀𝑐 ∈
ℕ ((coe1‘𝐹)‘𝑐) = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (¬ 𝑘 = 0 → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 85 | 84 | adantr 480 |
. . . . . . . . . . . 12
⊢
((∀𝑐 ∈
ℕ ((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (¬ 𝑘 = 0 → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 86 | 85 | com13 88 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = 0 → ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )))) |
| 87 | 51, 86 | pm2.61i 182 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → ((∀𝑐 ∈ ℕ ((coe1‘𝐹)‘𝑐) = 0 ∧ ∀𝑐 ∈ ℕ
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 88 | 19, 87 | biimtrid 242 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 ) → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ))) |
| 89 | 88 | imp 406 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) → ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 )) |
| 90 | 89 | impl 455 |
. . . . . . 7
⊢
(((((𝑅 ∈ Ring
∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑛)) → (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))) = 0 ) |
| 91 | 90 | mpteq2dva 5242 |
. . . . . 6
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (0...𝑛) ↦ (((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘)))) = (𝑘 ∈ (0...𝑛) ↦ 0 )) |
| 92 | 91 | oveq2d 7447 |
. . . . 5
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦
(((coe1‘𝐹)‘𝑘)(.r‘𝑅)((coe1‘𝐺)‘(𝑛 − 𝑘))))) = (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ 0 ))) |
| 93 | | ringmnd 20240 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
| 94 | | ovexd 7466 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (0...𝑛) ∈ V) |
| 95 | 40 | gsumz 18849 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Mnd ∧ (0...𝑛) ∈ V) → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦ 0 )) = 0 ) |
| 96 | 93, 94, 95 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦ 0 )) = 0 ) |
| 97 | 96 | adantr 480 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝑅 Σg (𝑘 ∈ (0...𝑛) ↦ 0 )) = 0 ) |
| 98 | 97 | adantr 480 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦ 0 )) = 0 ) |
| 99 | 98 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) → (𝑅 Σg
(𝑘 ∈ (0...𝑛) ↦ 0 )) = 0 ) |
| 100 | 18, 92, 99 | 3eqtrd 2781 |
. . . 4
⊢ ((((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) ∧ 𝑛 ∈ ℕ) →
((coe1‘(𝐹
×
𝐺))‘𝑛) = 0 ) |
| 101 | 100 | ralrimiva 3146 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) → ∀𝑛 ∈ ℕ
((coe1‘(𝐹
×
𝐺))‘𝑛) = 0 ) |
| 102 | | fveqeq2 6915 |
. . . 4
⊢ (𝑐 = 𝑛 → (((coe1‘(𝐹 × 𝐺))‘𝑐) = 0 ↔
((coe1‘(𝐹
×
𝐺))‘𝑛) = 0 )) |
| 103 | 102 | cbvralvw 3237 |
. . 3
⊢
(∀𝑐 ∈
ℕ ((coe1‘(𝐹 × 𝐺))‘𝑐) = 0 ↔ ∀𝑛 ∈ ℕ
((coe1‘(𝐹
×
𝐺))‘𝑛) = 0 ) |
| 104 | 101, 103 | sylibr 234 |
. 2
⊢ (((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) ∧ ∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 )) → ∀𝑐 ∈ ℕ
((coe1‘(𝐹
×
𝐺))‘𝑐) = 0 ) |
| 105 | 104 | ex 412 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (∀𝑐 ∈ ℕ
(((coe1‘𝐹)‘𝑐) = 0 ∧
((coe1‘𝐺)‘𝑐) = 0 ) → ∀𝑐 ∈ ℕ
((coe1‘(𝐹
×
𝐺))‘𝑐) = 0 )) |