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 22754

Description: Alternate proof of cayleyhamilton 22753, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 22752 directly, but has the same structure as the proof of cayleyhamilton0 22752. In contrast to the proof of cayleyhamilton0 22752, 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 2729	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2729	. . . 4 ⊢ (𝑁 Mat (Poly₁‘𝑅)) = (𝑁 Mat (Poly₁‘𝑅))
5		eqid 2729	. . . 4 ⊢ (._r‘(𝑁 Mat (Poly₁‘𝑅))) = (._r‘(𝑁 Mat (Poly₁‘𝑅)))
6		eqid 2729	. . . 4 ⊢ (-_g‘(𝑁 Mat (Poly₁‘𝑅))) = (-_g‘(𝑁 Mat (Poly₁‘𝑅)))
7		eqid 2729	. . . 4 ⊢ (0_g‘(𝑁 Mat (Poly₁‘𝑅))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅)))
8		eqid 2729	. . . 4 ⊢ (𝑁 matToPolyMat 𝑅) = (𝑁 matToPolyMat 𝑅)
9		cayleyhamilton.c	. . . 4 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
10		eqid 2729	. . . 4 ⊢ (𝐶‘𝑀) = (𝐶‘𝑀)
11		eqeq1 2733	. . . . . 6 ⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0))
12		eqeq1 2733	. . . . . . 7 ⊢ (𝑙 = 𝑛 → (𝑙 = (𝑠 + 1) ↔ 𝑛 = (𝑠 + 1)))
13		breq2 5106	. . . . . . . 8 ⊢ (𝑙 = 𝑛 → ((𝑠 + 1) < 𝑙 ↔ (𝑠 + 1) < 𝑛))
14		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑙 − 1) = (𝑛 − 1))
15	14	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → (𝑏‘(𝑙 − 1)) = (𝑏‘(𝑛 − 1)))
16	15	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1))) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1))))
17		fveq2 6840	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑏‘𝑙) = (𝑏‘𝑛))
18	17	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛)))
19	18	oveq2d 7385	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))) = (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))
20	16, 19	oveq12d 7387	. . . . . . . 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 4511	. . . . . . 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 4511	. . . . . 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 4511	. . . . 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 5206	. . . 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 2729	. . . 4 ⊢ (Base‘(𝑁 Mat (Poly₁‘𝑅))) = (Base‘(𝑁 Mat (Poly₁‘𝑅)))
26		eqid 2729	. . . 4 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
27		cayleyhamilton.m	. . . 4 ⊢ ∗ = ( ·_𝑠 ‘𝐴)
28		eqid 2729	. . . 4 ⊢ (𝑁 cPolyMatToMat 𝑅) = (𝑁 cPolyMatToMat 𝑅)
29		cayleyhamilton.e	. . . 4 ⊢ ↑ = (._g‘(mulGrp‘𝐴))
30		eqid 2729	. . . 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 22751	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (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 2729	. . . . . . . . 9 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
33	28, 32	cpm2mfval 22612	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
34	33	eqcomd 2735	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
35	34	3adant3 1132	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
36	35	fveq1d 6842	. . . . 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 2740	. . . 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 3200	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (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 𝑅)‘(𝑏‘𝑙))))))))‘𝑛))))) ↔ ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (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 257	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (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 2738	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
43	42	fveq1d 6842	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
44	43	oveq1d 7384	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
45	44	mpteq2dva 5195	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
46	45	oveq2d 7385	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
47	46	eqeq1d 2731	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 476	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 7376	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)) = (𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)))
50		fveq2 6840	. . . . . . . . . . . 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 7387	. . . . . . . . . . 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 5206	. . . . . . . . . 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 7380	. . . . . . . . 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 22729	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 2764	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 6840	. . . . . . . 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 20130	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	anim2i 617	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
60	59	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
61	28, 32	cpm2mfval 22612	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
62	61	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
63	62	fveq1d 6842	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))))
64		eqid 2729	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
65	1, 28, 3, 4, 64, 7	m2cpminv0 22624	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
66	63, 65	eqtrd 2764	. . . . . . . . . . 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	eqtr4di 2782	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
70	69	adantr 480	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
71	57, 70	sylan9eqr 2786	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 687	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 480	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 2764	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 412	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (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 3192	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (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 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∃wrex 3053 ifcif 4484 class class class wbr 5102 ↦ cmpt 5183 ‘cfv 6499 (class class class)co 7369 ∈ cmpo 7371 ↑_m cmap 8776 Fincfn 8895 0cc0 11044 1c1 11045 + caddc 11047 < clt 11184 − cmin 11381 ℕcn 12162 ℕ₀cn0 12418 ...cfz 13444 Basecbs 17155 ._rcmulr 17197 ·_𝑠 cvsca 17200 0_gc0g 17378 Σ_g cgsu 17379 -_gcsg 18843 ._gcmg 18975 mulGrpcmgp 20025 1_rcur 20066 Ringcrg 20118 CRingccrg 20119 Poly₁cpl1 22037 coe₁cco1 22038 Mat cmat 22270 ConstPolyMat ccpmat 22566 matToPolyMat cmat2pmat 22567 cPolyMatToMat ccpmat2mat 22568 CharPlyMat cchpmat 22689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-addf 11123 ax-mulf 11124

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1512 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-ot 4594 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-ofr 7634 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-tpos 8182 df-cur 8223 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-sup 9369 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-xnn0 12492 df-z 12506 df-dec 12626 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-word 14455 df-lsw 14504 df-concat 14512 df-s1 14537 df-substr 14582 df-pfx 14612 df-splice 14691 df-reverse 14700 df-s2 14790 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-0g 17380 df-gsum 17381 df-prds 17386 df-pws 17388 df-mre 17523 df-mrc 17524 df-acs 17526 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-mhm 18686 df-submnd 18687 df-efmnd 18772 df-grp 18844 df-minusg 18845 df-sbg 18846 df-mulg 18976 df-subg 19031 df-ghm 19121 df-gim 19167 df-cntz 19225 df-oppg 19254 df-symg 19276 df-pmtr 19348 df-psgn 19397 df-evpm 19398 df-cmn 19688 df-abl 19689 df-mgp 20026 df-rng 20038 df-ur 20067 df-srg 20072 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-dvr 20286 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-drng 20616 df-lmod 20744 df-lss 20814 df-sra 21056 df-rgmod 21057 df-cnfld 21241 df-zring 21333 df-zrh 21389 df-dsmm 21617 df-frlm 21632 df-assa 21738 df-ascl 21740 df-psr 21794 df-mvr 21795 df-mpl 21796 df-opsr 21798 df-psr1 22040 df-vr1 22041 df-ply1 22042 df-coe1 22043 df-mamu 22254 df-mat 22271 df-mdet 22448 df-madu 22497 df-cpmat 22569 df-mat2pmat 22570 df-cpmat2mat 22571 df-decpmat 22626 df-pm2mp 22656 df-chpmat 22690

This theorem is referenced by: (None)

W3C validator