cayleyhamilton0 - Metamath Proof Explorer

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

Theorem cayleyhamilton0 21758

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 21759 provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT 21760)! (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.)

**Hypotheses**
Ref	Expression
cayleyhamilton0.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
cayleyhamilton0.b	⊢ 𝐵 = (Base‘𝐴)
cayleyhamilton0.0	⊢ 0 = (0_g‘𝐴)
cayleyhamilton0.1	⊢ 1 = (1_r‘𝐴)
cayleyhamilton0.m	⊢ ∗ = ( ·_𝑠 ‘𝐴)
cayleyhamilton0.e1	⊢ ↑ = (._g‘(mulGrp‘𝐴))
cayleyhamilton0.c	⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
cayleyhamilton0.k	⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
cayleyhamilton0.p	⊢ 𝑃 = (Poly₁‘𝑅)
cayleyhamilton0.y	⊢ 𝑌 = (𝑁 Mat 𝑃)
cayleyhamilton0.r	⊢ × = (._r‘𝑌)
cayleyhamilton0.s	⊢ − = (-_g‘𝑌)
cayleyhamilton0.z	⊢ 𝑍 = (0_g‘𝑌)
cayleyhamilton0.w	⊢ 𝑊 = (Base‘𝑌)
cayleyhamilton0.e2	⊢ 𝐸 = (._g‘(mulGrp‘𝑌))
cayleyhamilton0.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
cayleyhamilton0.g	⊢ 𝐺 = (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, (𝑍 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 𝑍, ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
cayleyhamilton0.u	⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)

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

Distinct variable groups: 𝐴,𝑏,𝑛,𝑠 𝐵,𝑏,𝑛,𝑠 𝐶,𝑛 𝑛,𝐸 𝑛,𝐺 𝐾,𝑏,𝑠 𝑀,𝑏,𝑛,𝑠 𝑁,𝑏,𝑛,𝑠 𝑃,𝑏,𝑛,𝑠 𝑅,𝑏,𝑛,𝑠 𝑇,𝑏,𝑛,𝑠 𝑈,𝑛 𝑛,𝑊 𝑌,𝑏,𝑛,𝑠 𝑛,𝑍 ∗ ,𝑏,𝑛,𝑠 − ,𝑏,𝑛,𝑠 0 ,𝑏,𝑠 1 ,𝑛 × ,𝑛 ↑ ,𝑏,𝑛,𝑠 Allowed substitution hints: 𝐶(𝑠,𝑏) × (𝑠,𝑏) 𝑈(𝑠,𝑏) 1 (𝑠,𝑏) 𝐸(𝑠,𝑏) 𝐺(𝑠,𝑏) 𝐾(𝑛) 𝑊(𝑠,𝑏) 0 (𝑛) 𝑍(𝑠,𝑏)

Proof of Theorem cayleyhamilton0 Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cayleyhamilton0.a	. . 3 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		cayleyhamilton0.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
3		cayleyhamilton0.p	. . 3 ⊢ 𝑃 = (Poly₁‘𝑅)
4		cayleyhamilton0.y	. . 3 ⊢ 𝑌 = (𝑁 Mat 𝑃)
5		cayleyhamilton0.r	. . 3 ⊢ × = (._r‘𝑌)
6		cayleyhamilton0.s	. . 3 ⊢ − = (-_g‘𝑌)
7		cayleyhamilton0.z	. . 3 ⊢ 𝑍 = (0_g‘𝑌)
8		cayleyhamilton0.t	. . 3 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
9		cayleyhamilton0.c	. . 3 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
10		eqid 2734	. . 3 ⊢ (𝐶‘𝑀) = (𝐶‘𝑀)
11		cayleyhamilton0.g	. . 3 ⊢ 𝐺 = (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, (𝑍 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 𝑍, ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
12		cayleyhamilton0.w	. . 3 ⊢ 𝑊 = (Base‘𝑌)
13		cayleyhamilton0.1	. . 3 ⊢ 1 = (1_r‘𝐴)
14		cayleyhamilton0.m	. . 3 ⊢ ∗ = ( ·_𝑠 ‘𝐴)
15		cayleyhamilton0.u	. . 3 ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)
16		cayleyhamilton0.e1	. . 3 ⊢ ↑ = (._g‘(mulGrp‘𝐴))
17		cayleyhamilton0.e2	. . 3 ⊢ 𝐸 = (._g‘(mulGrp‘𝑌))
18	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	cayhamlem4 21757	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
19		cayleyhamilton0.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
20	19	eqcomi 2743	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
21	20	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
22	21	fveq1d 6708	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
23	22	oveq1d 7217	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
24	23	mpteq2dva 5139	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
25	24	oveq2d 7218	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
26	25	eqeq1d 2736	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) ↔ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))))
27	26	biimpa 480	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
28		oveq1 7209	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝑛𝐸(𝑇‘𝑀)) = (𝑙𝐸(𝑇‘𝑀)))
29		fveq2 6706	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝐺‘𝑛) = (𝐺‘𝑙))
30	28, 29	oveq12d 7220	. . . . . . . . . 10 ⊢ (𝑛 = 𝑙 → ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)) = ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
31	30	cbvmptv 5147	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))) = (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
32	31	oveq2i 7213	. . . . . . . 8 ⊢ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙))))
33	1, 2, 3, 4, 5, 6, 7, 8, 11, 17	cayhamlem1 21735	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))) = 𝑍)
34	32, 33	syl5eq 2786	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍)
35		fveq2 6706	. . . . . . . 8 ⊢ ((𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍 → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = (𝑈‘𝑍))
36		crngring 19546	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
37	36	anim2i 620	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
38	37	3adant3 1134	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
39		eqid 2734	. . . . . . . . . . . 12 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
40	1, 15, 3, 4, 39, 7	m2cpminv0 21630	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘𝑍) = (0_g‘𝐴))
41	38, 40	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈‘𝑍) = (0_g‘𝐴))
42		cayleyhamilton0.0	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝐴)
43	41, 42	eqtr4di 2792	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈‘𝑍) = 0 )
44	43	adantr 484	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘𝑍) = 0 )
45	35, 44	sylan9eqr 2796	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
46	34, 45	mpdan 687	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
47	46	adantr 484	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
48	27, 47	eqtrd 2774	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
49	48	ex 416	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
50	49	rexlimdvva 3206	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
51	18, 50	mpd 15	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ∃wrex 3055 ifcif 4429 class class class wbr 5043 ↦ cmpt 5124 ‘cfv 6369 (class class class)co 7202 ↑_m cmap 8497 Fincfn 8615 0cc0 10712 1c1 10713 + caddc 10715 < clt 10850 − cmin 11045 ℕcn 11813 ℕ₀cn0 12073 ...cfz 13078 Basecbs 16684 ._rcmulr 16768 ·_𝑠 cvsca 16771 0_gc0g 16916 Σ_g cgsu 16917 -_gcsg 18339 ._gcmg 18460 mulGrpcmgp 19476 1_rcur 19488 Ringcrg 19534 CRingccrg 19535 Poly₁cpl1 21070 coe₁cco1 21071 Mat cmat 21276 matToPolyMat cmat2pmat 21573 cPolyMatToMat ccpmat2mat 21574 CharPlyMat cchpmat 21695

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-addf 10791 ax-mulf 10792

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-xor 1508 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-ot 4540 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-ofr 7459 df-om 7634 df-1st 7750 df-2nd 7751 df-supp 7893 df-tpos 7957 df-cur 7998 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-er 8380 df-map 8499 df-pm 8500 df-ixp 8568 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-fsupp 8975 df-sup 9047 df-oi 9115 df-card 9538 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-7 11881 df-8 11882 df-9 11883 df-n0 12074 df-xnn0 12146 df-z 12160 df-dec 12277 df-uz 12422 df-rp 12570 df-fz 13079 df-fzo 13222 df-seq 13558 df-exp 13619 df-hash 13880 df-word 14053 df-lsw 14101 df-concat 14109 df-s1 14136 df-substr 14189 df-pfx 14219 df-splice 14298 df-reverse 14307 df-s2 14396 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-plusg 16780 df-mulr 16781 df-starv 16782 df-sca 16783 df-vsca 16784 df-ip 16785 df-tset 16786 df-ple 16787 df-ds 16789 df-unif 16790 df-hom 16791 df-cco 16792 df-0g 16918 df-gsum 16919 df-prds 16924 df-pws 16926 df-mre 17061 df-mrc 17062 df-acs 17064 df-mgm 18086 df-sgrp 18135 df-mnd 18146 df-mhm 18190 df-submnd 18191 df-efmnd 18268 df-grp 18340 df-minusg 18341 df-sbg 18342 df-mulg 18461 df-subg 18512 df-ghm 18592 df-gim 18635 df-cntz 18683 df-oppg 18710 df-symg 18732 df-pmtr 18806 df-psgn 18855 df-evpm 18856 df-cmn 19144 df-abl 19145 df-mgp 19477 df-ur 19489 df-srg 19493 df-ring 19536 df-cring 19537 df-oppr 19613 df-dvdsr 19631 df-unit 19632 df-invr 19662 df-dvr 19673 df-rnghom 19707 df-drng 19741 df-subrg 19770 df-lmod 19873 df-lss 19941 df-sra 20181 df-rgmod 20182 df-cnfld 20336 df-zring 20408 df-zrh 20442 df-dsmm 20666 df-frlm 20681 df-assa 20787 df-ascl 20789 df-psr 20840 df-mvr 20841 df-mpl 20842 df-opsr 20844 df-psr1 21073 df-vr1 21074 df-ply1 21075 df-coe1 21076 df-mamu 21255 df-mat 21277 df-mdet 21454 df-madu 21503 df-cpmat 21575 df-mat2pmat 21576 df-cpmat2mat 21577 df-decpmat 21632 df-pm2mp 21662 df-chpmat 21696

This theorem is referenced by: cayleyhamilton 21759

W3C validator