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

Theorem cayhamlem4 22109
Description: Lemma for cayleyhamilton 22111. (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 ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (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 1135 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑁 ∈ Fin)
32ad2antrr 723 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑁 ∈ Fin)
4 crngring 19863 . . . . . . 7 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
543ad2ant2 1133 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
65ad2antrr 723 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑅 ∈ Ring)
7 chcoeffeq.b . . . . . 6 𝐵 = (Base‘𝐴)
8 eqid 2737 . . . . . 6 (0g𝐴) = (0g𝐴)
9 chcoeffeq.a . . . . . . . . . . 11 𝐴 = (𝑁 Mat 𝑅)
109matring 21664 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
114, 10sylan2 593 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
12 ringcmn 19888 . . . . . . . . 9 (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
1311, 12syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ CMnd)
14133adant3 1131 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐴 ∈ CMnd)
1514ad2antrr 723 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐴 ∈ CMnd)
16 nn0ex 12312 . . . . . . 7 0 ∈ V
1716a1i 11 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → ℕ0 ∈ V)
183, 6, 10syl2anc 584 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐴 ∈ Ring)
1918adantr 481 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
202, 5, 10syl2anc 584 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝐴 ∈ Ring)
21 eqid 2737 . . . . . . . . . . . 12 (mulGrp‘𝐴) = (mulGrp‘𝐴)
2221ringmgp 19857 . . . . . . . . . . 11 (𝐴 ∈ Ring → (mulGrp‘𝐴) ∈ Mnd)
2320, 22syl 17 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (mulGrp‘𝐴) ∈ Mnd)
2423ad3antrrr 727 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
25 simpr 485 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
26 simpll3 1213 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑀𝐵)
2726adantr 481 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑀𝐵)
2821, 7mgpbas 19794 . . . . . . . . . 10 𝐵 = (Base‘(mulGrp‘𝐴))
29 cayhamlem.e1 . . . . . . . . . 10 = (.g‘(mulGrp‘𝐴))
3028, 29mulgnn0cl 18789 . . . . . . . . 9 (((mulGrp‘𝐴) ∈ Mnd ∧ 𝑛 ∈ ℕ0𝑀𝐵) → (𝑛 𝑀) ∈ 𝐵)
3124, 25, 27, 30syl3anc 1370 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑛 𝑀) ∈ 𝐵)
32 eqid 2737 . . . . . . . . . . . 12 (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
33 chcoeffeq.u . . . . . . . . . . . 12 𝑈 = (𝑁 cPolyMatToMat 𝑅)
349, 7, 32, 33cpm2mf 21973 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
352, 5, 34syl2anc 584 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
3635ad3antrrr 727 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
37 simplr 766 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑠 ∈ ℕ)
38 simpr 485 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑏 ∈ (𝐵m (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 22076 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
473, 6, 26, 37, 38, 46syl32anc 1377 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
4847ffvelcdmda 7000 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝐺𝑛) ∈ (𝑁 ConstPolyMat 𝑅))
4936, 48ffvelcdmd 7001 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺𝑛)) ∈ 𝐵)
50 eqid 2737 . . . . . . . . 9 (.r𝐴) = (.r𝐴)
517, 50ringcl 19868 . . . . . . . 8 ((𝐴 ∈ Ring ∧ (𝑛 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺𝑛)) ∈ 𝐵) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
5219, 31, 49, 51syl3anc 1370 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
5352fmpttd 7028 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))):ℕ0𝐵)
54 fvexd 6826 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (0g𝐴) ∈ V)
55 ovexd 7350 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ V)
569, 7, 39, 40, 41, 42, 43, 44, 45chfacffsupp 22077 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵m (0...𝑠)))) → 𝐺 finSupp (0g𝑌))
5756anassrs 468 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐺 finSupp (0g𝑌))
58 ovex 7348 . . . . . . . . . . . . 13 (𝑁 ConstPolyMat 𝑅) ∈ V
5958, 16pm3.2i 471 . . . . . . . . . . . 12 ((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V)
60 elmapg 8676 . . . . . . . . . . . 12 (((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
6159, 60mp1i 13 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
6247, 61mpbird 256 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m0))
63 fvex 6824 . . . . . . . . . 10 (0g𝑌) ∈ V
64 fsuppmapnn0ub 13788 . . . . . . . . . 10 ((𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m0) ∧ (0g𝑌) ∈ V) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌))))
6562, 63, 64sylancl 586 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌))))
66 csbov12g 7359 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (𝑧 / 𝑛(𝑛 𝑀)(.r𝐴)𝑧 / 𝑛(𝑈‘(𝐺𝑛))))
67 csbov1g 7360 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑛 𝑀) = (𝑧 / 𝑛𝑛 𝑀))
68 csbvarg 4376 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ℕ0𝑧 / 𝑛𝑛 = 𝑧)
6968oveq1d 7330 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0 → (𝑧 / 𝑛𝑛 𝑀) = (𝑧 𝑀))
7067, 69eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑛 𝑀) = (𝑧 𝑀))
71 csbfv2g 6857 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑈‘(𝐺𝑛)) = (𝑈𝑧 / 𝑛(𝐺𝑛)))
72 csbfv 6858 . . . . . . . . . . . . . . . . . . . . 21 𝑧 / 𝑛(𝐺𝑛) = (𝐺𝑧)
7372a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝐺𝑛) = (𝐺𝑧))
7473fveq2d 6815 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℕ0 → (𝑈𝑧 / 𝑛(𝐺𝑛)) = (𝑈‘(𝐺𝑧)))
7571, 74eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℕ0𝑧 / 𝑛(𝑈‘(𝐺𝑛)) = (𝑈‘(𝐺𝑧)))
7670, 75oveq12d 7333 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℕ0 → (𝑧 / 𝑛(𝑛 𝑀)(.r𝐴)𝑧 / 𝑛(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
7766, 76eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ0𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
7877ad2antlr 724 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))))
79 fveq2 6811 . . . . . . . . . . . . . . . . 17 ((𝐺𝑧) = (0g𝑌) → (𝑈‘(𝐺𝑧)) = (𝑈‘(0g𝑌)))
802, 5jca 512 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
8180adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
82 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (0g𝑌) = (0g𝑌)
839, 33, 39, 40, 8, 82m2cpminv0 21982 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘(0g𝑌)) = (0g𝐴))
8481, 83syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) → (𝑈‘(0g𝑌)) = (0g𝐴))
8584ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑈‘(0g𝑌)) = (0g𝐴))
8679, 85sylan9eqr 2799 . . . . . . . . . . . . . . . 16 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → (𝑈‘(𝐺𝑧)) = (0g𝐴))
8786oveq2d 7331 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → ((𝑧 𝑀)(.r𝐴)(𝑈‘(𝐺𝑧))) = ((𝑧 𝑀)(.r𝐴)(0g𝐴)))
8818adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝐴 ∈ Ring)
8923ad3antrrr 727 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
90 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑧 ∈ ℕ0)
9126adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑀𝐵)
9228, 29mulgnn0cl 18789 . . . . . . . . . . . . . . . . . . 19 (((mulGrp‘𝐴) ∈ Mnd ∧ 𝑧 ∈ ℕ0𝑀𝐵) → (𝑧 𝑀) ∈ 𝐵)
9389, 90, 91, 92syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑧 𝑀) ∈ 𝐵)
9488, 93jca 512 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵))
9594adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → (𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵))
967, 50, 8ringrz 19895 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Ring ∧ (𝑧 𝑀) ∈ 𝐵) → ((𝑧 𝑀)(.r𝐴)(0g𝐴)) = (0g𝐴))
9795, 96syl 17 . . . . . . . . . . . . . . 15 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → ((𝑧 𝑀)(.r𝐴)(0g𝐴)) = (0g𝐴))
9878, 87, 973eqtrd 2781 . . . . . . . . . . . . . 14 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺𝑧) = (0g𝑌)) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))
9998ex 413 . . . . . . . . . . . . 13 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → ((𝐺𝑧) = (0g𝑌) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
10099adantlr 712 . . . . . . . . . . . 12 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝐺𝑧) = (0g𝑌) → 𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
101100imim2d 57 . . . . . . . . . . 11 ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
102101ralimdva 3161 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) → (∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
103102reximdva 3162 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺𝑧) = (0g𝑌)) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
10465, 103syld 47 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐺 finSupp (0g𝑌) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴))))
10557, 104mpd 15 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → ∃𝑤 ∈ ℕ0𝑧 ∈ ℕ0 (𝑤 < 𝑧𝑧 / 𝑛((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) = (0g𝐴)))
10654, 55, 105mptnn0fsupp 13790 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) finSupp (0g𝐴))
1077, 8, 15, 17, 53, 106gsumcl 19584 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) ∈ 𝐵)
10833, 9, 7, 44m2cpminvid 21974 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) ∈ 𝐵) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
1093, 6, 107, 108syl3anc 1370 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
11039, 40pmatring 21913 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
1112, 5, 110syl2anc 584 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Ring)
112 ringmnd 19861 . . . . . . . . 9 (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
113111, 112syl 17 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑌 ∈ Mnd)
114113ad2antrr 723 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑌 ∈ Mnd)
115 chcoeffeq.w . . . . . . . . . 10 𝑊 = (Base‘𝑌)
11644, 9, 7, 39, 40, 115mat2pmatghm 21951 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
1173, 6, 116syl2anc 584 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
118 ghmmhm 18913 . . . . . . . 8 (𝑇 ∈ (𝐴 GrpHom 𝑌) → 𝑇 ∈ (𝐴 MndHom 𝑌))
119117, 118syl 17 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → 𝑇 ∈ (𝐴 MndHom 𝑌))
12020ad3antrrr 727 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
1214, 34sylan2 593 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
1221213adant3 1131 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
123122ad3antrrr 727 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
124123, 48ffvelcdmd 7001 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺𝑛)) ∈ 𝐵)
125120, 31, 124, 51syl3anc 1370 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))) ∈ 𝐵)
1267, 8, 15, 114, 17, 119, 125, 106gsummptmhm 19609 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))))
12744, 9, 7, 39, 40, 115mat2pmatrhm 21955 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 RingHom 𝑌))
1281273adant3 1131 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑇 ∈ (𝐴 RingHom 𝑌))
129128ad3antrrr 727 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ (𝐴 RingHom 𝑌))
1307, 50, 41rhmmul 20039 . . . . . . . . . 10 ((𝑇 ∈ (𝐴 RingHom 𝑌) ∧ (𝑛 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺𝑛)) ∈ 𝐵) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))))
131129, 31, 124, 130syl3anc 1370 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))))
13244, 9, 7, 39, 40, 115mat2pmatmhm 21954 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
1331323adant3 1131 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
134133ad3antrrr 727 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
135 cayhamlem.e2 . . . . . . . . . . . 12 𝐸 = (.g‘(mulGrp‘𝑌))
13628, 29, 135mhmmulg 18813 . . . . . . . . . . 11 ((𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)) ∧ 𝑛 ∈ ℕ0𝑀𝐵) → (𝑇‘(𝑛 𝑀)) = (𝑛𝐸(𝑇𝑀)))
137134, 25, 27, 136syl3anc 1370 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑛 𝑀)) = (𝑛𝐸(𝑇𝑀)))
1382ad3antrrr 727 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin)
1395ad3antrrr 727 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring)
14032, 33, 44m2cpminvid2 21976 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐺𝑛) ∈ (𝑁 ConstPolyMat 𝑅)) → (𝑇‘(𝑈‘(𝐺𝑛))) = (𝐺𝑛))
141138, 139, 48, 140syl3anc 1370 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑈‘(𝐺𝑛))) = (𝐺𝑛))
142137, 141oveq12d 7333 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑇‘(𝑛 𝑀)) × (𝑇‘(𝑈‘(𝐺𝑛)))) = ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))
143131, 142eqtrd 2777 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))) = ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))
144143mpteq2dva 5187 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))
145144oveq2d 7331 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))))
146126, 145eqtr3d 2779 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛)))))
147146fveq2d 6815 . . . 4 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
148109, 147eqtr3d 2779 . . 3 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
1491, 148sylan9eqr 2799 . 2 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵m (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 22108 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 𝑀)(.r𝐴)(𝑈‘(𝐺𝑛))))))
155149, 154reximddv2 3203 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1𝐾)‘𝑛) (𝑛 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇𝑀)) × (𝐺𝑛))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wral 3062  wrex 3071  Vcvv 3441  csb 3842  ifcif 4471   class class class wbr 5087  cmpt 5170  wf 6461  cfv 6465  (class class class)co 7315  m cmap 8663  Fincfn 8781   finSupp cfsupp 9198  0cc0 10944  1c1 10945   + caddc 10947   < clt 11082  cmin 11278  cn 12046  0cn0 12306  ...cfz 13312  Basecbs 16982  .rcmulr 17033   ·𝑠 cvsca 17036  0gc0g 17220   Σg cgsu 17221  Mndcmnd 18455   MndHom cmhm 18498  -gcsg 18648  .gcmg 18769   GrpHom cghm 18900  CMndccmn 19454  mulGrpcmgp 19788  1rcur 19805  Ringcrg 19851  CRingccrg 19852   RingHom crh 20024  Poly1cpl1 21420  coe1cco1 21421   Mat cmat 21626   ConstPolyMat ccpmat 21924   matToPolyMat cmat2pmat 21925   cPolyMatToMat ccpmat2mat 21926   CharPlyMat cchpmat 22047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-addf 11023  ax-mulf 11024
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-xor 1509  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-ot 4580  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-ofr 7574  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-tpos 8089  df-cur 8130  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-2o 8345  df-er 8546  df-map 8665  df-pm 8666  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-sup 9271  df-oi 9339  df-card 9768  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-xnn0 12379  df-z 12393  df-dec 12511  df-uz 12656  df-rp 12804  df-fz 13313  df-fzo 13456  df-seq 13795  df-exp 13856  df-hash 14118  df-word 14290  df-lsw 14338  df-concat 14346  df-s1 14373  df-substr 14426  df-pfx 14456  df-splice 14535  df-reverse 14544  df-s2 14633  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-0g 17222  df-gsum 17223  df-prds 17228  df-pws 17230  df-mre 17365  df-mrc 17366  df-acs 17368  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-mhm 18500  df-submnd 18501  df-efmnd 18577  df-grp 18649  df-minusg 18650  df-sbg 18651  df-mulg 18770  df-subg 18821  df-ghm 18901  df-gim 18944  df-cntz 18992  df-oppg 19019  df-symg 19044  df-pmtr 19119  df-psgn 19168  df-evpm 19169  df-cmn 19456  df-abl 19457  df-mgp 19789  df-ur 19806  df-srg 19810  df-ring 19853  df-cring 19854  df-oppr 19930  df-dvdsr 19951  df-unit 19952  df-invr 19982  df-dvr 19993  df-rnghom 20027  df-drng 20065  df-subrg 20094  df-lmod 20197  df-lss 20266  df-sra 20506  df-rgmod 20507  df-cnfld 20670  df-zring 20743  df-zrh 20777  df-dsmm 21011  df-frlm 21026  df-assa 21132  df-ascl 21134  df-psr 21184  df-mvr 21185  df-mpl 21186  df-opsr 21188  df-psr1 21423  df-vr1 21424  df-ply1 21425  df-coe1 21426  df-mamu 21605  df-mat 21627  df-mdet 21806  df-madu 21855  df-cpmat 21927  df-mat2pmat 21928  df-cpmat2mat 21929  df-decpmat 21984  df-pm2mp 22014  df-chpmat 22048
This theorem is referenced by:  cayleyhamilton0  22110  cayleyhamiltonALT  22112
  Copyright terms: Public domain W3C validator