Proof of Theorem chcoeffeq
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.t |
. . 3
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
6 | | chcoeffeq.r |
. . 3
⊢ × =
(.r‘𝑌) |
7 | | chcoeffeq.s |
. . 3
⊢ − =
(-g‘𝑌) |
8 | | chcoeffeq.0 |
. . 3
⊢ 0 =
(0g‘𝑌) |
9 | | chcoeffeq.g |
. . 3
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
10 | | eqid 2739 |
. . 3
⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅) |
11 | | eqid 2739 |
. . 3
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
12 | | eqid 2739 |
. . 3
⊢
(1r‘𝑌) = (1r‘𝑌) |
13 | | eqid 2739 |
. . 3
⊢
(var1‘𝑅) = (var1‘𝑅) |
14 | | eqid 2739 |
. . 3
⊢
(((var1‘𝑅)( ·𝑠
‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) = (((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) |
15 | | eqid 2739 |
. . 3
⊢ (𝑁 maAdju 𝑃) = (𝑁 maAdju 𝑃) |
16 | | chcoeffeq.w |
. . 3
⊢ 𝑊 = (Base‘𝑌) |
17 | | eqid 2739 |
. . 3
⊢
(Poly1‘𝐴) = (Poly1‘𝐴) |
18 | | eqid 2739 |
. . 3
⊢
(var1‘𝐴) = (var1‘𝐴) |
19 | | eqid 2739 |
. . 3
⊢ (
·𝑠 ‘(Poly1‘𝐴)) = (
·𝑠 ‘(Poly1‘𝐴)) |
20 | | eqid 2739 |
. . 3
⊢
(.g‘(mulGrp‘(Poly1‘𝐴))) =
(.g‘(mulGrp‘(Poly1‘𝐴))) |
21 | | chcoeffeq.u |
. . 3
⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) |
22 | | eqid 2739 |
. . 3
⊢ (𝑁 pMatToMatPoly 𝑅) = (𝑁 pMatToMatPoly 𝑅) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22 | cpmadumatpoly 21811 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
24 | | eqid 2739 |
. . . . . . 7
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
25 | | eqid 2739 |
. . . . . . 7
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
26 | | chcoeffeq.c |
. . . . . . 7
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
27 | | chcoeffeq.k |
. . . . . . 7
⊢ 𝐾 = (𝐶‘𝑀) |
28 | | eqid 2739 |
. . . . . . 7
⊢ (𝐾(
·𝑠 ‘𝑌)(1r‘𝑌)) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌)) |
29 | | chcoeffeq.1 |
. . . . . . 7
⊢ 1 =
(1r‘𝐴) |
30 | | chcoeffeq.m |
. . . . . . 7
⊢ ∗ = (
·𝑠 ‘𝐴) |
31 | 1, 2, 3, 4, 13, 24, 11, 12, 25, 26, 27, 28, 29, 30, 5, 16, 17, 18, 19, 20, 22 | cpmidpmat 21801 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
32 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑁 CharPlyMat 𝑅) = (𝑁 CharPlyMat 𝑅) |
33 | 1, 2, 32, 3, 4, 13, 5, 7, 11, 12, 14, 15, 6 | cpmadurid 21795 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (((𝑁 CharPlyMat 𝑅)‘𝑀)( ·𝑠
‘𝑌)(1r‘𝑌))) |
34 | 26 | fveq1i 6739 |
. . . . . . . . . . 11
⊢ (𝐶‘𝑀) = ((𝑁 CharPlyMat 𝑅)‘𝑀) |
35 | 27, 34 | eqtri 2767 |
. . . . . . . . . 10
⊢ 𝐾 = ((𝑁 CharPlyMat 𝑅)‘𝑀) |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 = ((𝑁 CharPlyMat 𝑅)‘𝑀)) |
37 | 36 | eqcomd 2745 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑁 CharPlyMat 𝑅)‘𝑀) = 𝐾) |
38 | 37 | oveq1d 7249 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (((𝑁 CharPlyMat 𝑅)‘𝑀)( ·𝑠
‘𝑌)(1r‘𝑌)) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) |
39 | 33, 38 | eqtrd 2779 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) |
40 | | fveq2 6738 |
. . . . . . . . 9
⊢
(((((var1‘𝑅)( ·𝑠
‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌)) → ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌)))) |
41 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
43 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) |
44 | 42, 43 | eqeq12d 2755 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((𝑁
pMatToMatPoly 𝑅)‘(𝐾( ·𝑠 ‘𝑌)(1r‘𝑌))) ↔ ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))))) |
45 | 1, 2, 3, 4, 6, 7, 8, 5, 26, 27, 9, 16, 29, 30, 21 | chcoeffeqlem 21813 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
46 | 45 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → (((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
47 | 46 | adantr 484 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → (((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
48 | 44, 47 | sylbid 243 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ CRing ∧
𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) ∧ ((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴)))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((𝑁
pMatToMatPoly 𝑅)‘(𝐾( ·𝑠 ‘𝑌)(1r‘𝑌))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
49 | 48 | exp31 423 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((𝑁 pMatToMatPoly 𝑅)‘(𝐾(
·𝑠 ‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦
((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((𝑁
pMatToMatPoly 𝑅)‘(𝐾( ·𝑠 ‘𝑌)(1r‘𝑌))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))))) |
50 | 49 | com24 95 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) → (((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))))) |
51 | 40, 50 | syl5 34 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌)) → (((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))))) |
52 | 51 | ex 416 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (𝐾( ·𝑠
‘𝑌)(1r‘𝑌)) → (((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 )))))) |
53 | 52 | com24 95 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠
‘𝑌)(1r‘𝑌))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → (((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)))) = (𝐾(
·𝑠 ‘𝑌)(1r‘𝑌)) → ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵
↑m (0...𝑠))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))
× ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)( ·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))(
·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 )))))) |
54 | 31, 39, 53 | mp2d 49 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 )))) |
55 | 54 | impl 459 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
56 | 55 | reximdva 3203 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (∃𝑏 ∈ (𝐵 ↑m (0...𝑠))((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∃𝑏 ∈ (𝐵
↑m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
57 | 56 | reximdva 3203 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))((𝑁 pMatToMatPoly 𝑅)‘((((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘𝑌)(1r‘𝑌)) − (𝑇‘𝑀))))) = ((Poly1‘𝐴) Σg
(𝑛 ∈
ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠
‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵
↑m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛))
= (((coe1‘𝐾)‘𝑛) ∗ 1 ))) |
58 | 23, 57 | mpd 15 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 )) |