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

Theorem cayhamlem4 20971
Description: Lemma for cayleyhamilton 20973. (Contributed by AV, 25-Nov-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 𝑅)
cayhamlem.e1 = (.g‘(mulGrp‘𝐴))
cayhamlem.e2 𝐸 = (.g‘(mulGrp‘𝑌))
Assertion
Ref Expression
cayhamlem4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝑛,𝐾   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑈,𝑛   𝑛,𝑌   1 ,𝑛   ,𝑛   𝑛,𝑏,𝑠,𝐴   𝐵,𝑏,𝑠   𝑀,𝑏,𝑠   𝑁,𝑏,𝑠   𝑃,𝑏,𝑛,𝑠   𝑅,𝑏,𝑠   𝑇,𝑏,𝑛,𝑠   𝑛,𝑊   𝑌,𝑏,𝑠   0 ,𝑛   × ,𝑛   ,𝑏,𝑛,𝑠   ,𝑛
Allowed substitution hints:   𝐶(𝑛,𝑠,𝑏)   × (𝑠,𝑏)   𝑈(𝑠,𝑏)   1 (𝑠,𝑏)   𝐸(𝑛,𝑠,𝑏)   (𝑠,𝑏)   𝐺(𝑠,𝑏)   (𝑠,𝑏)   𝐾(𝑠,𝑏)   𝑊(𝑠,𝑏)   0 (𝑠,𝑏)

Proof of Theorem cayhamlem4
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . 3 ((𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
2 simp1 1166 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑁 ∈ Fin)
32ad2antrr 717 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑁 ∈ Fin)
4 crngring 18824 . . . . . . 7 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
543ad2ant2 1164 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
65ad2antrr 717 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑅 ∈ Ring)
7 chcoeffeq.b . . . . . 6 𝐵 = (Base‘𝐴)
8 eqid 2764 . . . . . 6 (0g𝐴) = (0g𝐴)
9 chcoeffeq.a . . . . . . . . . . 11 𝐴 = (𝑁 Mat 𝑅)
109matring 20524 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
114, 10sylan2 586 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
12 ringcmn 18847 . . . . . . . . 9 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
1311, 12syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ CMnd)
14133adant3 1162 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐴 ∈ CMnd)
1514ad2antrr 717 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝐴 ∈ CMnd)
16 nn0ex 11544 . . . . . . 7 0 ∈ V
1716a1i 11 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → ℕ0 ∈ V)
183, 6, 10syl2anc 579 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝐴 ∈ Ring)
1918adantr 472 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
202, 5, 10syl2anc 579 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐴 ∈ Ring)
21 eqid 2764 . . . . . . . . . . . 12 (mulGrp‘𝐴) = (mulGrp‘𝐴)
2221ringmgp 18819 . . . . . . . . . . 11 (𝐴 ∈ Ring → (mulGrp‘𝐴) ∈ Mnd)
2320, 22syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (mulGrp‘𝐴) ∈ Mnd)
2423ad3antrrr 721 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
25 simpr 477 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
26 simpll3 1273 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑀𝐵)
2726adantr 472 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑀𝐵)
2821, 7mgpbas 18761 . . . . . . . . . 10 𝐵 = (Base‘(mulGrp‘𝐴))
29 cayhamlem.e1 . . . . . . . . . 10 = (.g‘(mulGrp‘𝐴))
3028, 29mulgnn0cl 17825 . . . . . . . . 9 (((mulGrp‘𝐴) ∈ Mnd ∧ 𝑛 ∈ ℕ0𝑀𝐵) → (𝑛 𝑀) ∈ 𝐵)
3124, 25, 27, 30syl3anc 1490 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑛 𝑀) ∈ 𝐵)
32 eqid 2764 . . . . . . . . . . . 12 (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
33 chcoeffeq.u . . . . . . . . . . . 12 𝑈 = (𝑁 cPolyMatToMat 𝑅)
349, 7, 32, 33cpm2mf 20835 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
352, 5, 34syl2anc 579 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
3635ad3antrrr 721 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
37 simplr 785 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑠 ∈ ℕ)
38 simpr 477 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑏 ∈ (𝐵𝑚 (0...𝑠)))
39 chcoeffeq.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
40 chcoeffeq.y . . . . . . . . . . . 12 𝑌 = (𝑁 Mat 𝑃)
41 chcoeffeq.r . . . . . . . . . . . 12 × = (.r𝑌)
42 chcoeffeq.s . . . . . . . . . . . 12 = (-g𝑌)
43 chcoeffeq.0 . . . . . . . . . . . 12 0 = (0g𝑌)
44 chcoeffeq.t . . . . . . . . . . . 12 𝑇 = (𝑁 matToPolyMat 𝑅)
45 chcoeffeq.g . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 ((𝑇𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) ((𝑇𝑀) × (𝑇‘(𝑏𝑛))))))))
469, 7, 39, 40, 41, 42, 43, 44, 45, 32chfacfisfcpmat 20938 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
473, 6, 26, 37, 38, 46syl32anc 1497 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
4847ffvelrnda 6548 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ (𝑁 ConstPolyMat 𝑅))
4936, 48ffvelrnd 6549 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺𝑛)) ∈ 𝐵)
50 eqid 2764 . . . . . . . . 9 (.r𝐴) = (.r𝐴)
517, 50ringcl 18827 . . . . . . . 8 ((𝐴 ∈ Ring ∧ (𝑛 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺𝑛)) ∈ 𝐵) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
5219, 31, 49, 51syl3anc 1490 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
5352fmpttd 6574 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))):ℕ0𝐵)
54 fvexd 6389 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (0g𝐴) ∈ V)
55 ovexd 6875 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ V)
569, 7, 39, 40, 41, 42, 43, 44, 45chfacffsupp 20939 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠)))) → 𝐺 finSupp (0g𝑌))
5756anassrs 459 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝐺 finSupp (0g𝑌))
58 ovex 6873 . . . . . . . . . . . . 13 (𝑁 ConstPolyMat 𝑅) ∈ V
5958, 16pm3.2i 462 . . . . . . . . . . . 12 ((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V)
60 elmapg 8072 . . . . . . . . . . . 12 (((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑𝑚0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
6159, 60mp1i 13 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑𝑚0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
6247, 61mpbird 248 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑𝑚0))
63 fvex 6387 . . . . . . . . . 10 (0g𝑌) ∈ V
64 fsuppmapnn0ub 13001 . . . . . . . . . 10 ((𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑𝑚0) ∧ (0g𝑌) ∈ V) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌))))
6562, 63, 64sylancl 580 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌))))
66 csbov12g 6884 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (𝑧 / 𝑛(𝑛 𝑀)(.r𝐴)𝑧 / 𝑛(𝑈‘(𝐺𝑛))))
67 csbov1g 6885 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑛 𝑀) = (𝑧 / 𝑛𝑛 𝑀))
68 csbvarg 4163 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ℕ0𝑧 / 𝑛𝑛 = 𝑧)
6968oveq1d 6856 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0 → (𝑧 / 𝑛𝑛 𝑀) = (𝑧 𝑀))
7067, 69eqtrd 2798 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑛 𝑀) = (𝑧 𝑀))
71 csbfv2g 6419 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑈‘(𝐺𝑛)) = (𝑈𝑧 / 𝑛(𝐺𝑛)))
72 csbfv 6420 . . . . . . . . . . . . . . . . . . . . 21 𝑧 / 𝑛(𝐺𝑛) = (𝐺𝑧)
7372a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝐺𝑛) = (𝐺𝑧))
7473fveq2d 6378 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0 → (𝑈𝑧 / 𝑛(𝐺𝑛)) = (𝑈‘(𝐺𝑧)))
7571, 74eqtrd 2798 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑈‘(𝐺𝑛)) = (𝑈‘(𝐺𝑧)))
7670, 75oveq12d 6859 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0 → (𝑧 / 𝑛(𝑛 𝑀)(.r𝐴)𝑧 / 𝑛(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
7766, 76eqtrd 2798 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ0𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
7877ad2antlr 718 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
79 fveq2 6374 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) = (0g𝑌) → (𝑈‘(𝐺𝑧)) = (𝑈‘(0g𝑌)))
802, 5jca 507 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
8180adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
82 eqid 2764 . . . . . . . . . . . . . . . . . . . 20 (0g𝑌) = (0g𝑌)
839, 33, 39, 40, 8, 82m2cpminv0 20844 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘(0g𝑌)) = (0g𝐴))
8481, 83syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) → (𝑈‘(0g𝑌)) = (0g𝐴))
8584ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑈‘(0g𝑌)) = (0g𝐴))
8679, 85sylan9eqr 2820 . . . . . . . . . . . . . . . 16 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → (𝑈‘(𝐺𝑧)) = (0g𝐴))
8786oveq2d 6857 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))) = ((𝑧 𝑀)(.r𝐴)(0g𝐴)))
8818adantr 472 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝐴 ∈ Ring)
8923ad3antrrr 721 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
90 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑧 ∈ ℕ0)
9126adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑀𝐵)
9228, 29mulgnn0cl 17825 . . . . . . . . . . . . . . . . . . 19 (((mulGrp‘𝐴) ∈ Mnd ∧ 𝑧 ∈ ℕ0𝑀𝐵) → (𝑧 𝑀) ∈ 𝐵)
9389, 90, 91, 92syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑧 𝑀) ∈ 𝐵)
9488, 93jca 507 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵))
9594adantr 472 . . . . . . . . . . . . . . . 16 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → (𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵))
967, 50, 8ringrz 18854 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵) → ((𝑧 𝑀)(.r𝐴)(0g𝐴)) = (0g𝐴))
9795, 96syl 17 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → ((𝑧 𝑀)(.r𝐴)(0g𝐴)) = (0g𝐴))
9878, 87, 973eqtrd 2802 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))
9998ex 401 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → ((𝐺𝑧) = (0g𝑌) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
10099adantlr 706 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝐺𝑧) = (0g𝑌) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
101100imim2d 57 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
102101ralimdva 3108 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑤 ∈ ℕ0) → (∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
103102reximdva 3162 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
10465, 103syld 47 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
10557, 104mpd 15 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
10654, 55, 105mptnn0fsupp 13003 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) finSupp (0g𝐴))
1077, 8, 15, 17, 53, 106gsumcl 18581 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) ∈ 𝐵)
10833, 9, 7, 44m2cpminvid 20836 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) ∈ 𝐵) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
1093, 6, 107, 108syl3anc 1490 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
11039, 40pmatring 20776 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
1112, 5, 110syl2anc 579 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
112 ringmnd 18822 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
113111, 112syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
114113ad2antrr 717 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑌 ∈ Mnd)
115 chcoeffeq.w . . . . . . . . . 10 𝑊 = (Base‘𝑌)
11644, 9, 7, 39, 40, 115mat2pmatghm 20813 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
1173, 6, 116syl2anc 579 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
118 ghmmhm 17935 . . . . . . . 8 (𝑇 ∈ (𝐴 GrpHom 𝑌) → 𝑇 ∈ (𝐴 MndHom 𝑌))
119117, 118syl 17 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → 𝑇 ∈ (𝐴 MndHom 𝑌))
12020ad3antrrr 721 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
1214, 34sylan2 586 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
1221213adant3 1162 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
123122ad3antrrr 721 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
124123, 48ffvelrnd 6549 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺𝑛)) ∈ 𝐵)
125120, 31, 124, 51syl3anc 1490 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
1267, 8, 15, 114, 17, 119, 125, 106gsummptmhm 18605 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))))
12744, 9, 7, 39, 40, 115mat2pmatrhm 20817 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 RingHom 𝑌))
1281273adant3 1162 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑇 ∈ (𝐴 RingHom 𝑌))
129128ad3antrrr 721 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ (𝐴 RingHom 𝑌))
1307, 50, 41rhmmul 18995 . . . . . . . . . 10 ((𝑇 ∈ (𝐴 RingHom 𝑌) ∧ (𝑛 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺𝑛)) ∈ 𝐵) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))))
131129, 31, 124, 130syl3anc 1490 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))))
13244, 9, 7, 39, 40, 115mat2pmatmhm 20816 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
1331323adant3 1162 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
134133ad3antrrr 721 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
135 cayhamlem.e2 . . . . . . . . . . . 12 𝐸 = (.g‘(mulGrp‘𝑌))
13628, 29, 135mhmmulg 17848 . . . . . . . . . . 11 ((𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)) ∧ 𝑛 ∈ ℕ0𝑀𝐵) → (𝑇‘(𝑛 𝑀)) = (𝑛𝐸(𝑇𝑀)))
137134, 25, 27, 136syl3anc 1490 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑛 𝑀)) = (𝑛𝐸(𝑇𝑀)))
1382ad3antrrr 721 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin)
1395ad3antrrr 721 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring)
14032, 33, 44m2cpminvid2 20838 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐺𝑛) ∈ (𝑁 ConstPolyMat 𝑅)) → (𝑇‘(𝑈‘(𝐺𝑛))) = (𝐺𝑛))
141138, 139, 48, 140syl3anc 1490 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑈‘(𝐺𝑛))) = (𝐺𝑛))
142137, 141oveq12d 6859 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))) = ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))
143131, 142eqtrd 2798 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))
144143mpteq2dva 4902 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))
145144oveq2d 6857 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))))
146126, 145eqtr3d 2800 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))))
147146fveq2d 6378 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
148109, 147eqtr3d 2800 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
1491, 148sylan9eqr 2820 . 2 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵𝑚 (0...𝑠))) ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
150 chcoeffeq.c . . 3 𝐶 = (𝑁 CharPlyMat 𝑅)
151 chcoeffeq.k . . 3 𝐾 = (𝐶𝑀)
152 chcoeffeq.1 . . 3 1 = (1r𝐴)
153 chcoeffeq.m . . 3 = ( ·𝑠𝐴)
1549, 7, 39, 40, 41, 42, 43, 44, 150, 151, 45, 115, 152, 153, 33, 29, 50cayhamlem3 20970 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
155149, 154reximddv2 3166 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵𝑚 (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3054  wrex 3055  Vcvv 3349  csb 3690  ifcif 4242   class class class wbr 4808  cmpt 4887  wf 6063  cfv 6067  (class class class)co 6841  𝑚 cmap 8059  Fincfn 8159   finSupp cfsupp 8481  0cc0 10188  1c1 10189   + caddc 10191   < clt 10327  cmin 10519  cn 11273  0cn0 11537  ...cfz 12532  Basecbs 16131  .rcmulr 16216   ·𝑠 cvsca 16219  0gc0g 16367   Σg cgsu 16368  Mndcmnd 17561   MndHom cmhm 17600  -gcsg 17692  .gcmg 17808   GrpHom cghm 17922  CMndccmn 18458  mulGrpcmgp 18755  1rcur 18767  Ringcrg 18813  CRingccrg 18814   RingHom crh 18980  Poly1cpl1 19819  coe1cco1 19820   Mat cmat 20488   ConstPolyMat ccpmat 20786   matToPolyMat cmat2pmat 20787   cPolyMatToMat ccpmat2mat 20788   CharPlyMat cchpmat 20909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-xor 1634  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-ot 4342  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-ofr 7095  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-tpos 7554  df-cur 7595  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-sup 8554  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-xnn0 11610  df-z 11624  df-dec 11740  df-uz 11886  df-rp 12028  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-word 13486  df-lsw 13533  df-concat 13541  df-s1 13566  df-substr 13616  df-pfx 13661  df-splice 13764  df-reverse 13782  df-s2 13878  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-0g 16369  df-gsum 16370  df-prds 16375  df-pws 16377  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-mhm 17602  df-submnd 17603  df-grp 17693  df-minusg 17694  df-sbg 17695  df-mulg 17809  df-subg 17856  df-ghm 17923  df-gim 17966  df-cntz 18014  df-oppg 18040  df-symg 18062  df-pmtr 18126  df-psgn 18175  df-evpm 18176  df-cmn 18460  df-abl 18461  df-mgp 18756  df-ur 18768  df-srg 18772  df-ring 18815  df-cring 18816  df-oppr 18889  df-dvdsr 18907  df-unit 18908  df-invr 18938  df-dvr 18949  df-rnghom 18983  df-drng 19017  df-subrg 19046  df-lmod 19133  df-lss 19201  df-sra 19445  df-rgmod 19446  df-assa 19585  df-ascl 19587  df-psr 19629  df-mvr 19630  df-mpl 19631  df-opsr 19633  df-psr1 19822  df-vr1 19823  df-ply1 19824  df-coe1 19825  df-cnfld 20019  df-zring 20091  df-zrh 20124  df-dsmm 20351  df-frlm 20366  df-mamu 20465  df-mat 20489  df-mdet 20667  df-madu 20716  df-cpmat 20789  df-mat2pmat 20790  df-cpmat2mat 20791  df-decpmat 20846  df-pm2mp 20876  df-chpmat 20910
This theorem is referenced by:  cayleyhamilton0  20972  cayleyhamiltonALT  20974
  Copyright terms: Public domain W3C validator