Proof of Theorem chfacfpmmulgsum
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝑌) =
(Base‘𝑌) |
2 | | cayhamlem1.0 |
. . 3
⊢ 0 =
(0g‘𝑌) |
3 | | chfacfpmmulgsum.p |
. . 3
⊢ + =
(+g‘𝑌) |
4 | | crngring 19428 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
5 | 4 | anim2i 620 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
6 | 5 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
7 | | cayhamlem1.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
8 | | cayhamlem1.y |
. . . . . . 7
⊢ 𝑌 = (𝑁 Mat 𝑃) |
9 | 7, 8 | pmatring 21443 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
10 | 6, 9 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
11 | | ringcmn 19453 |
. . . . 5
⊢ (𝑌 ∈ Ring → 𝑌 ∈ CMnd) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ CMnd) |
13 | 12 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ CMnd) |
14 | | nn0ex 11982 |
. . . 4
⊢
ℕ0 ∈ V |
15 | 14 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ℕ0 ∈
V) |
16 | | simpll 767 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
17 | | simplr 769 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
18 | | simpr 488 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
19 | 16, 17, 18 | 3jca 1129 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈
ℕ0)) |
20 | | cayhamlem1.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
21 | | cayhamlem1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
22 | | cayhamlem1.r |
. . . . 5
⊢ × =
(.r‘𝑌) |
23 | | cayhamlem1.s |
. . . . 5
⊢ − =
(-g‘𝑌) |
24 | | cayhamlem1.t |
. . . . 5
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
25 | | cayhamlem1.g |
. . . . 5
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
26 | | cayhamlem1.e |
. . . . 5
⊢ ↑ =
(.g‘(mulGrp‘𝑌)) |
27 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 21612 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
28 | 19, 27 | syl 17 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
29 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulfsupp 21614 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) finSupp 0 ) |
30 | | nn0disj 13114 |
. . . 4
⊢
((0...(𝑠 + 1)) ∩
(ℤ≥‘((𝑠 + 1) + 1))) = ∅ |
31 | 30 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0...(𝑠 + 1)) ∩
(ℤ≥‘((𝑠 + 1) + 1))) = ∅) |
32 | | nnnn0 11983 |
. . . . . 6
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
33 | | peano2nn0 12016 |
. . . . . 6
⊢ (𝑠 ∈ ℕ0
→ (𝑠 + 1) ∈
ℕ0) |
34 | 32, 33 | syl 17 |
. . . . 5
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ0) |
35 | | nn0split 13113 |
. . . . 5
⊢ ((𝑠 + 1) ∈ ℕ0
→ ℕ0 = ((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝑠 ∈ ℕ →
ℕ0 = ((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
37 | 36 | ad2antrl 728 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ℕ0 =
((0...(𝑠 + 1)) ∪
(ℤ≥‘((𝑠 + 1) + 1)))) |
38 | 1, 2, 3, 13, 15, 28, 29, 31, 37 | gsumsplit2 19168 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))))) |
39 | | simpll 767 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
40 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
41 | | nncn 11724 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
42 | | add1p1 11967 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
44 | 43 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑠 + 1) + 1) = (𝑠 + 2)) |
45 | 44 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) →
(ℤ≥‘((𝑠 + 1) + 1)) =
(ℤ≥‘(𝑠 + 2))) |
46 | 45 | eleq2d 2818 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↔ 𝑖 ∈
(ℤ≥‘(𝑠 + 2)))) |
47 | 46 | biimpa 480 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → 𝑖 ∈
(ℤ≥‘(𝑠 + 2))) |
48 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmul0 21613 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ) |
49 | 39, 40, 47, 48 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1))) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = 0 ) |
50 | 49 | mpteq2dva 5125 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) = (𝑖 ∈ (ℤ≥‘((𝑠 + 1) + 1)) ↦ 0
)) |
51 | 50 | oveq2d 7186 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 ))) |
52 | 4, 9 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring) |
53 | | ringmnd 19426 |
. . . . . . . . . 10
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Mnd) |
55 | 54 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Mnd) |
56 | | fvex 6687 |
. . . . . . . 8
⊢
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V |
57 | 55, 56 | jctir 524 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V)) |
58 | 57 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V)) |
59 | 2 | gsumz 18116 |
. . . . . 6
⊢ ((𝑌 ∈ Mnd ∧
(ℤ≥‘((𝑠 + 1) + 1)) ∈ V) → (𝑌 Σg
(𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 ) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ 0 )) = 0 ) |
61 | 51, 60 | eqtrd 2773 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = 0 ) |
62 | 61 | oveq2d 7186 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) = ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + 0 )) |
63 | | fzfid 13432 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (0...(𝑠 + 1)) ∈ Fin) |
64 | | elfznn0 13091 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...(𝑠 + 1)) → 𝑖 ∈ ℕ0) |
65 | 64, 19 | sylan2 596 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑖 ∈
ℕ0)) |
66 | 65, 27 | syl 17 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...(𝑠 + 1))) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
67 | 66 | ralrimiva 3096 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑖 ∈ (0...(𝑠 + 1))((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
68 | 1, 13, 63, 67 | gsummptcl 19206 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) ∈ (Base‘𝑌)) |
69 | 1, 3, 2 | mndrid 18048 |
. . . 4
⊢ ((𝑌 ∈ Mnd ∧ (𝑌 Σg
(𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) ∈ (Base‘𝑌)) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) |
70 | 55, 68, 69 | syl2an2r 685 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + 0 ) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) |
71 | 62, 70 | eqtrd 2773 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈
(ℤ≥‘((𝑠 + 1) + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) = (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) |
72 | 32 | ad2antrl 728 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑠 ∈ ℕ0) |
73 | 1, 3, 13, 72, 66 | gsummptfzsplit 19171 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))))) |
74 | | elfznn0 13091 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑠) → 𝑖 ∈ ℕ0) |
75 | 74, 28 | sylan2 596 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (0...𝑠)) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
76 | 1, 3, 13, 72, 75 | gsummptfzsplitl 19172 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))))) |
77 | 55 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Mnd) |
78 | | 0nn0 11991 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈
ℕ0) |
80 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 21612 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 0 ∈ ℕ0)
→ ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌)) |
81 | 79, 80 | mpd3an3 1463 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌)) |
82 | | oveq1 7177 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 ↑ (𝑇‘𝑀)) = (0 ↑ (𝑇‘𝑀))) |
83 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝐺‘𝑖) = (𝐺‘0)) |
84 | 82, 83 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑖 = 0 → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) |
85 | 1, 84 | gsumsn 19193 |
. . . . . . 7
⊢ ((𝑌 ∈ Mnd ∧ 0 ∈
ℕ0 ∧ ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) |
86 | 77, 79, 81, 85 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) |
87 | 86 | oveq2d 7186 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {0} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)))) |
88 | 76, 87 | eqtrd 2773 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)))) |
89 | | ovexd 7205 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ V) |
90 | | 1nn0 11992 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
91 | 90 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 1 ∈
ℕ0) |
92 | 72, 91 | nn0addcld 12040 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
93 | 20, 21, 7, 8, 22, 23, 2, 24, 25, 26 | chfacfpmmulcl 21612 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝑠 + 1) ∈ ℕ0) →
(((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) |
94 | 92, 93 | mpd3an3 1463 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) |
95 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑖 = (𝑠 + 1) → (𝑖 ↑ (𝑇‘𝑀)) = ((𝑠 + 1) ↑ (𝑇‘𝑀))) |
96 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑖 = (𝑠 + 1) → (𝐺‘𝑖) = (𝐺‘(𝑠 + 1))) |
97 | 95, 96 | oveq12d 7188 |
. . . . . 6
⊢ (𝑖 = (𝑠 + 1) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) |
98 | 1, 97 | gsumsn 19193 |
. . . . 5
⊢ ((𝑌 ∈ Mnd ∧ (𝑠 + 1) ∈ V ∧ (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) |
99 | 77, 89, 94, 98 | syl3anc 1372 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) |
100 | 88, 99 | oveq12d 7188 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (𝑌 Σg (𝑖 ∈ {(𝑠 + 1)} ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))))) = (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))))) |
101 | | fzfid 13432 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (1...𝑠) ∈ Fin) |
102 | | simpll 767 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
103 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) |
104 | | elfznn 13027 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ) |
105 | 104 | nnnn0d 12036 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℕ0) |
106 | 105 | adantl 485 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 ∈ ℕ0) |
107 | 102, 103,
106, 27 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
108 | 107 | ralrimiva 3096 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑖 ∈ (1...𝑠)((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) ∈ (Base‘𝑌)) |
109 | 1, 13, 101, 108 | gsummptcl 19206 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) ∈ (Base‘𝑌)) |
110 | 1, 3 | mndass 18036 |
. . . . 5
⊢ ((𝑌 ∈ Mnd ∧ ((𝑌 Σg
(𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) ∈ (Base‘𝑌) ∧ ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))))) |
111 | 77, 109, 81, 94, 110 | syl13anc 1373 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))))) |
112 | 104 | nnne0d 11766 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ≠ 0) |
113 | 112 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ 0) |
114 | | neeq1 2996 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑖 → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0)) |
115 | 114 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ 0 ↔ 𝑖 ≠ 0)) |
116 | 113, 115 | mpbird 260 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ 0) |
117 | | eqneqall 2945 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (𝑛 ≠ 0 → 0 = (𝑇‘(𝑏‘(𝑖 − 1))))) |
118 | 116, 117 | mpan9 510 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = (𝑇‘(𝑏‘(𝑖 − 1)))) |
119 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 𝑛 = 𝑖) |
120 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . 17
⊢ (0 =
𝑛 → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
121 | 120 | eqcoms 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
122 | 121 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (0 = 𝑖 ↔ 𝑛 = 𝑖)) |
123 | 119, 122 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → 0 = 𝑖) |
124 | 123 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑏‘0) = (𝑏‘𝑖)) |
125 | 124 | fveq2d 6678 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → (𝑇‘(𝑏‘0)) = (𝑇‘(𝑏‘𝑖))) |
126 | 125 | oveq2d 7186 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) = ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) |
127 | 118, 126 | oveq12d 7188 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
128 | | elfz2 12988 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) ↔ ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (1 ≤
𝑖 ∧ 𝑖 ≤ 𝑠))) |
129 | | zleltp1 12114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑖 ≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
130 | 129 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
131 | 130 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
≤ 𝑠 ↔ 𝑖 < (𝑠 + 1))) |
132 | 131 | biimpcd 252 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ≤ 𝑠 → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1))) |
133 | 132 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1 ≤
𝑖 ∧ 𝑖 ≤ 𝑠) → ((1 ∈ ℤ ∧ 𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → 𝑖 < (𝑠 + 1))) |
134 | 133 | impcom 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → 𝑖 < (𝑠 + 1)) |
135 | 134 | orcd 872 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖)) |
136 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ ℤ → 𝑠 ∈
ℝ) |
137 | | 1red 10720 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 ∈ ℤ → 1 ∈
ℝ) |
138 | 136, 137 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 ∈ ℤ → (𝑠 + 1) ∈
ℝ) |
139 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℝ) |
140 | 138, 139 | anim12ci 617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈
ℝ)) |
141 | 140 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
∈ ℝ ∧ (𝑠 +
1) ∈ ℝ)) |
142 | | lttri2 10801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) →
(𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) → (𝑖
≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
144 | 143 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → (𝑖 ≠ (𝑠 + 1) ↔ (𝑖 < (𝑠 + 1) ∨ (𝑠 + 1) < 𝑖))) |
145 | 135, 144 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ 𝑖
∈ ℤ) ∧ (1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑠)) → 𝑖 ≠ (𝑠 + 1)) |
146 | 128, 145 | sylbi 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ≠ (𝑠 + 1)) |
147 | 146 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 ≠ (𝑠 + 1)) |
148 | | neeq1 2996 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1))) |
149 | 148 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 ≠ (𝑠 + 1) ↔ 𝑖 ≠ (𝑠 + 1))) |
150 | 147, 149 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ≠ (𝑠 + 1)) |
151 | 150 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → 𝑛 ≠ (𝑠 + 1)) |
152 | 151 | neneqd 2939 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → ¬ 𝑛 = (𝑠 + 1)) |
153 | 152 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → (𝑛 = (𝑠 + 1) → (𝑇‘(𝑏‘𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
154 | 153 | imp 410 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏‘𝑠)) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
155 | 104 | nnred 11731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℝ) |
156 | | eleq1w 2815 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝑛 ∈ ℝ ↔ 𝑖 ∈ ℝ)) |
157 | 155, 156 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) → (𝑛 = 𝑖 → 𝑛 ∈ ℝ)) |
158 | 157 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝑛 = 𝑖 → 𝑛 ∈ ℝ)) |
159 | 158 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 ∈ ℝ) |
160 | 72 | nn0red 12037 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑠 ∈ ℝ) |
161 | 160 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑠 ∈ ℝ) |
162 | | 1red 10720 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 1 ∈ ℝ) |
163 | 161, 162 | readdcld 10748 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑠 + 1) ∈ ℝ) |
164 | 128, 134 | sylbi 220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 < (𝑠 + 1)) |
165 | 164 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑖 < (𝑠 + 1)) |
166 | | breq1 5033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1))) |
167 | 166 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → (𝑛 < (𝑠 + 1) ↔ 𝑖 < (𝑠 + 1))) |
168 | 165, 167 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → 𝑛 < (𝑠 + 1)) |
169 | 159, 163,
168 | ltnsymd 10867 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ¬ (𝑠 + 1) < 𝑛) |
170 | 169 | pm2.21d 121 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → ((𝑠 + 1) < 𝑛 → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
171 | 170 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → ((𝑠 + 1) < 𝑛 → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
172 | 171 | imp 410 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
173 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 = 𝑖) |
174 | 173 | fvoveq1d 7192 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘(𝑛 − 1)) = (𝑏‘(𝑖 − 1))) |
175 | 174 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘(𝑛 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1)))) |
176 | 173 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑏‘𝑛) = (𝑏‘𝑖)) |
177 | 176 | fveq2d 6678 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → (𝑇‘(𝑏‘𝑛)) = (𝑇‘(𝑏‘𝑖))) |
178 | 177 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) = ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) |
179 | 175, 178 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢
((((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
180 | 172, 179 | ifeqda 4450 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
181 | 154, 180 | ifeqda 4450 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
182 | 127, 181 | ifeqda 4450 |
. . . . . . . . 9
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) ∧ 𝑛 = 𝑖) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
183 | | ovexd 7205 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))) ∈ V) |
184 | 25, 182, 106, 183 | fvmptd2 6783 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → (𝐺‘𝑖) = ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))) |
185 | 184 | oveq2d 7186 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ (1...𝑠)) → ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)) = ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))) |
186 | 185 | mpteq2dva 5125 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) = (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) |
187 | 186 | oveq2d 7186 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖)))))))) |
188 | | nn0p1gt0 12005 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ0
→ 0 < (𝑠 +
1)) |
189 | | 0red 10722 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℕ0
→ 0 ∈ ℝ) |
190 | | ltne 10815 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 0 < (𝑠 + 1)) → (𝑠 + 1) ≠ 0) |
191 | 189, 190 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℕ0
∧ 0 < (𝑠 + 1))
→ (𝑠 + 1) ≠
0) |
192 | | neeq1 2996 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑠 + 1) → (𝑛 ≠ 0 ↔ (𝑠 + 1) ≠ 0)) |
193 | 191, 192 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℕ0
∧ 0 < (𝑠 + 1))
→ (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
194 | 32, 188, 193 | syl2anc2 588 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℕ → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
195 | 194 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑛 = (𝑠 + 1) → 𝑛 ≠ 0)) |
196 | 195 | imp 410 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → 𝑛 ≠ 0) |
197 | | eqneqall 2945 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → (𝑛 ≠ 0 → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏‘𝑠)))) |
198 | 196, 197 | mpan9 510 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = (𝑇‘(𝑏‘𝑠))) |
199 | | iftrue 4420 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑠 + 1) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = (𝑇‘(𝑏‘𝑠))) |
200 | 199 | ad2antlr 727 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) = (𝑇‘(𝑏‘𝑠))) |
201 | 198, 200 | ifeqda 4450 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 = (𝑠 + 1)) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = (𝑇‘(𝑏‘𝑠))) |
202 | 72, 33 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈
ℕ0) |
203 | | fvexd 6689 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘𝑠)) ∈ V) |
204 | 25, 201, 202, 203 | fvmptd2 6783 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘(𝑠 + 1)) = (𝑇‘(𝑏‘𝑠))) |
205 | 204 | oveq2d 7186 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠)))) |
206 | 24, 20, 21, 7, 8 | mat2pmatbas 21477 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
207 | 4, 206 | syl3an2 1165 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
208 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
209 | 208, 1 | mgpbas 19364 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑌) =
(Base‘(mulGrp‘𝑌)) |
210 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(0g‘(mulGrp‘𝑌)) =
(0g‘(mulGrp‘𝑌)) |
211 | 209, 210,
26 | mulg0 18349 |
. . . . . . . . . . . 12
⊢ ((𝑇‘𝑀) ∈ (Base‘𝑌) → (0 ↑ (𝑇‘𝑀)) =
(0g‘(mulGrp‘𝑌))) |
212 | 207, 211 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0 ↑ (𝑇‘𝑀)) =
(0g‘(mulGrp‘𝑌))) |
213 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(1r‘𝑌) = (1r‘𝑌) |
214 | 208, 213 | ringidval 19372 |
. . . . . . . . . . 11
⊢
(1r‘𝑌) = (0g‘(mulGrp‘𝑌)) |
215 | 212, 214 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0 ↑ (𝑇‘𝑀)) = (1r‘𝑌)) |
216 | 215 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (0 ↑ (𝑇‘𝑀)) = (1r‘𝑌)) |
217 | 216 | oveq1d 7185 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) = ((1r‘𝑌) × (𝐺‘0))) |
218 | 52 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
219 | 20, 21, 7, 8, 22, 23, 2, 24, 25 | chfacfisf 21605 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) |
220 | 4, 219 | syl3anl2 1414 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) |
221 | 220, 79 | ffvelrnd 6862 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘0) ∈ (Base‘𝑌)) |
222 | 1, 22, 213 | ringlidm 19443 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Ring ∧ (𝐺‘0) ∈
(Base‘𝑌)) →
((1r‘𝑌)
×
(𝐺‘0)) = (𝐺‘0)) |
223 | 218, 221,
222 | syl2an2r 685 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((1r‘𝑌) × (𝐺‘0)) = (𝐺‘0)) |
224 | | iftrue 4420 |
. . . . . . . . 9
⊢ (𝑛 = 0 → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
225 | | ovexd 7205 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ V) |
226 | 25, 224, 79, 225 | fvmptd3 6798 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝐺‘0) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
227 | 217, 223,
226 | 3eqtrd 2777 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) = ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
228 | 205, 227 | oveq12d 7188 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
229 | 1, 3 | cmncom 19041 |
. . . . . . 7
⊢ ((𝑌 ∈ CMnd ∧ ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) ∈ (Base‘𝑌)) → (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)))) |
230 | 13, 81, 94, 229 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)))) |
231 | | ringgrp 19421 |
. . . . . . . . 9
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
232 | 10, 231 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp) |
233 | 232 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Grp) |
234 | 205, 94 | eqeltrrd 2834 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌)) |
235 | 10 | adantr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Ring) |
236 | 207 | adantr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
237 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑁 ∈ Fin) |
238 | 4 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
239 | 238 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑅 ∈ Ring) |
240 | | elmapi 8459 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵) |
241 | 240 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵) |
242 | 241 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵) |
243 | | 0elfz 13095 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ0
→ 0 ∈ (0...𝑠)) |
244 | 32, 243 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ℕ → 0 ∈
(0...𝑠)) |
245 | 244 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈ (0...𝑠)) |
246 | 242, 245 | ffvelrnd 6862 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑏‘0) ∈ 𝐵) |
247 | 24, 20, 21, 7, 8 | mat2pmatbas 21477 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
248 | 237, 239,
246, 247 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
249 | 1, 22 | ringcl 19433 |
. . . . . . . 8
⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
250 | 235, 236,
248, 249 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
251 | 1, 2, 23, 3 | grpsubadd0sub 18304 |
. . . . . . 7
⊢ ((𝑌 ∈ Grp ∧ (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌) ∧ ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
252 | 233, 234,
250, 251 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) + ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
253 | 228, 230,
252 | 3eqtr4d 2783 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) |
254 | 187, 253 | oveq12d 7188 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + (((0 ↑ (𝑇‘𝑀)) × (𝐺‘0)) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
255 | 111, 254 | eqtrd 2773 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) + ((0 ↑ (𝑇‘𝑀)) × (𝐺‘0))) + (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝐺‘(𝑠 + 1)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
256 | 73, 100, 255 | 3eqtrd 2777 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (0...(𝑠 + 1)) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
257 | 38, 71, 256 | 3eqtrd 2777 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |