cayleyhamiltonALT - Metamath Proof Explorer

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

Theorem cayleyhamiltonALT 21206

Description: Alternate proof of cayleyhamilton 21205, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 21204 directly, but has the same structure as the proof of cayleyhamilton0 21204. In contrast to the proof of cayleyhamilton0 21204, only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
cayleyhamilton.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
cayleyhamilton.b	⊢ 𝐵 = (Base‘𝐴)
cayleyhamilton.0	⊢ 0 = (0_g‘𝐴)
cayleyhamilton.c	⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
cayleyhamilton.k	⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
cayleyhamilton.m	⊢ ∗ = ( ·_𝑠 ‘𝐴)
cayleyhamilton.e	⊢ ↑ = (._g‘(mulGrp‘𝐴))

**Assertion**
Ref	Expression
cayleyhamiltonALT	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )

Distinct variable groups: 𝐴,𝑛 𝐵,𝑛 𝐶,𝑛 𝑛,𝑀 𝑛,𝑁 𝑅,𝑛 ∗ ,𝑛 ↑ ,𝑛 Allowed substitution hints: 𝐾(𝑛) 0 (𝑛)

Proof of Theorem cayleyhamiltonALT Dummy variables 𝑏 𝑚 𝑠 𝑥 𝑦 𝑙 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	. . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		cayleyhamilton.b	. . . 4 ⊢ 𝐵 = (Base‘𝐴)
3		eqid 2778	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2778	. . . 4 ⊢ (𝑁 Mat (Poly₁‘𝑅)) = (𝑁 Mat (Poly₁‘𝑅))
5		eqid 2778	. . . 4 ⊢ (._r‘(𝑁 Mat (Poly₁‘𝑅))) = (._r‘(𝑁 Mat (Poly₁‘𝑅)))
6		eqid 2778	. . . 4 ⊢ (-_g‘(𝑁 Mat (Poly₁‘𝑅))) = (-_g‘(𝑁 Mat (Poly₁‘𝑅)))
7		eqid 2778	. . . 4 ⊢ (0_g‘(𝑁 Mat (Poly₁‘𝑅))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅)))
8		eqid 2778	. . . 4 ⊢ (𝑁 matToPolyMat 𝑅) = (𝑁 matToPolyMat 𝑅)
9		cayleyhamilton.c	. . . 4 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
10		eqid 2778	. . . 4 ⊢ (𝐶‘𝑀) = (𝐶‘𝑀)
11		eqeq1 2782	. . . . . 6 ⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0))
12		eqeq1 2782	. . . . . . 7 ⊢ (𝑙 = 𝑛 → (𝑙 = (𝑠 + 1) ↔ 𝑛 = (𝑠 + 1)))
13		breq2 4934	. . . . . . . 8 ⊢ (𝑙 = 𝑛 → ((𝑠 + 1) < 𝑙 ↔ (𝑠 + 1) < 𝑛))
14		oveq1 6985	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑙 − 1) = (𝑛 − 1))
15	14	fveq2d 6505	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → (𝑏‘(𝑙 − 1)) = (𝑏‘(𝑛 − 1)))
16	15	fveq2d 6505	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1))) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1))))
17		fveq2 6501	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑏‘𝑙) = (𝑏‘𝑛))
18	17	fveq2d 6505	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛)))
19	18	oveq2d 6994	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))) = (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))
20	16, 19	oveq12d 6996	. . . . . . . 8 ⊢ (𝑙 = 𝑛 → (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)))) = (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛)))))
21	13, 20	ifbieq2d 4376	. . . . . . 7 ⊢ (𝑙 = 𝑛 → if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))) = if((𝑠 + 1) < 𝑛, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))))
22	12, 21	ifbieq2d 4376	. . . . . 6 ⊢ (𝑙 = 𝑛 → if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)))))) = if(𝑛 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛)))))))
23	11, 22	ifbieq2d 4376	. . . . 5 ⊢ (𝑙 = 𝑛 → if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))) = if(𝑛 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))))))
24	23	cbvmptv 5029	. . . 4 ⊢ (𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)))))))) = (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))))))
25		eqid 2778	. . . 4 ⊢ (Base‘(𝑁 Mat (Poly₁‘𝑅))) = (Base‘(𝑁 Mat (Poly₁‘𝑅)))
26		eqid 2778	. . . 4 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
27		cayleyhamilton.m	. . . 4 ⊢ ∗ = ( ·_𝑠 ‘𝐴)
28		eqid 2778	. . . 4 ⊢ (𝑁 cPolyMatToMat 𝑅) = (𝑁 cPolyMatToMat 𝑅)
29		cayleyhamilton.e	. . . 4 ⊢ ↑ = (._g‘(mulGrp‘𝐴))
30		eqid 2778	. . . 4 ⊢ (._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅)))) = (._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))
31	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 24, 25, 26, 27, 28, 29, 30	cayhamlem4 21203	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑁 cPolyMatToMat 𝑅)‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))))
32		eqid 2778	. . . . . . . . 9 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
33	28, 32	cpm2mfval 21064	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
34	33	eqcomd 2784	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
35	34	3adant3 1112	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
36	35	fveq1d 6503	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) = ((𝑁 cPolyMatToMat 𝑅)‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))))
37	36	eqeq2d 2788	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) ↔ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑁 cPolyMatToMat 𝑅)‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))))
38	37	2rexbidv 3245	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) ↔ ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑁 cPolyMatToMat 𝑅)‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))))
39	31, 38	mpbird 249	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))))
40		cayleyhamilton.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
41	40	eqcomi 2787	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
43	42	fveq1d 6503	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
44	43	oveq1d 6993	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
45	44	mpteq2dva 5023	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
46	45	oveq2d 6994	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
47	46	eqeq1d 2780	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) ↔ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))))
48	47	biimpa 469	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))))
49		oveq1 6985	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)) = (𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)))
50		fveq2 6501	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛) = ((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗))
51	49, 50	oveq12d 6996	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)) = ((𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗)))
52	51	cbvmptv 5029	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))) = (𝑗 ∈ ℕ₀ ↦ ((𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗)))
53	52	oveq2i 6989	. . . . . . . . 9 ⊢ ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))) = ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑗 ∈ ℕ₀ ↦ ((𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗))))
54	53	a1i 11	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))) = ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑗 ∈ ℕ₀ ↦ ((𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗)))))
55	1, 2, 3, 4, 5, 6, 7, 8, 24, 30	cayhamlem1 21181	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑗 ∈ ℕ₀ ↦ ((𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑗)))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅))))
56	54, 55	eqtrd 2814	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅))))
57		fveq2 6501	. . . . . . . 8 ⊢ (((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))))
58		crngring 19034	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	anim2i 607	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
60	59	3adant3 1112	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
61	28, 32	cpm2mfval 21064	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
62	61	eqcomd 2784	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
63	62	fveq1d 6503	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))))
64		eqid 2778	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
65	1, 28, 3, 4, 64, 7	m2cpminv0 21076	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
66	63, 65	eqtrd 2814	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
67	60, 66	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
68		cayleyhamilton.0	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝐴)
69	67, 68	syl6eqr 2832	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
70	69	adantr 473	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
71	57, 70	sylan9eqr 2836	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ ((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅)))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) = 0 )
72	56, 71	mpdan 674	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) = 0 )
73	72	adantr 473	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) = 0 )
74	48, 73	eqtrd 2814	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
75	74	ex 405	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
76	75	rexlimdvva 3239	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_𝑚 (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘((𝑁 Mat (Poly₁‘𝑅)) Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀))(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑙 ∈ ℕ₀ ↦ if(𝑙 = 0, ((0_g‘(𝑁 Mat (Poly₁‘𝑅)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘0)))), if(𝑙 = (𝑠 + 1), ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑙, (0_g‘(𝑁 Mat (Poly₁‘𝑅))), (((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1)))(-_g‘(𝑁 Mat (Poly₁‘𝑅)))(((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
77	39, 76	mpd 15	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∃wrex 3089 ifcif 4351 class class class wbr 4930 ↦ cmpt 5009 ‘cfv 6190 (class class class)co 6978 ∈ cmpo 6980 ↑_𝑚 cmap 8208 Fincfn 8308 0cc0 10337 1c1 10338 + caddc 10340 < clt 10476 − cmin 10672 ℕcn 11441 ℕ₀cn0 11710 ...cfz 12711 Basecbs 16342 ._rcmulr 16425 ·_𝑠 cvsca 16428 0_gc0g 16572 Σ_g cgsu 16573 -_gcsg 17896 ._gcmg 18014 mulGrpcmgp 18965 1_rcur 18977 Ringcrg 19023 CRingccrg 19024 Poly₁cpl1 20051 coe₁cco1 20052 Mat cmat 20723 ConstPolyMat ccpmat 21018 matToPolyMat cmat2pmat 21019 cPolyMatToMat ccpmat2mat 21020 CharPlyMat cchpmat 21141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 ax-pre-mulgt0 10414 ax-addf 10416 ax-mulf 10417

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-xor 1489 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-tp 4447 df-op 4449 df-ot 4451 df-uni 4714 df-int 4751 df-iun 4795 df-iin 4796 df-br 4931 df-opab 4993 df-mpt 5010 df-tr 5032 df-id 5313 df-eprel 5318 df-po 5327 df-so 5328 df-fr 5367 df-se 5368 df-we 5369 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-pred 5988 df-ord 6034 df-on 6035 df-lim 6036 df-suc 6037 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-isom 6199 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-of 7229 df-ofr 7230 df-om 7399 df-1st 7503 df-2nd 7504 df-supp 7636 df-tpos 7697 df-cur 7738 df-wrecs 7752 df-recs 7814 df-rdg 7852 df-1o 7907 df-2o 7908 df-oadd 7911 df-er 8091 df-map 8210 df-pm 8211 df-ixp 8262 df-en 8309 df-dom 8310 df-sdom 8311 df-fin 8312 df-fsupp 8631 df-sup 8703 df-oi 8771 df-card 9164 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-sub 10674 df-neg 10675 df-div 11101 df-nn 11442 df-2 11506 df-3 11507 df-4 11508 df-5 11509 df-6 11510 df-7 11511 df-8 11512 df-9 11513 df-n0 11711 df-xnn0 11783 df-z 11797 df-dec 11915 df-uz 12062 df-rp 12208 df-fz 12712 df-fzo 12853 df-seq 13188 df-exp 13248 df-hash 13509 df-word 13676 df-lsw 13729 df-concat 13737 df-s1 13762 df-substr 13807 df-pfx 13856 df-splice 13963 df-reverse 13981 df-s2 14075 df-struct 16344 df-ndx 16345 df-slot 16346 df-base 16348 df-sets 16349 df-ress 16350 df-plusg 16437 df-mulr 16438 df-starv 16439 df-sca 16440 df-vsca 16441 df-ip 16442 df-tset 16443 df-ple 16444 df-ds 16446 df-unif 16447 df-hom 16448 df-cco 16449 df-0g 16574 df-gsum 16575 df-prds 16580 df-pws 16582 df-mre 16718 df-mrc 16719 df-acs 16721 df-mgm 17713 df-sgrp 17755 df-mnd 17766 df-mhm 17806 df-submnd 17807 df-grp 17897 df-minusg 17898 df-sbg 17899 df-mulg 18015 df-subg 18063 df-ghm 18130 df-gim 18173 df-cntz 18221 df-oppg 18248 df-symg 18270 df-pmtr 18334 df-psgn 18383 df-evpm 18384 df-cmn 18671 df-abl 18672 df-mgp 18966 df-ur 18978 df-srg 18982 df-ring 19025 df-cring 19026 df-oppr 19099 df-dvdsr 19117 df-unit 19118 df-invr 19148 df-dvr 19159 df-rnghom 19193 df-drng 19230 df-subrg 19259 df-lmod 19361 df-lss 19429 df-sra 19669 df-rgmod 19670 df-assa 19809 df-ascl 19811 df-psr 19853 df-mvr 19854 df-mpl 19855 df-opsr 19857 df-psr1 20054 df-vr1 20055 df-ply1 20056 df-coe1 20057 df-cnfld 20251 df-zring 20323 df-zrh 20356 df-dsmm 20581 df-frlm 20596 df-mamu 20700 df-mat 20724 df-mdet 20901 df-madu 20950 df-cpmat 21021 df-mat2pmat 21022 df-cpmat2mat 21023 df-decpmat 21078 df-pm2mp 21108 df-chpmat 21142

This theorem is referenced by: (None)

W3C validator