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 23014

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 23015 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 23016)! (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 2769	. . 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 23013	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
19		cayleyhamilton0.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (coe₁‘(𝐶‘𝑀))
20	19	eqcomi 2778	. . . . . . . . . . . 12 ⊢ (coe₁‘(𝐶‘𝑀)) = 𝐾
21	20	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (coe₁‘(𝐶‘𝑀)) = 𝐾)
22	21	fveq1d 6884	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → ((coe₁‘(𝐶‘𝑀))‘𝑛) = (𝐾‘𝑛))
23	22	oveq1d 7426	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ 𝑛 ∈ ℕ₀) → (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)) = ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))
24	23	mpteq2dva 5208	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀))) = (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀))))
25	24	oveq2d 7427	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))))
26	25	eqeq1d 2771	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) ↔ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))))
27	26	biimpa 481	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
28		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝑛𝐸(𝑇‘𝑀)) = (𝑙𝐸(𝑇‘𝑀)))
29		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑙 → (𝐺‘𝑛) = (𝐺‘𝑙))
30	28, 29	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑛 = 𝑙 → ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)) = ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
31	30	cbvmptv 5219	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))) = (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))
32	31	oveq2i 7422	. . . . . . . 8 ⊢ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙))))
33	1, 2, 3, 4, 5, 6, 7, 8, 11, 17	cayhamlem1 22991	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑙 ∈ ℕ₀ ↦ ((𝑙𝐸(𝑇‘𝑀)) × (𝐺‘𝑙)))) = 𝑍)
34	32, 33	eqtrid 2816	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍)
35		fveq2 6882	. . . . . . . 8 ⊢ ((𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍 → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = (𝑈‘𝑍))
36		crngring 20326	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
37	36	anim2i 628	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
38	37	3adant3 1148	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
39		eqid 2769	. . . . . . . . . . . 12 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
40	1, 15, 3, 4, 39, 7	m2cpminv0 22886	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘𝑍) = (0_g‘𝐴))
41	38, 40	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈‘𝑍) = (0_g‘𝐴))
42		cayleyhamilton0.0	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝐴)
43	41, 42	eqtr4di 2822	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈‘𝑍) = 0 )
44	43	adantr 485	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘𝑍) = 0 )
45	35, 44	sylan9eqr 2826	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))) = 𝑍) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
46	34, 45	mpdan 699	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
47	46	adantr 485	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) = 0 )
48	27, 47	eqtrd 2804	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) ∧ (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )
49	48	ex 417	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑_m (0...𝑠)))) → ((𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
50	49	rexlimdvva 3228	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑_m (0...𝑠))(𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ (((coe₁‘(𝐶‘𝑀))‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ))
51	18, 50	mpd 16	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σ_g (𝑛 ∈ ℕ₀ ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ∃wrex 3095 ifcif 4492 class class class wbr 5113 ↦ cmpt 5196 ‘cfv 6537 (class class class)co 7411 ↑_m cmap 8823 Fincfn 8942 0cc0 11099 1c1 11100 + caddc 11102 < clt 11242 − cmin 11440 ℕcn 12232 ℕ₀cn0 12503 ...cfz 13534 Basecbs 17268 ._rcmulr 17310 ·_𝑠 cvsca 17313 0_gc0g 17491 Σ_g cgsu 17492 -_gcsg 19001 ._gcmg 19132 mulGrpcmgp 20215 1_rcur 20262 Ringcrg 20314 CRingccrg 20315 Poly₁cpl1 22305 coe₁cco1 22306 Mat cmat 22532 matToPolyMat cmat2pmat 22829 cPolyMatToMat ccpmat2mat 22830 CharPlyMat cchpmat 22951

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-addf 11178 ax-mulf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-xor 1539 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-ot 4603 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-ofr 7676 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-cur 8262 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-seq 14037 df-exp 14097 df-hash 14366 df-word 14550 df-lsw 14599 df-concat 14607 df-s1 14633 df-substr 14678 df-pfx 14708 df-splice 14786 df-reverse 14795 df-s2 14884 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-efmnd 18927 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-gim 19328 df-cntz 19386 df-oppg 19415 df-symg 19439 df-pmtr 19511 df-psgn 19560 df-evpm 19561 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-srg 20268 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-rhm 20553 df-subrng 20630 df-subrg 20654 df-drng 20814 df-lmod 20960 df-lss 21030 df-sra 21271 df-rgmod 21272 df-cnfld 21491 df-zring 21565 df-zrh 21621 df-dsmm 21850 df-frlm 21865 df-assa 21971 df-ascl 21973 df-psr 22027 df-mvr 22028 df-mpl 22029 df-opsr 22031 df-psr1 22308 df-vr1 22309 df-ply1 22310 df-coe1 22311 df-mamu 22516 df-mat 22533 df-mdet 22710 df-madu 22759 df-cpmat 22831 df-mat2pmat 22832 df-cpmat2mat 22833 df-decpmat 22888 df-pm2mp 22918 df-chpmat 22952

This theorem is referenced by: cayleyhamilton 23015

W3C validator