Step | Hyp | Ref
| Expression |
1 | | chcoeffeq.a |
. . 3
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | chcoeffeq.b |
. . 3
⊢ 𝐵 = (Base‘𝐴) |
3 | | chcoeffeq.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | chcoeffeq.y |
. . 3
⊢ 𝑌 = (𝑁 Mat 𝑃) |
5 | | chcoeffeq.r |
. . 3
⊢ × =
(.r‘𝑌) |
6 | | chcoeffeq.s |
. . 3
⊢ − =
(-g‘𝑌) |
7 | | chcoeffeq.0 |
. . 3
⊢ 0 =
(0g‘𝑌) |
8 | | chcoeffeq.t |
. . 3
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
9 | | chcoeffeq.c |
. . 3
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
10 | | chcoeffeq.k |
. . 3
⊢ 𝐾 = (𝐶‘𝑀) |
11 | | chcoeffeq.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
12 | | chcoeffeq.w |
. . 3
⊢ 𝑊 = (Base‘𝑌) |
13 | | chcoeffeq.1 |
. . 3
⊢ 1 =
(1r‘𝐴) |
14 | | chcoeffeq.m |
. . 3
⊢ ∗ = (
·𝑠 ‘𝐴) |
15 | | chcoeffeq.u |
. . 3
⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | chcoeffeq 20691 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 )) |
17 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → (𝐺‘𝑛) = (𝐺‘𝑙)) |
18 | 17 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑛 = 𝑙 → (𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑙))) |
19 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑙 → ((coe1‘𝐾)‘𝑛) = ((coe1‘𝐾)‘𝑙)) |
20 | 19 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑙 → (((coe1‘𝐾)‘𝑛) ∗ 1 ) =
(((coe1‘𝐾)‘𝑙) ∗ 1 )) |
21 | 18, 20 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 𝑙 → ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ))) |
22 | 21 | cbvralv 3171 |
. . . . 5
⊢
(∀𝑛 ∈
ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ↔ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) |
23 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑛 → (𝐺‘𝑙) = (𝐺‘𝑛)) |
24 | 23 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑛 → (𝑈‘(𝐺‘𝑙)) = (𝑈‘(𝐺‘𝑛))) |
25 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑛 → ((coe1‘𝐾)‘𝑙) = ((coe1‘𝐾)‘𝑛)) |
26 | 25 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑛 → (((coe1‘𝐾)‘𝑙) ∗ 1 ) =
(((coe1‘𝐾)‘𝑛) ∗ 1 )) |
27 | 24, 26 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑛 → ((𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) ↔ (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
28 | 27 | rspccva 3308 |
. . . . . . . . . . 11
⊢
((∀𝑙 ∈
ℕ0 (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 )) |
29 | | simprll 802 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵)) |
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑃) =
(Base‘𝑃) |
31 | 9, 1, 2, 3, 30 | chpmatply1 20637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
32 | 29, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
33 | 10, 32 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐾 ∈ (Base‘𝑃)) |
34 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(coe1‘𝐾) = (coe1‘𝐾) |
35 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑅) =
(Base‘𝑅) |
36 | 34, 30, 3, 35 | coe1f 19581 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ (Base‘𝑃) →
(coe1‘𝐾):ℕ0⟶(Base‘𝑅)) |
37 | 33, 36 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
(coe1‘𝐾):ℕ0⟶(Base‘𝑅)) |
38 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑅)
∈ V |
39 | | nn0ex 11298 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 ∈ V |
40 | 38, 39 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Base‘𝑅)
∈ V ∧ ℕ0 ∈ V) |
41 | | elmapg 7870 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((Base‘𝑅)
∈ V ∧ ℕ0 ∈ V) →
((coe1‘𝐾)
∈ ((Base‘𝑅)
↑𝑚 ℕ0) ↔
(coe1‘𝐾):ℕ0⟶(Base‘𝑅))) |
42 | 40, 41 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
((coe1‘𝐾)
∈ ((Base‘𝑅)
↑𝑚 ℕ0) ↔
(coe1‘𝐾):ℕ0⟶(Base‘𝑅))) |
43 | 37, 42 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
(coe1‘𝐾)
∈ ((Base‘𝑅)
↑𝑚 ℕ0)) |
44 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝑛 ∈ ℕ0) |
45 | | cayhamlem.e1 |
. . . . . . . . . . . . . . . . . 18
⊢ ↑ =
(.g‘(mulGrp‘𝐴)) |
46 | | cayhamlem.r |
. . . . . . . . . . . . . . . . . 18
⊢ · =
(.r‘𝐴) |
47 | 35, 1, 2, 13, 14, 45, 46 | cayhamlem2 20689 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ ((coe1‘𝐾) ∈ ((Base‘𝑅) ↑𝑚
ℕ0) ∧ 𝑛 ∈ ℕ0)) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) ·
(((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
48 | 29, 43, 44, 47 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) ·
(((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ∧ (𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) ·
(((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
50 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))) = ((𝑛 ↑ 𝑀) ·
(((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ∧ (𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))))) → ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))) = ((𝑛 ↑ 𝑀) ·
(((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
52 | 49, 51 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ (((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) ∧ (𝑛 ∈ ℕ0
∧ (((𝑁 ∈ Fin ∧
𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))) |
53 | 52 | exp32 631 |
. . . . . . . . . . . . 13
⊢ ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → (𝑛 ∈ ℕ0
→ ((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) |
54 | 53 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) |
55 | 54 | adantl 482 |
. . . . . . . . . . 11
⊢
((∀𝑙 ∈
ℕ0 (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∧ 𝑛 ∈ ℕ0) → ((𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) |
56 | 28, 55 | mpd 15 |
. . . . . . . . . 10
⊢
((∀𝑙 ∈
ℕ0 (𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∧ 𝑛 ∈ ℕ0) → ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))) |
57 | 56 | com12 32 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → ((∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) ∧ 𝑛 ∈ ℕ0) →
(((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))) |
58 | 57 | impl 650 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) ∧ 𝑛 ∈ ℕ0)
→ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))) |
59 | 58 | mpteq2dva 4744 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) → (𝑛 ∈ ℕ0
↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))) |
60 | 59 | oveq2d 6666 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ ∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 )) → (𝐴 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) |
61 | 60 | ex 450 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (∀𝑙 ∈ ℕ0
(𝑈‘(𝐺‘𝑙)) = (((coe1‘𝐾)‘𝑙) ∗ 1 ) → (𝐴 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))))) |
62 | 22, 61 | syl5bi 232 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) → (∀𝑛 ∈ ℕ0
(𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → (𝐴 Σg
(𝑛 ∈
ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))))) |
63 | 62 | reximdva 3017 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))))) |
64 | 63 | reximdva 3017 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛))))))) |
65 | 16, 64 | mpd 15 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0
↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0
↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) |