MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chcoeffeq Structured version   Visualization version   GIF version

Theorem chcoeffeq 21814
Description: The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 8-Dec-2019.) (Revised by AV, 15-Dec-2019.)
Hypotheses
Ref Expression
chcoeffeq.a 𝐴 = (𝑁 Mat 𝑅)
chcoeffeq.b 𝐵 = (Base‘𝐴)
chcoeffeq.p 𝑃 = (Poly1𝑅)
chcoeffeq.y 𝑌 = (𝑁 Mat 𝑃)
chcoeffeq.r × = (.r𝑌)
chcoeffeq.s = (-g𝑌)
chcoeffeq.0 0 = (0g𝑌)
chcoeffeq.t 𝑇 = (𝑁 matToPolyMat 𝑅)
chcoeffeq.c 𝐶 = (𝑁 CharPlyMat 𝑅)
chcoeffeq.k 𝐾 = (𝐶𝑀)
chcoeffeq.g 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
chcoeffeq.w 𝑊 = (Base‘𝑌)
chcoeffeq.1 1 = (1r𝐴)
chcoeffeq.m = ( ·𝑠𝐴)
chcoeffeq.u 𝑈 = (𝑁 cPolyMatToMat 𝑅)
Assertion
Ref Expression
chcoeffeq ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺𝑛)) = (((coe1𝐾)‘𝑛) 1 ))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝑛,𝐾   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑈,𝑛   𝑛,𝑌   1 ,𝑛   ,𝑛   𝑛,𝑏,𝑠,𝐴   𝐵,𝑏,𝑠   𝑀,𝑏,𝑠   𝑁,𝑏,𝑠   𝑃,𝑏,𝑛,𝑠   𝑅,𝑏,𝑠   𝑇,𝑏,𝑛,𝑠   𝑛,𝑊   𝑌,𝑏,𝑠   0 ,𝑛   × ,𝑛   ,𝑏,𝑛,𝑠
Allowed substitution hints:   𝐶(𝑛,𝑠,𝑏)   × (𝑠,𝑏)   𝑈(𝑠,𝑏)   1 (𝑠,𝑏)   𝐺(𝑠,𝑏)   (𝑠,𝑏)   𝐾(𝑠,𝑏)   𝑊(𝑠,𝑏)   0 (𝑠,𝑏)

Proof of Theorem chcoeffeq
StepHypRef 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 𝑅)
231, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22cpmadumatpoly 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 = ( ·𝑠𝐴)
311, 2, 3, 4, 13, 24, 11, 12, 25, 26, 27, 28, 29, 30, 5, 16, 17, 18, 19, 20, 22cpmidpmat 21801 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑁 pMatToMatPoly 𝑅)‘(𝐾( ·𝑠𝑌)(1r𝑌))) = ((Poly1𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((((coe1𝐾)‘𝑛) 1 )( ·𝑠 ‘(Poly1𝐴))(𝑛(.g‘(mulGrp‘(Poly1𝐴)))(var1𝐴))))))
32 eqid 2739 . . . . . . . 8 (𝑁 CharPlyMat 𝑅) = (𝑁 CharPlyMat 𝑅)
331, 2, 32, 3, 4, 13, 5, 7, 11, 12, 14, 15, 6cpmadurid 21795 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀)))) = (((𝑁 CharPlyMat 𝑅)‘𝑀)( ·𝑠𝑌)(1r𝑌)))
3426fveq1i 6739 . . . . . . . . . . 11 (𝐶𝑀) = ((𝑁 CharPlyMat 𝑅)‘𝑀)
3527, 34eqtri 2767 . . . . . . . . . 10 𝐾 = ((𝑁 CharPlyMat 𝑅)‘𝑀)
3635a1i 11 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐾 = ((𝑁 CharPlyMat 𝑅)‘𝑀))
3736eqcomd 2745 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑁 CharPlyMat 𝑅)‘𝑀) = 𝐾)
3837oveq1d 7249 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (((𝑁 CharPlyMat 𝑅)‘𝑀)( ·𝑠𝑌)(1r𝑌)) = (𝐾( ·𝑠𝑌)(1r𝑌)))
3933, 38eqtrd 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𝐴))))))
4241adantr 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𝐴))))))
4442, 43eqeq12d 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𝐴)))))))
451, 2, 3, 4, 6, 7, 8, 5, 26, 27, 9, 16, 29, 30, 21chcoeffeqlem 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 )))
4645adantr 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 )))
4746adantr 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 )))
4844, 47sylbid 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 )))
4948exp31 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 )))))
5049com24 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 )))))
5140, 50syl5 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 )))))
5251ex 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 ))))))
5352com24 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 ))))))
5431, 39, 53mp2d 49 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀))))) = ((Poly1𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺𝑛))( ·𝑠 ‘(Poly1𝐴))(𝑛(.g‘(mulGrp‘(Poly1𝐴)))(var1𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺𝑛)) = (((coe1𝐾)‘𝑛) 1 ))))
5554impl 459 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (((𝑁 pMatToMatPoly 𝑅)‘((((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀)) × ((𝑁 maAdju 𝑃)‘(((var1𝑅)( ·𝑠𝑌)(1r𝑌)) (𝑇𝑀))))) = ((Poly1𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺𝑛))( ·𝑠 ‘(Poly1𝐴))(𝑛(.g‘(mulGrp‘(Poly1𝐴)))(var1𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺𝑛)) = (((coe1𝐾)‘𝑛) 1 )))
5655reximdva 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 )))
5756reximdva 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 )))
5823, 57mpd 15 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺𝑛)) = (((coe1𝐾)‘𝑛) 1 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2112  wral 3064  wrex 3065  ifcif 4455   class class class wbr 5069  cmpt 5151  cfv 6400  (class class class)co 7234  m cmap 8531  Fincfn 8649  0cc0 10758  1c1 10759   + caddc 10761   < clt 10896  cmin 11091  cn 11859  0cn0 12119  ...cfz 13124  Basecbs 16792  .rcmulr 16835   ·𝑠 cvsca 16838  0gc0g 16976   Σg cgsu 16977  -gcsg 18399  .gcmg 18520  mulGrpcmgp 19536  1rcur 19548  CRingccrg 19595  algSccascl 20846  var1cv1 21128  Poly1cpl1 21129  coe1cco1 21130   Mat cmat 21335   maAdju cmadu 21560   ConstPolyMat ccpmat 21631   matToPolyMat cmat2pmat 21632   cPolyMatToMat ccpmat2mat 21633   pMatToMatPoly cpm2mp 21720   CharPlyMat cchpmat 21754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835  ax-addf 10837  ax-mulf 10838
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-xor 1508  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-ot 4566  df-uni 4836  df-int 4876  df-iun 4922  df-iin 4923  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-se 5527  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-isom 6409  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-of 7490  df-ofr 7491  df-om 7666  df-1st 7782  df-2nd 7783  df-supp 7927  df-tpos 7991  df-cur 8032  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-1o 8225  df-2o 8226  df-er 8414  df-map 8533  df-pm 8534  df-ixp 8602  df-en 8650  df-dom 8651  df-sdom 8652  df-fin 8653  df-fsupp 9015  df-sup 9087  df-oi 9155  df-card 9584  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-div 11519  df-nn 11860  df-2 11922  df-3 11923  df-4 11924  df-5 11925  df-6 11926  df-7 11927  df-8 11928  df-9 11929  df-n0 12120  df-xnn0 12192  df-z 12206  df-dec 12323  df-uz 12468  df-rp 12616  df-fz 13125  df-fzo 13268  df-seq 13606  df-exp 13667  df-hash 13929  df-word 14102  df-lsw 14150  df-concat 14158  df-s1 14185  df-substr 14238  df-pfx 14268  df-splice 14347  df-reverse 14356  df-s2 14445  df-struct 16732  df-sets 16749  df-slot 16767  df-ndx 16777  df-base 16793  df-ress 16817  df-plusg 16847  df-mulr 16848  df-starv 16849  df-sca 16850  df-vsca 16851  df-ip 16852  df-tset 16853  df-ple 16854  df-ds 16856  df-unif 16857  df-hom 16858  df-cco 16859  df-0g 16978  df-gsum 16979  df-prds 16984  df-pws 16986  df-mre 17121  df-mrc 17122  df-acs 17124  df-mgm 18146  df-sgrp 18195  df-mnd 18206  df-mhm 18250  df-submnd 18251  df-efmnd 18328  df-grp 18400  df-minusg 18401  df-sbg 18402  df-mulg 18521  df-subg 18572  df-ghm 18652  df-gim 18695  df-cntz 18743  df-oppg 18770  df-symg 18792  df-pmtr 18866  df-psgn 18915  df-evpm 18916  df-cmn 19204  df-abl 19205  df-mgp 19537  df-ur 19549  df-srg 19553  df-ring 19596  df-cring 19597  df-oppr 19673  df-dvdsr 19691  df-unit 19692  df-invr 19722  df-dvr 19733  df-rnghom 19767  df-drng 19801  df-subrg 19830  df-lmod 19933  df-lss 20001  df-sra 20241  df-rgmod 20242  df-cnfld 20396  df-zring 20468  df-zrh 20502  df-dsmm 20726  df-frlm 20741  df-assa 20847  df-ascl 20849  df-psr 20899  df-mvr 20900  df-mpl 20901  df-opsr 20903  df-psr1 21132  df-vr1 21133  df-ply1 21134  df-coe1 21135  df-mamu 21314  df-mat 21336  df-mdet 21513  df-madu 21562  df-cpmat 21634  df-mat2pmat 21635  df-cpmat2mat 21636  df-decpmat 21691  df-pm2mp 21721  df-chpmat 21755
This theorem is referenced by:  cayhamlem3  21815
  Copyright terms: Public domain W3C validator