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 22774

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 22775 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 22776)! (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 2729	. . 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 22773	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
19		cayleyhamilton0.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
20	19	eqcomi 2738	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
21	20	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
22	21	fveq1d 6824	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
23	22	oveq1d 7364	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
24	23	mpteq2dva 5185	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
25	24	oveq2d 7365	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
26	25	eqeq1d 2731	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) ↔ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))))
27	26	biimpa 476	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
28		oveq1 7356	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝑛𝐸(𝑇‘𝑀)) = (𝑙𝐸(𝑇‘𝑀)))
29		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝐺‘𝑛) = (𝐺‘𝑙))
30	28, 29	oveq12d 7367	. . . . . . . . . 10 ⊢ (𝑛 = 𝑙 → ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)) = ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
31	30	cbvmptv 5196	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))) = (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
32	31	oveq2i 7360	. . . . . . . 8 ⊢ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙))))
33	1, 2, 3, 4, 5, 6, 7, 8, 11, 17	cayhamlem1 22751	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))) = 𝑍)
34	32, 33	eqtrid 2776	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍)
35		fveq2 6822	. . . . . . . 8 ⊢ ((𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍 → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = (𝑈‘𝑍))
36		crngring 20130	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
37	36	anim2i 617	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
38	37	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
39		eqid 2729	. . . . . . . . . . . 12 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
40	1, 15, 3, 4, 39, 7	m2cpminv0 22646	. . . . . . . . . . 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 2782	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈‘𝑍) = 0 )
44	43	adantr 480	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘𝑍) = 0 )
45	35, 44	sylan9eqr 2786	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
46	34, 45	mpdan 687	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
47	46	adantr 480	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
48	27, 47	eqtrd 2764	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
49	48	ex 412	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
50	49	rexlimdvva 3186	. 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 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∃wrex 3053 ifcif 4476 class class class wbr 5092 ↦ cmpt 5173 ‘cfv 6482 (class class class)co 7349 ↑_m cmap 8753 Fincfn 8872 0cc0 11009 1c1 11010 + caddc 11012 < clt 11149 − cmin 11347 ℕcn 12128 ℕ₀cn0 12384 ...cfz 13410 Basecbs 17120 ._rcmulr 17162 ·_𝑠 cvsca 17165 0_gc0g 17343 Σ_g cgsu 17344 -_gcsg 18814 ._gcmg 18946 mulGrpcmgp 20025 1_rcur 20066 Ringcrg 20118 CRingccrg 20119 Poly₁cpl1 22059 coe₁cco1 22060 Mat cmat 22292 matToPolyMat cmat2pmat 22589 cPolyMatToMat ccpmat2mat 22590 CharPlyMat cchpmat 22711

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 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-addf 11088 ax-mulf 11089

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 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-ot 4586 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-ofr 7614 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-tpos 8159 df-cur 8200 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-sup 9332 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-xnn0 12458 df-z 12472 df-dec 12592 df-uz 12736 df-rp 12894 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-hash 14238 df-word 14421 df-lsw 14470 df-concat 14478 df-s1 14503 df-substr 14548 df-pfx 14578 df-splice 14656 df-reverse 14665 df-s2 14755 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-0g 17345 df-gsum 17346 df-prds 17351 df-pws 17353 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-submnd 18658 df-efmnd 18743 df-grp 18815 df-minusg 18816 df-sbg 18817 df-mulg 18947 df-subg 19002 df-ghm 19092 df-gim 19138 df-cntz 19196 df-oppg 19225 df-symg 19249 df-pmtr 19321 df-psgn 19370 df-evpm 19371 df-cmn 19661 df-abl 19662 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 20765 df-lss 20835 df-sra 21077 df-rgmod 21078 df-cnfld 21262 df-zring 21354 df-zrh 21410 df-dsmm 21639 df-frlm 21654 df-assa 21760 df-ascl 21762 df-psr 21816 df-mvr 21817 df-mpl 21818 df-opsr 21820 df-psr1 22062 df-vr1 22063 df-ply1 22064 df-coe1 22065 df-mamu 22276 df-mat 22293 df-mdet 22470 df-madu 22519 df-cpmat 22591 df-mat2pmat 22592 df-cpmat2mat 22593 df-decpmat 22648 df-pm2mp 22678 df-chpmat 22712

This theorem is referenced by: cayleyhamilton 22775

W3C validator