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 23145

Description: Alternate proof of cayleyhamilton 23144, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 23143 directly, but has the same structure as the proof of cayleyhamilton0 23143. In contrast to the proof of cayleyhamilton0 23143, 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 2760	. . . 4 ⊢ (Poly₁‘𝑅) = (Poly₁‘𝑅)
4		eqid 2760	. . . 4 ⊢ (𝑁 Mat (Poly₁‘𝑅)) = (𝑁 Mat (Poly₁‘𝑅))
5		eqid 2760	. . . 4 ⊢ (._r‘(𝑁 Mat (Poly₁‘𝑅))) = (._r‘(𝑁 Mat (Poly₁‘𝑅)))
6		eqid 2760	. . . 4 ⊢ (-_g‘(𝑁 Mat (Poly₁‘𝑅))) = (-_g‘(𝑁 Mat (Poly₁‘𝑅)))
7		eqid 2760	. . . 4 ⊢ (0_g‘(𝑁 Mat (Poly₁‘𝑅))) = (0_g‘(𝑁 Mat (Poly₁‘𝑅)))
8		eqid 2760	. . . 4 ⊢ (𝑁 matToPolyMat 𝑅) = (𝑁 matToPolyMat 𝑅)
9		cayleyhamilton.c	. . . 4 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
10		eqid 2760	. . . 4 ⊢ (𝐶‘𝑀) = (𝐶‘𝑀)
11		eqeq1 2764	. . . . . 6 ⊢ (𝑙 = 𝑛 → (𝑙 = 0 ↔ 𝑛 = 0))
12		eqeq1 2764	. . . . . . 7 ⊢ (𝑙 = 𝑛 → (𝑙 = (𝑠 + 1) ↔ 𝑛 = (𝑠 + 1)))
13		breq2 5107	. . . . . . . 8 ⊢ (𝑙 = 𝑛 → ((𝑠 + 1) < 𝑙 ↔ (𝑠 + 1) < 𝑛))
14		oveq1 7422	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑙 − 1) = (𝑛 − 1))
15	14	fveq2d 6884	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → (𝑏‘(𝑙 − 1)) = (𝑏‘(𝑛 − 1)))
16	15	fveq2d 6884	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑙 − 1))) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘(𝑛 − 1))))
17		fveq2 6880	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑛 → (𝑏‘𝑙) = (𝑏‘𝑛))
18	17	fveq2d 6884	. . . . . . . . . 10 ⊢ (𝑙 = 𝑛 → ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙)) = ((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛)))
19	18	oveq2d 7431	. . . . . . . . 9 ⊢ (𝑙 = 𝑛 → (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑙))) = (((𝑁 matToPolyMat 𝑅)‘𝑀)(._r‘(𝑁 Mat (Poly₁‘𝑅)))((𝑁 matToPolyMat 𝑅)‘(𝑏‘𝑛))))
20	16, 19	oveq12d 7433	. . . . . . . 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 4509	. . . . . . 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 4509	. . . . . 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 4509	. . . . 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 5209	. . . 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 2760	. . . 4 ⊢ (Base‘(𝑁 Mat (Poly₁‘𝑅))) = (Base‘(𝑁 Mat (Poly₁‘𝑅)))
26		eqid 2760	. . . 4 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
27		cayleyhamilton.m	. . . 4 ⊢ ∗ = ( ·_𝑠 ‘𝐴)
28		eqid 2760	. . . 4 ⊢ (𝑁 cPolyMatToMat 𝑅) = (𝑁 cPolyMatToMat 𝑅)
29		cayleyhamilton.e	. . . 4 ⊢ ↑ = (._g‘(mulGrp‘𝐴))
30		eqid 2760	. . . 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 23142	. . 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 2760	. . . . . . . . 9 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
33	28, 32	cpm2mfval 23003	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
34	33	eqcomd 2766	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
35	34	3adant3 1150	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
36	35	fveq1d 6882	. . . . 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 2771	. . . 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 3227	. . 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 260	. 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 2769	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
43	42	fveq1d 6882	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
44	43	oveq1d 7430	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
45	44	mpteq2dva 5198	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
46	45	oveq2d 7431	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
47	46	eqeq1d 2762	. . . . . 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 482	. . . . 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 7422	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)) = (𝑗(._g‘(mulGrp‘(𝑁 Mat (Poly₁‘𝑅))))((𝑁 matToPolyMat 𝑅)‘𝑀)))
50		fveq2 6880	. . . . . . . . . . . 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 7433	. . . . . . . . . . 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 5209	. . . . . . . . . 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 7426	. . . . . . . . 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 23120	. . . . . . . 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 2795	. . . . . . 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 6880	. . . . . . . 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 20408	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	anim2i 629	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
60	59	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
61	28, 32	cpm2mfval 23003	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 cPolyMatToMat 𝑅) = (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))))
62	61	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0))) = (𝑁 cPolyMatToMat 𝑅))
63	62	fveq1d 6882	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))))
64		eqid 2760	. . . . . . . . . . . . 13 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
65	1, 28, 3, 4, 64, 7	m2cpminv0 23015	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑁 cPolyMatToMat 𝑅)‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
66	63, 65	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
67	60, 66	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = (0_g‘𝐴))
68		cayleyhamilton.0	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝐴)
69	67, 68	eqtr4di 2813	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
70	69	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝑚 ∈ (𝑁 ConstPolyMat 𝑅) ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((coe₁‘(𝑥𝑚𝑦))‘0)))‘(0_g‘(𝑁 Mat (Poly₁‘𝑅)))) = 0 )
71	57, 70	sylan9eqr 2817	. . . . . . 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 700	. . . . . 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 486	. . . . 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 2795	. . . 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 418	. . 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 3219	. 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 16	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∃wrex 3086 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 ‘cfv 6534 (class class class)co 7415 ∈ cmpo 7417 ↑_m cmap 8830 Fincfn 8956 0cc0 11146 1c1 11147 + caddc 11149 < clt 11289 − cmin 11487 ℕcn 12279 ℕ₀cn0 12550 ...cfz 13583 Basecbs 17323 ._rcmulr 17365 ·_𝑠 cvsca 17368 0_gc0g 17546 Σ_g cgsu 17547 -_gcsg 19082 ._gcmg 19213 mulGrpcmgp 20296 1_rcur 20343 Ringcrg 20395 CRingccrg 20396 Poly₁cpl1 22431 coe₁cco1 22432 Mat cmat 22658 ConstPolyMat ccpmat 22957 matToPolyMat cmat2pmat 22958 cPolyMatToMat ccpmat2mat 22959 CharPlyMat cchpmat 23080

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7738 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-addf 11225 ax-mulf 11226

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-ot 4593 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-isom 6543 df-riota 7372 df-ov 7418 df-oprab 7419 df-mpo 7420 df-of 7680 df-ofr 7681 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8161 df-tpos 8226 df-cur 8267 df-frecs 8282 df-wrecs 8313 df-recs 8362 df-rdg 8401 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-sup 9416 df-oi 9486 df-card 9966 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11489 df-neg 11490 df-div 11918 df-nn 12280 df-2 12349 df-3 12350 df-4 12351 df-5 12352 df-6 12353 df-7 12354 df-8 12355 df-9 12356 df-n0 12551 df-xnn0 12624 df-z 12638 df-dec 12759 df-uz 12910 df-rp 13065 df-fz 13584 df-fzo 13732 df-seq 14088 df-exp 14148 df-hash 14417 df-word 14601 df-lsw 14650 df-concat 14658 df-s1 14685 df-substr 14731 df-pfx 14763 df-splice 14841 df-reverse 14850 df-s2 14941 df-struct 17261 df-sets 17278 df-slot 17296 df-ndx 17308 df-base 17324 df-ress 17345 df-plusg 17377 df-mulr 17378 df-starv 17379 df-sca 17380 df-vsca 17381 df-ip 17382 df-tset 17383 df-ple 17384 df-ds 17386 df-unif 17387 df-hom 17388 df-cco 17389 df-0g 17548 df-gsum 17549 df-prds 17554 df-pws 17556 df-mre 17692 df-mrc 17693 df-acs 17695 df-mgm 18752 df-sgrp 18844 df-mnd 18860 df-mhm 18914 df-submnd 18915 df-efmnd 19001 df-grp 19083 df-minusg 19084 df-sbg 19085 df-mulg 19214 df-subg 19269 df-ghm 19364 df-gim 19409 df-cntz 19467 df-oppg 19496 df-symg 19520 df-pmtr 19592 df-psgn 19641 df-evpm 19642 df-cmn 19932 df-abl 19933 df-mgp 20297 df-rng 20311 df-ur 20344 df-srg 20349 df-ring 20397 df-cring 20398 df-oppr 20503 df-dvdsr 20523 df-unit 20524 df-invr 20554 df-dvr 20567 df-rhm 20638 df-subrng 20734 df-subrg 20758 df-drng 20918 df-lmod 21073 df-lss 21143 df-sra 21384 df-rgmod 21385 df-cnfld 21615 df-zring 21689 df-zrh 21745 df-dsmm 21974 df-frlm 21989 df-assa 22097 df-ascl 22099 df-psr 22153 df-mvr 22154 df-mpl 22155 df-opsr 22157 df-psr1 22434 df-vr1 22435 df-ply1 22436 df-coe1 22437 df-mamu 22642 df-mat 22659 df-mdet 22836 df-madu 22885 df-cpmat 22960 df-mat2pmat 22961 df-cpmat2mat 22962 df-decpmat 23017 df-pm2mp 23047 df-chpmat 23081

This theorem is used by: (None)

W3C validator