chpmat0d

Description: The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019)

		Ref	Expression
	Hypothesis	chpmat0.c	⊢ 𝐶 = ( ∅ CharPlyMat 𝑅 )
	Assertion	chpmat0d	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ‘ ∅ ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpmat0.c	⊢ 𝐶 = ( ∅ CharPlyMat 𝑅 )
2		0fin	⊢ ∅ ∈ Fin
3		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
4		0ex	⊢ ∅ ∈ V
5	4	snid	⊢ ∅ ∈ { ∅ }
6		mat0dimbas0	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
7	5 6	eleqtrrid	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) )
8		eqid	⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
9		eqid	⊢ ( Base ‘ ( ∅ Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
10		eqid	⊢ ( Poly₁ ‘ 𝑅 ) = ( Poly₁ ‘ 𝑅 )
11		eqid	⊢ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) = ( ∅ Mat ( Poly₁ ‘ 𝑅 ) )
12		eqid	⊢ ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) = ( ∅ maDet ( Poly₁ ‘ 𝑅 ) )
13		eqid	⊢ ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) )
14		eqid	⊢ ( var₁ ‘ 𝑅 ) = ( var₁ ‘ 𝑅 )
15		eqid	⊢ ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) )
16		eqid	⊢ ( ∅ matToPolyMat 𝑅 ) = ( ∅ matToPolyMat 𝑅 )
17		eqid	⊢ ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) )
18	1 8 9 10 11 12 13 14 15 16 17	chpmatval	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ∧ ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ) → ( 𝐶 ‘ ∅ ) = ( ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) )
19	2 3 7 18	mp3an2i	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ‘ ∅ ) = ( ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) )
20	10	ply1ring	⊢ ( 𝑅 ∈ Ring → ( Poly₁ ‘ 𝑅 ) ∈ Ring )
21		mdet0pr	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ Ring → ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) = { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } )
22	21	fveq1d	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ Ring → ( ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) = ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) )
23	20 22	syl	⊢ ( 𝑅 ∈ Ring → ( ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) = ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) )
24	11	mat0dimid	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ Ring → ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ∅ )
25	20 24	syl	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ∅ )
26	25	oveq2d	⊢ ( 𝑅 ∈ Ring → ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) = ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) )
27		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
28	14 10 27	vr1cl	⊢ ( 𝑅 ∈ Ring → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
29	11	mat0dimscm	⊢ ( ( ( Poly₁ ‘ 𝑅 ) ∈ Ring ∧ ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) = ∅ )
30	20 28 29	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) = ∅ )
31	26 30	eqtrd	⊢ ( 𝑅 ∈ Ring → ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) = ∅ )
32		d0mat2pmat	⊢ ( 𝑅 ∈ Ring → ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) = ∅ )
33	31 32	oveq12d	⊢ ( 𝑅 ∈ Ring → ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) = ( ∅ ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) )
34	11	matring	⊢ ( ( ∅ ∈ Fin ∧ ( Poly₁ ‘ 𝑅 ) ∈ Ring ) → ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Ring )
35	2 20 34	sylancr	⊢ ( 𝑅 ∈ Ring → ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Ring )
36		ringgrp	⊢ ( ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Ring → ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Grp )
37	35 36	syl	⊢ ( 𝑅 ∈ Ring → ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Grp )
38		mat0dimbas0	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ Ring → ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = { ∅ } )
39	20 38	syl	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = { ∅ } )
40	5 39	eleqtrrid	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) )
41		eqid	⊢ ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) )
42		eqid	⊢ ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) )
43	41 42 13	grpsubid	⊢ ( ( ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ∈ Grp ∧ ∅ ∈ ( Base ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) → ( ∅ ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) = ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) )
44	37 40 43	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ∅ ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ∅ ) = ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) )
45	33 44	eqtrd	⊢ ( 𝑅 ∈ Ring → ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) = ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) )
46	45	fveq2d	⊢ ( 𝑅 ∈ Ring → ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) = ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) )
47	11	mat0dim0	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ Ring → ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ∅ )
48	20 47	syl	⊢ ( 𝑅 ∈ Ring → ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) = ∅ )
49	48	fveq2d	⊢ ( 𝑅 ∈ Ring → ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) = ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ∅ ) )
50		fvex	⊢ ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ∈ V
51	4 50	fvsn	⊢ ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ∅ ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) )
52	49 51	eqtrdi	⊢ ( 𝑅 ∈ Ring → ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( 0_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) )
53	46 52	eqtrd	⊢ ( 𝑅 ∈ Ring → ( { ⟨ ∅ , ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) ⟩ } ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) )
54	23 53	eqtrd	⊢ ( 𝑅 ∈ Ring → ( ( ∅ maDet ( Poly₁ ‘ 𝑅 ) ) ‘ ( ( ( var₁ ‘ 𝑅 ) ( ·_𝑠 ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( 1_r ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ) ( -_g ‘ ( ∅ Mat ( Poly₁ ‘ 𝑅 ) ) ) ( ( ∅ matToPolyMat 𝑅 ) ‘ ∅ ) ) ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) )
55	19 54	eqtrd	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ‘ ∅ ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) )

Metamath Proof Explorer

Theorem chpmat0d

Proof