Proof of Theorem chfacfscmulgsum
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝑌) =
(Base‘𝑌) |
2 | | chfacfisf.0 |
. . 3
⊢ 0 =
(0g‘𝑌) |
3 | | chfacfscmulgsum.p |
. . 3
⊢ + =
(+g‘𝑌) |
4 | | crngring 19795 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
5 | 4 | anim2i 617 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
6 | 5 | 3adant3 1131 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
7 | | chfacfisf.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
8 | | chfacfisf.y |
. . . . . . 7
⊢ 𝑌 = (𝑁 Mat 𝑃) |
9 | 7, 8 | pmatring 21841 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
10 | 6, 9 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
11 | | ringcmn 19820 |
. . . . 5
⊢ (𝑌 ∈ Ring → 𝑌 ∈ CMnd) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ CMnd) |
13 | 12 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ CMnd) |
14 | | nn0ex 12239 |
. . . 4
⊢
ℕ0 ∈ V |
15 | 14 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ℕ0 ∈
V) |
16 | | simpll 764 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
17 | | simplr 766 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
18 | | simpr 485 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
19 | 16, 17, 18 | 3jca 1127 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈
ℕ0)) |
20 | | chfacfisf.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
21 | | chfacfisf.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
22 | | chfacfisf.r |
. . . . 5
⊢ × =
(.r‘𝑌) |
23 | | chfacfisf.s |
. . . . 5
⊢ − =
(-g‘𝑌) |
24 | | chfacfisf.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
25 | | chfacfisf.g |
. . . . 5
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
26 | | chfacfscmulcl.x |
. . . . 5
⊢ 𝑋 = (var1‘𝑅) |
27 | | chfacfscmulcl.m |
. . . . 5
⊢ · = (
·𝑠 ‘𝑌) |
28 | | chfacfscmulcl.e |
. . . . 5
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
29 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28 | chfacfscmulcl 22006 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
30 | 19, 29 | syl 17 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
31 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28 | chfacfscmulfsupp 22008 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 ) |
32 | | nn0disj 13372 |
. . . 4
⊢
((0...(𝑠 + 1)) ∩
(ℤ≥‘((𝑠 + 1) + 1))) = ∅ |
33 | 32 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0...(𝑠 + 1)) ∩
(ℤ≥‘((𝑠 + 1) + 1))) = ∅) |
34 | | nnnn0 12240 |
. . . . . 6
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
35 | | peano2nn0 12273 |
. . . . . 6
⊢ (𝑠 ∈ ℕ0
→ (𝑠 + 1) ∈
ℕ0) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ0) |
37 | | nn0split 13371 |
. . . . 5
⊢ ((𝑠 + 1) ∈ ℕ0
→ ℕ0 = ((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝑠 ∈ ℕ →
ℕ0 = ((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
39 | 38 | ad2antrl 725 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ℕ0 =
((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
40 | 1, 2, 3, 13, 15, 30, 31, 33, 39 | gsumsplit2 19530 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))) |
41 | | simpll 764 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
42 | | simplr 766 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
43 | | nncn 11981 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
44 | | add1p1 12224 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
46 | 45 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
47 | 46 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) →
(ℤ≥‘((𝑠 + 1) + 1)) =
(ℤ≥‘(𝑠 + 2))) |
48 | 47 | eleq2d 2824 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↔ 𝑖 ∈
(ℤ≥‘(𝑠 + 2)))) |
49 | 48 | biimpa 477 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → 𝑖 ∈
(ℤ≥‘(𝑠 + 2))) |
50 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28 | chfacfscmul0 22007 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ) |
51 | 41, 42, 49, 50 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ) |
52 | 51 | mpteq2dva 5174 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) = (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↦ 0
)) |
53 | 52 | oveq2d 7291 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 ))) |
54 | 4, 9 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring) |
55 | | ringmnd 19793 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Mnd) |
57 | 56 | 3adant3 1131 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Mnd) |
58 | | fvex 6787 |
. . . . . . . 8
⊢
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V |
59 | 57, 58 | jctir 521 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V)) |
60 | 59 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V)) |
61 | 2 | gsumz 18474 |
. . . . . 6
⊢ ((𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V) → (𝑌 Σg
(𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 ) |
62 | 60, 61 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 ) |
63 | 53, 62 | eqtrd 2778 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = 0 ) |
64 | 63 | oveq2d 7291 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + 0 )) |
65 | | fzfid 13693 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (0...(𝑠 + 1)) ∈ Fin) |
66 | | elfznn0 13349 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...(𝑠 + 1)) → 𝑖 ∈ ℕ0) |
67 | 66, 19 | sylan2 593 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈
ℕ0)) |
68 | 67, 29 | syl 17 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
69 | 68 | ralrimiva 3103 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 + 1))((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
70 | 1, 13, 65, 69 | gsummptcl 19568 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) ∈ (Base‘𝑌)) |
71 | 1, 3, 2 | mndrid 18406 |
. . . 4
⊢ ((𝑌 ∈ Mnd ∧ (𝑌 Σg
(𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) ∈ (Base‘𝑌)) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
72 | 57, 70, 71 | syl2an2r 682 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
73 | 64, 72 | eqtrd 2778 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
74 | 34 | ad2antrl 725 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑠 ∈ ℕ0) |
75 | 1, 3, 13, 74, 68 | gsummptfzsplit 19533 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))) |
76 | | elfznn0 13349 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0) |
77 | 76, 30 | sylan2 593 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
78 | 1, 3, 13, 74, 77 | gsummptfzsplitl 19534 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))))) |
79 | 57 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Mnd) |
80 | | 0nn0 12248 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
81 | 80 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈
ℕ0) |
82 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28 | chfacfscmulcl 22006 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 0 ∈ ℕ0)
→ ((0 ↑ 𝑋) · (𝐺‘0)) ∈ (Base‘𝑌)) |
83 | 81, 82 | mpd3an3 1461 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ 𝑋) · (𝐺‘0)) ∈ (Base‘𝑌)) |
84 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 ↑ 𝑋) = (0 ↑ 𝑋)) |
85 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝐺‘𝑖) = (𝐺‘0)) |
86 | 84, 85 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((0 ↑ 𝑋) · (𝐺‘0))) |
87 | 1, 86 | gsumsn 19555 |
. . . . . . 7
⊢ ((𝑌 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ ((0 ↑ 𝑋) · (𝐺‘0)) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((0 ↑ 𝑋) · (𝐺‘0))) |
88 | 79, 81, 83, 87 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((0 ↑ 𝑋) · (𝐺‘0))) |
89 | 88 | oveq2d 7291 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0)))) |
90 | 78, 89 | eqtrd 2778 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0)))) |
91 | | ovexd 7310 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ V) |
92 | | 1nn0 12249 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
93 | 92 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 1 ∈
ℕ0) |
94 | 74, 93 | nn0addcld 12297 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
95 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28 | chfacfscmulcl 22006 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝑠 + 1) ∈ ℕ0) →
(((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) |
96 | 94, 95 | mpd3an3 1461 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) |
97 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑖 = (𝑠 + 1) → (𝑖 ↑ 𝑋) = ((𝑠 + 1) ↑ 𝑋)) |
98 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑖 = (𝑠 + 1) → (𝐺‘𝑖) = (𝐺‘(𝑠 + 1))) |
99 | 97, 98 | oveq12d 7293 |
. . . . . 6
⊢ (𝑖 = (𝑠 + 1) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) |
100 | 1, 99 | gsumsn 19555 |
. . . . 5
⊢ ((𝑌 ∈ Mnd ∧ (𝑠 + 1) ∈ V ∧ (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) |
101 | 79, 91, 96, 100 | syl3anc 1370 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) |
102 | 90, 101 | oveq12d 7293 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0))) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))))) |
103 | | fzfid 13693 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (1...𝑠) ∈ Fin) |
104 | | simpll 764 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
105 | | simplr 766 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
106 | | elfznn 13285 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ) |
107 | 106 | nnnn0d 12293 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0) |
108 | 107 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0) |
109 | 104, 105,
108, 29 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
110 | 109 | ralrimiva 3103 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
111 | 1, 13, 103, 110 | gsummptcl 19568 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) ∈ (Base‘𝑌)) |
112 | 1, 3 | mndass 18394 |
. . . . 5
⊢ ((𝑌 ∈ Mnd ∧ ((𝑌 Σg
(𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) ∈ (Base‘𝑌) ∧ ((0 ↑ 𝑋) · (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0))) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))))) |
113 | 79, 111, 83, 96, 112 | syl13anc 1371 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0))) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))))) |
114 | 106 | nnne0d 12023 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ≠ 0) |
115 | 114 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ 0) |
116 | | neeq1 3006 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0)) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0)) |
118 | 115, 117 | mpbird 256 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ 0) |
119 | | eqneqall 2954 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝑛 ≠ 0 → 0 = (𝑇‘(𝑏‘(𝑖 − 1))))) |
120 | 118, 119 | mpan9 507 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = (𝑇‘(𝑏‘(𝑖 − 1)))) |
121 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 𝑛 = 𝑖) |
122 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . 17
⊢ (0 =
𝑛 → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
123 | 122 | eqcoms 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
124 | 123 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
125 | 121, 124 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = 𝑖) |
126 | 125 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑏‘0) = (𝑏‘𝑖)) |
127 | 126 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑇‘(𝑏‘0)) = (𝑇‘(𝑏‘𝑖))) |
128 | 127 | oveq2d 7291 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) = ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) |
129 | 120, 128 | oveq12d 7293 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
130 | | elfz2 13246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) ↔ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤
𝑖 ∧ 𝑖 ≤ 𝑠))) |
131 | | zleltp1 12371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖 ≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
132 | 131 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
133 | 132 | 3adant1 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
134 | 133 | biimpcd 248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ≤ 𝑠 → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1))) |
135 | 134 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 ≤
𝑖 ∧ 𝑖 ≤ 𝑠) → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1))) |
136 | 135 | impcom 408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → 𝑖 < (𝑠 + 1)) |
137 | 136 | orcd 870 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)) |
138 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ ℤ → 𝑠 ∈
ℝ) |
139 | | 1red 10976 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ ℤ → 1 ∈
ℝ) |
140 | 138, 139 | readdcld 11004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 ∈ ℤ → (𝑠 + 1) ∈
ℝ) |
141 | | zre 12323 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℝ) |
142 | 140, 141 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈
ℝ)) |
143 | 142 | 3adant1 1129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
∈ ℝ ∧ (𝑠 +
1) ∈ ℝ)) |
144 | | lttri2 11057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) →
(𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
146 | 145 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
147 | 137, 146 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → 𝑖 ≠ (𝑠 + 1)) |
148 | 130, 147 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ≠ (𝑠 + 1)) |
149 | 148 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ (𝑠 + 1)) |
150 | | neeq1 3006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1))) |
151 | 150 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1))) |
152 | 149, 151 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ (𝑠 + 1)) |
153 | 152 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → 𝑛 ≠ (𝑠 + 1)) |
154 | 153 | neneqd 2948 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → ¬ 𝑛 = (𝑠 + 1)) |
155 | 154 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → (𝑛 = (𝑠 + 1) → (𝑇‘(𝑏‘𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
156 | 155 | imp 407 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏‘𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
157 | 106 | nnred 11988 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℝ) |
158 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝑛 ∈ ℝ ↔ 𝑖 ∈ ℝ)) |
159 | 157, 158 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) → (𝑛 = 𝑖 → 𝑛 ∈ ℝ)) |
160 | 159 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑛 = 𝑖 → 𝑛 ∈ ℝ)) |
161 | 160 | imp 407 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ∈ ℝ) |
162 | 74 | nn0red 12294 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑠 ∈ ℝ) |
163 | 162 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑠 ∈ ℝ) |
164 | | 1red 10976 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 1 ∈ ℝ) |
165 | 163, 164 | readdcld 11004 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑠 + 1) ∈ ℝ) |
166 | 130, 136 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 < (𝑠 + 1)) |
167 | 166 | ad2antlr 724 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 < (𝑠 + 1)) |
168 | | breq1 5077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1))) |
169 | 168 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1))) |
170 | 167, 169 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 < (𝑠 + 1)) |
171 | 161, 165,
170 | ltnsymd 11124 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ¬ (𝑠 + 1) < 𝑛) |
172 | 171 | pm2.21d 121 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ((𝑠 + 1) < 𝑛 → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
173 | 172 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → ((𝑠 + 1) < 𝑛 → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
174 | 173 | imp 407 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
175 | | simp-4r 781 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 = 𝑖) |
176 | 175 | fvoveq1d 7297 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘(𝑛 − 1)) = (𝑏‘(𝑖 − 1))) |
177 | 176 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘(𝑛 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1)))) |
178 | 175 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘𝑛) = (𝑏‘𝑖)) |
179 | 178 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘𝑛)) = (𝑇‘(𝑏‘𝑖))) |
180 | 179 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) = ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) |
181 | 177, 180 | oveq12d 7293 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
182 | 174, 181 | ifeqda 4495 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
183 | 156, 182 | ifeqda 4495 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
184 | 129, 183 | ifeqda 4495 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
185 | | ovexd 7310 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) ∈ V) |
186 | 25, 184, 108, 185 | fvmptd2 6883 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝐺‘𝑖) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
187 | 186 | oveq2d 7291 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
188 | 187 | mpteq2dva 5174 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) |
189 | 188 | oveq2d 7291 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))))) |
190 | | nn0p1gt0 12262 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ0
→ 0 < (𝑠 +
1)) |
191 | | 0red 10978 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ0
→ 0 ∈ ℝ) |
192 | | ltne 11072 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0) |
193 | 191, 192 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℕ0
∧ 0 < (𝑠 + 1))
→ (𝑠 + 1) ≠
0) |
194 | | neeq1 3006 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑠 + 1) → (𝑛 ≠ 0 ↔ (𝑠 + 1) ≠ 0)) |
195 | 193, 194 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℕ0
∧ 0 < (𝑠 + 1))
→ (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
196 | 34, 190, 195 | syl2anc2 585 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
197 | 196 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
198 | 197 | imp 407 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → 𝑛 ≠ 0) |
199 | | eqneqall 2954 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → (𝑛 ≠ 0 → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏‘𝑠)))) |
200 | 198, 199 | mpan9 507 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏‘𝑠))) |
201 | | iftrue 4465 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑠 + 1) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = (𝑇‘(𝑏‘𝑠))) |
202 | 201 | ad2antlr 724 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = (𝑇‘(𝑏‘𝑠))) |
203 | 200, 202 | ifeqda 4495 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = (𝑇‘(𝑏‘𝑠))) |
204 | 74, 35 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
205 | | fvexd 6789 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘𝑠)) ∈ V) |
206 | 25, 203, 204, 205 | fvmptd2 6883 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘(𝑠 + 1)) = (𝑇‘(𝑏‘𝑠))) |
207 | 206 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) = (((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠)))) |
208 | 4 | 3ad2ant2 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
209 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑃) =
(Base‘𝑃) |
210 | 26, 7, 209 | vr1cl 21388 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
211 | 208, 210 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑋 ∈ (Base‘𝑃)) |
212 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
213 | 212, 209 | mgpbas 19726 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
214 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝑃) = (1r‘𝑃) |
215 | 212, 214 | ringidval 19739 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑃) = (0g‘(mulGrp‘𝑃)) |
216 | 213, 215,
28 | mulg0 18707 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (Base‘𝑃) → (0 ↑ 𝑋) = (1r‘𝑃)) |
217 | 211, 216 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0 ↑ 𝑋) = (1r‘𝑃)) |
218 | 7 | ply1crng 21369 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
219 | 218 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
220 | 219 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑃 ∈ CRing)) |
221 | 8 | matsca2 21569 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ CRing) → 𝑃 = (Scalar‘𝑌)) |
222 | 220, 221 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑃 = (Scalar‘𝑌)) |
223 | 222 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (1r‘𝑃) =
(1r‘(Scalar‘𝑌))) |
224 | 217, 223 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0 ↑ 𝑋) = (1r‘(Scalar‘𝑌))) |
225 | 224 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (0 ↑ 𝑋) = (1r‘(Scalar‘𝑌))) |
226 | 225 | oveq1d 7290 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ 𝑋) · (𝐺‘0)) =
((1r‘(Scalar‘𝑌)) · (𝐺‘0))) |
227 | 7, 8 | pmatlmod 21842 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod) |
228 | 4, 227 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ LMod) |
229 | 228 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ LMod) |
230 | 20, 21, 7, 8, 22, 23, 2, 24, 25 | chfacfisf 22003 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) |
231 | 4, 230 | syl3anl2 1412 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) |
232 | 231, 81 | ffvelrnd 6962 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘0) ∈ (Base‘𝑌)) |
233 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
234 | | eqid 2738 |
. . . . . . . . . 10
⊢
(1r‘(Scalar‘𝑌)) =
(1r‘(Scalar‘𝑌)) |
235 | 1, 233, 27, 234 | lmodvs1 20151 |
. . . . . . . . 9
⊢ ((𝑌 ∈ LMod ∧ (𝐺‘0) ∈
(Base‘𝑌)) →
((1r‘(Scalar‘𝑌)) · (𝐺‘0)) = (𝐺‘0)) |
236 | 229, 232,
235 | syl2an2r 682 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) →
((1r‘(Scalar‘𝑌)) · (𝐺‘0)) = (𝐺‘0)) |
237 | | iftrue 4465 |
. . . . . . . . 9
⊢ (𝑛 = 0 → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
238 | | ovexd 7310 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ V) |
239 | 25, 237, 81, 238 | fvmptd3 6898 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘0) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
240 | 226, 236,
239 | 3eqtrd 2782 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ 𝑋) · (𝐺‘0)) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
241 | 207, 240 | oveq12d 7293 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) + ((0 ↑ 𝑋) · (𝐺‘0))) = ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
242 | 1, 3 | cmncom 19403 |
. . . . . . 7
⊢ ((𝑌 ∈ CMnd ∧ ((0 ↑ 𝑋) · (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) + ((0 ↑ 𝑋) · (𝐺‘0)))) |
243 | 13, 83, 96, 242 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))) + ((0 ↑ 𝑋) · (𝐺‘0)))) |
244 | | ringgrp 19788 |
. . . . . . . . 9
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
245 | 10, 244 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp) |
246 | 245 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Grp) |
247 | 207, 96 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌)) |
248 | 10 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Ring) |
249 | 24, 20, 21, 7, 8 | mat2pmatbas 21875 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
250 | 4, 249 | syl3an2 1163 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
251 | 250 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
252 | | simpl1 1190 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑁 ∈ Fin) |
253 | 208 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑅 ∈ Ring) |
254 | | elmapi 8637 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵) |
255 | 254 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵) |
256 | 255 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵) |
257 | | 0elfz 13353 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ0
→ 0 ∈ (0...𝑠)) |
258 | 34, 257 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ℕ → 0 ∈
(0...𝑠)) |
259 | 258 | ad2antrl 725 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈ (0...𝑠)) |
260 | 256, 259 | ffvelrnd 6962 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑏‘0) ∈ 𝐵) |
261 | 24, 20, 21, 7, 8 | mat2pmatbas 21875 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
262 | 252, 253,
260, 261 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
263 | 1, 22 | ringcl 19800 |
. . . . . . . 8
⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
264 | 248, 251,
262, 263 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
265 | 1, 2, 23, 3 | grpsubadd0sub 18662 |
. . . . . . 7
⊢ ((𝑌 ∈ Grp ∧ (((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
266 | 246, 247,
264, 265 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
267 | 241, 243,
266 | 3eqtr4d 2788 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
268 | 189, 267 | oveq12d 7293 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + (((0 ↑ 𝑋) · (𝐺‘0)) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
269 | 113, 268 | eqtrd 2778 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) + ((0 ↑ 𝑋) · (𝐺‘0))) + (((𝑠 + 1) ↑ 𝑋) · (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
270 | 75, 102, 269 | 3eqtrd 2782 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
271 | 40, 73, 270 | 3eqtrd 2782 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |