Step | Hyp | Ref
| Expression |
1 | | cayhamlem1.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | cayhamlem1.b |
. . 3
⊢ 𝐵 = (Base‘𝐴) |
3 | | cayhamlem1.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | cayhamlem1.y |
. . 3
⊢ 𝑌 = (𝑁 Mat 𝑃) |
5 | | cayhamlem1.r |
. . 3
⊢ × =
(.r‘𝑌) |
6 | | cayhamlem1.s |
. . 3
⊢ − =
(-g‘𝑌) |
7 | | cayhamlem1.0 |
. . 3
⊢ 0 =
(0g‘𝑌) |
8 | | cayhamlem1.t |
. . 3
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
9 | | cayhamlem1.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
10 | | cayhamlem1.e |
. . 3
⊢ ↑ =
(.g‘(mulGrp‘𝑌)) |
11 | | eqid 2622 |
. . 3
⊢
(+g‘𝑌) = (+g‘𝑌) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | chfacfpmmulgsum2 20670 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖))))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
13 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℤ) |
14 | 13 | zcnd 11483 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 ∈ ℂ) |
15 | | pncan1 10454 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℂ → ((𝑖 + 1) − 1) = 𝑖) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑠) → ((𝑖 + 1) − 1) = 𝑖) |
17 | 16 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...𝑠) → 𝑖 = ((𝑖 + 1) − 1)) |
18 | 17 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑠)) → 𝑖 = ((𝑖 + 1) − 1)) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑠)) → (𝑏‘𝑖) = (𝑏‘((𝑖 + 1) − 1))) |
20 | 19 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑠)) → (𝑇‘(𝑏‘𝑖)) = (𝑇‘(𝑏‘((𝑖 + 1) − 1)))) |
21 | 20 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖))) = (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1))))) |
22 | 21 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑠)) → (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))) = (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1)))))) |
23 | 22 | mpteq2dva 4744 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖))))) = (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1))))))) |
24 | 23 | oveq2d 6666 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1)))))))) |
25 | 24 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1)))))))) |
26 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑌) |
27 | | crngring 18558 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
28 | 27 | anim2i 593 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
29 | 28 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
30 | 3, 4 | pmatring 20498 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
32 | | ringabl 18580 |
. . . . . . 7
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Abel) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Abel) |
34 | 33 | adantr 481 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑌 ∈ Abel) |
35 | | elnnuz 11724 |
. . . . . . 7
⊢ (𝑠 ∈ ℕ ↔ 𝑠 ∈
(ℤ≥‘1)) |
36 | 35 | biimpi 206 |
. . . . . 6
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
(ℤ≥‘1)) |
37 | 36 | ad2antrl 764 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑠 ∈
(ℤ≥‘1)) |
38 | 31 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑌 ∈ Ring) |
39 | 38 | adantr 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → 𝑌 ∈ Ring) |
40 | 28, 30 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑌 ∈ Ring) |
41 | 40 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring) |
42 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑌) =
(mulGrp‘𝑌) |
43 | 42 | ringmgp 18553 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ Ring →
(mulGrp‘𝑌) ∈
Mnd) |
44 | 41, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑌) ∈ Mnd) |
45 | 44 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (mulGrp‘𝑌) ∈ Mnd) |
46 | 45 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (mulGrp‘𝑌) ∈ Mnd) |
47 | | mndmgm 17300 |
. . . . . . . . 9
⊢
((mulGrp‘𝑌)
∈ Mnd → (mulGrp‘𝑌) ∈ Mgm) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (mulGrp‘𝑌) ∈ Mgm) |
49 | | elfznn 12370 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...(𝑠 + 1)) → 𝑘 ∈ ℕ) |
50 | 49 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → 𝑘 ∈ ℕ) |
51 | 8, 1, 2, 3, 4 | mat2pmatbas 20531 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
52 | 27, 51 | syl3an2 1360 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
53 | 52 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
54 | 53 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (𝑇‘𝑀) ∈ (Base‘𝑌)) |
55 | 42, 26 | mgpbas 18495 |
. . . . . . . . 9
⊢
(Base‘𝑌) =
(Base‘(mulGrp‘𝑌)) |
56 | 55, 10 | mulgnncl 17556 |
. . . . . . . 8
⊢
(((mulGrp‘𝑌)
∈ Mgm ∧ 𝑘 ∈
ℕ ∧ (𝑇‘𝑀) ∈ (Base‘𝑌)) → (𝑘 ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌)) |
57 | 48, 50, 54, 56 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (𝑘 ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌)) |
58 | | simpl1 1064 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑁 ∈ Fin) |
59 | 58 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → 𝑁 ∈ Fin) |
60 | 27 | 3ad2ant2 1083 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
61 | 60 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑅 ∈ Ring) |
62 | 61 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → 𝑅 ∈ Ring) |
63 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵) |
64 | 63 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵) |
65 | 64 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑏:(0...𝑠)⟶𝐵) |
66 | 65 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → 𝑏:(0...𝑠)⟶𝐵) |
67 | | nnz 11399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
68 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ) |
69 | 68 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℤ) |
70 | | elfzm1b 12418 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℤ ∧ (𝑠 + 1) ∈ ℤ) →
(𝑘 ∈ (1...(𝑠 + 1)) ↔ (𝑘 − 1) ∈ (0...((𝑠 + 1) −
1)))) |
71 | 67, 69, 70 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑘 ∈ (1...(𝑠 + 1)) ↔ (𝑘 − 1) ∈ (0...((𝑠 + 1) − 1)))) |
72 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℂ) |
73 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) − 1) = 𝑠) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) − 1) = 𝑠) |
75 | 74 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑠 + 1) − 1) = 𝑠) |
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) →
(0...((𝑠 + 1) − 1)) =
(0...𝑠)) |
77 | 76 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑘 − 1) ∈ (0...((𝑠 + 1) − 1)) ↔ (𝑘 − 1) ∈ (0...𝑠))) |
78 | 77 | biimpd 219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) → ((𝑘 − 1) ∈ (0...((𝑠 + 1) − 1)) → (𝑘 − 1) ∈ (0...𝑠))) |
79 | 71, 78 | sylbid 230 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑘 ∈ (1...(𝑠 + 1)) → (𝑘 − 1) ∈ (0...𝑠))) |
80 | 79 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℕ → (𝑘 ∈ ℕ → (𝑘 ∈ (1...(𝑠 + 1)) → (𝑘 − 1) ∈ (0...𝑠)))) |
81 | 80 | com13 88 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑠 + 1)) → (𝑘 ∈ ℕ → (𝑠 ∈ ℕ → (𝑘 − 1) ∈ (0...𝑠)))) |
82 | 49, 81 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(𝑠 + 1)) → (𝑠 ∈ ℕ → (𝑘 − 1) ∈ (0...𝑠))) |
83 | 82 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ℕ → (𝑘 ∈ (1...(𝑠 + 1)) → (𝑘 − 1) ∈ (0...𝑠))) |
84 | 83 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑘 ∈ (1...(𝑠 + 1)) → (𝑘 − 1) ∈ (0...𝑠))) |
85 | 84 | imp 445 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (𝑘 − 1) ∈ (0...𝑠)) |
86 | 66, 85 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (𝑏‘(𝑘 − 1)) ∈ 𝐵) |
87 | 8, 1, 2, 3, 4 | mat2pmatbas 20531 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑘 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑘 − 1))) ∈ (Base‘𝑌)) |
88 | 59, 62, 86, 87 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → (𝑇‘(𝑏‘(𝑘 − 1))) ∈ (Base‘𝑌)) |
89 | 26, 5 | ringcl 18561 |
. . . . . . 7
⊢ ((𝑌 ∈ Ring ∧ (𝑘 ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘(𝑘 − 1))) ∈ (Base‘𝑌)) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) ∈ (Base‘𝑌)) |
90 | 39, 57, 88, 89 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) ∧ 𝑘 ∈ (1...(𝑠 + 1))) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) ∈ (Base‘𝑌)) |
91 | 90 | ralrimiva 2966 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ∀𝑘 ∈ (1...(𝑠 + 1))((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) ∈ (Base‘𝑌)) |
92 | | oveq1 6657 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝑘 ↑ (𝑇‘𝑀)) = (𝑖 ↑ (𝑇‘𝑀))) |
93 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (𝑘 − 1) = (𝑖 − 1)) |
94 | 93 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝑏‘(𝑘 − 1)) = (𝑏‘(𝑖 − 1))) |
95 | 94 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝑇‘(𝑏‘(𝑘 − 1))) = (𝑇‘(𝑏‘(𝑖 − 1)))) |
96 | 92, 95 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = 𝑖 → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) = ((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1))))) |
97 | | oveq1 6657 |
. . . . . 6
⊢ (𝑘 = (𝑖 + 1) → (𝑘 ↑ (𝑇‘𝑀)) = ((𝑖 + 1) ↑ (𝑇‘𝑀))) |
98 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑘 = (𝑖 + 1) → (𝑘 − 1) = ((𝑖 + 1) − 1)) |
99 | 98 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = (𝑖 + 1) → (𝑏‘(𝑘 − 1)) = (𝑏‘((𝑖 + 1) − 1))) |
100 | 99 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = (𝑖 + 1) → (𝑇‘(𝑏‘(𝑘 − 1))) = (𝑇‘(𝑏‘((𝑖 + 1) − 1)))) |
101 | 97, 100 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = (𝑖 + 1) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) = (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1))))) |
102 | | oveq1 6657 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑘 ↑ (𝑇‘𝑀)) = (1 ↑ (𝑇‘𝑀))) |
103 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝑘 − 1) = (1 − 1)) |
104 | 103 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑏‘(𝑘 − 1)) = (𝑏‘(1 − 1))) |
105 | 104 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 1 → (𝑇‘(𝑏‘(𝑘 − 1))) = (𝑇‘(𝑏‘(1 − 1)))) |
106 | 102, 105 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = 1 → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) = ((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1))))) |
107 | | oveq1 6657 |
. . . . . 6
⊢ (𝑘 = (𝑠 + 1) → (𝑘 ↑ (𝑇‘𝑀)) = ((𝑠 + 1) ↑ (𝑇‘𝑀))) |
108 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑘 = (𝑠 + 1) → (𝑘 − 1) = ((𝑠 + 1) − 1)) |
109 | 108 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = (𝑠 + 1) → (𝑏‘(𝑘 − 1)) = (𝑏‘((𝑠 + 1) − 1))) |
110 | 109 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = (𝑠 + 1) → (𝑇‘(𝑏‘(𝑘 − 1))) = (𝑇‘(𝑏‘((𝑠 + 1) − 1)))) |
111 | 107, 110 | oveq12d 6668 |
. . . . 5
⊢ (𝑘 = (𝑠 + 1) → ((𝑘 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑘 − 1)))) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) − 1))))) |
112 | 26, 34, 6, 37, 91, 96, 101, 106, 111 | telgsumfz 18387 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑖 + 1) − 1))))))) = (((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) − 1)))))) |
113 | 25, 112 | eqtrd 2656 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))))) = (((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) − 1)))))) |
114 | 113 | oveq1d 6665 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖))))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) = ((((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) −
1)))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
115 | 55, 10 | mulg1 17548 |
. . . . . . . 8
⊢ ((𝑇‘𝑀) ∈ (Base‘𝑌) → (1 ↑ (𝑇‘𝑀)) = (𝑇‘𝑀)) |
116 | 52, 115 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (1 ↑ (𝑇‘𝑀)) = (𝑇‘𝑀)) |
117 | 116 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (1 ↑ (𝑇‘𝑀)) = (𝑇‘𝑀)) |
118 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 1 ∈
ℂ) |
119 | 118 | subidd 10380 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (1 − 1) =
0) |
120 | 119 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑏‘(1 − 1)) = (𝑏‘0)) |
121 | 120 | fveq2d 6195 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘(1 − 1))) = (𝑇‘(𝑏‘0))) |
122 | 117, 121 | oveq12d 6668 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) = ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) |
123 | 72 | ad2antrl 764 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑠 ∈ ℂ) |
124 | 123, 118 | pncand 10393 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑠 + 1) − 1) = 𝑠) |
125 | 124 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑏‘((𝑠 + 1) − 1)) = (𝑏‘𝑠)) |
126 | 125 | fveq2d 6195 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘((𝑠 + 1) − 1))) = (𝑇‘(𝑏‘𝑠))) |
127 | 126 | oveq2d 6666 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) − 1)))) = (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠)))) |
128 | 122, 127 | oveq12d 6668 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) − 1))))) = (((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))))) |
129 | 128 | oveq1d 6665 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) −
1)))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) = ((((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
130 | | ringgrp 18552 |
. . . . . 6
⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp) |
131 | 31, 130 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp) |
132 | 131 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑌 ∈ Grp) |
133 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℕ0) |
134 | | 0elfz 12436 |
. . . . . . . . 9
⊢ (𝑠 ∈ ℕ0
→ 0 ∈ (0...𝑠)) |
135 | 133, 134 | syl 17 |
. . . . . . . 8
⊢ (𝑠 ∈ ℕ → 0 ∈
(0...𝑠)) |
136 | 135 | ad2antrl 764 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 0 ∈ (0...𝑠)) |
137 | 65, 136 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑏‘0) ∈ 𝐵) |
138 | 8, 1, 2, 3, 4 | mat2pmatbas 20531 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
139 | 58, 61, 137, 138 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) |
140 | 26, 5 | ringcl 18561 |
. . . . 5
⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
141 | 38, 53, 139, 140 | syl3anc 1326 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) |
142 | 45, 47 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (mulGrp‘𝑌) ∈ Mgm) |
143 | | simprl 794 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑠 ∈ ℕ) |
144 | 143 | peano2nnd 11037 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑠 + 1) ∈ ℕ) |
145 | 55, 10 | mulgnncl 17556 |
. . . . . 6
⊢
(((mulGrp‘𝑌)
∈ Mgm ∧ (𝑠 + 1)
∈ ℕ ∧ (𝑇‘𝑀) ∈ (Base‘𝑌)) → ((𝑠 + 1) ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌)) |
146 | 142, 144,
53, 145 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑠 + 1) ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌)) |
147 | | nn0fz0 12437 |
. . . . . . . . 9
⊢ (𝑠 ∈ ℕ0
↔ 𝑠 ∈ (0...𝑠)) |
148 | 133, 147 | sylib 208 |
. . . . . . . 8
⊢ (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠)) |
149 | 148 | ad2antrl 764 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑠 ∈ (0...𝑠)) |
150 | 65, 149 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑏‘𝑠) ∈ 𝐵) |
151 | 8, 1, 2, 3, 4 | mat2pmatbas 20531 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘𝑠) ∈ 𝐵) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
152 | 58, 61, 150, 151 | syl3anc 1326 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) |
153 | 26, 5 | ringcl 18561 |
. . . . 5
⊢ ((𝑌 ∈ Ring ∧ ((𝑠 + 1) ↑ (𝑇‘𝑀)) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌)) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌)) |
154 | 38, 146, 152, 153 | syl3anc 1326 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌)) |
155 | 26, 11, 6, 7 | grpnpncan0 17511 |
. . . 4
⊢ ((𝑌 ∈ Grp ∧ (((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌) ∧ (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) ∈ (Base‘𝑌))) → ((((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) = 0 ) |
156 | 132, 141,
154, 155 | syl12anc 1324 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) = 0 ) |
157 | 129, 156 | eqtrd 2656 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((((1 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(1 − 1)))) − (((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘((𝑠 + 1) −
1)))))(+g‘𝑌)((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))))) = 0 ) |
158 | 12, 114, 157 | 3eqtrd 2660 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0
↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = 0 ) |