chpmat0d

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

		Ref	Expression
	Hypothesis	chpmat0.c	$⊢ C = \emptyset CharPlyMat R$
	Assertion	chpmat0d	$⊢ R \in Ring \to C (\emptyset) = 1_{{Poly}_{1} (R)}$

Proof

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

Metamath Proof Explorer

Theorem chpmat0d

Proof