chpmatfval

Description: Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019)

	Ref	Expression
Hypotheses	chpmatfval.c	$⊢ C = N CharPlyMat R$
	chpmatfval.a	$⊢ A = N Mat R$
	chpmatfval.b	$⊢ B = {Base}_{A}$
	chpmatfval.p	$⊢ P = {Poly}_{1} (R)$
	chpmatfval.y	$⊢ Y = N Mat P$
	chpmatfval.d	$⊢ D = N maDet P$
	chpmatfval.s	$⊢ \underset{˙}{-} = -_{Y}$
	chpmatfval.x	$⊢ X = {var}_{1} (R)$
	chpmatfval.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	chpmatfval.t	$⊢ T = N matToPolyMat R$
	chpmatfval.i	$⊢ \underset{˙}{1} = 1_{Y}$
Assertion	chpmatfval	$⊢ (N \in Fin \land R \in V) \to C = (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)))$

Proof

Step	Hyp	Ref	Expression
1		chpmatfval.c	$⊢ C = N CharPlyMat R$
2		chpmatfval.a	$⊢ A = N Mat R$
3		chpmatfval.b	$⊢ B = {Base}_{A}$
4		chpmatfval.p	$⊢ P = {Poly}_{1} (R)$
5		chpmatfval.y	$⊢ Y = N Mat P$
6		chpmatfval.d	$⊢ D = N maDet P$
7		chpmatfval.s	$⊢ \underset{˙}{-} = -_{Y}$
8		chpmatfval.x	$⊢ X = {var}_{1} (R)$
9		chpmatfval.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
10		chpmatfval.t	$⊢ T = N matToPolyMat R$
11		chpmatfval.i	$⊢ \underset{˙}{1} = 1_{Y}$
12		df-chpmat	$⊢ CharPlyMat = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m))))$
13	12	a1i	$⊢ (N \in Fin \land R \in V) \to CharPlyMat = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m))))$
14		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
15	14 2	eqtr4di	$⊢ (n = N \land r = R) \to n Mat r = A$
16	15	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = {Base}_{A}$
17	16 3	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = B$
18		simpl	$⊢ (n = N \land r = R) \to n = N$
19		simpr	$⊢ (n = N \land r = R) \to r = R$
20	19	fveq2d	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = {Poly}_{1} (R)$
21	20 4	eqtr4di	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = P$
22	18 21	oveq12d	$⊢ (n = N \land r = R) \to n maDet {Poly}_{1} (r) = N maDet P$
23	22 6	eqtr4di	$⊢ (n = N \land r = R) \to n maDet {Poly}_{1} (r) = D$
24		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
25	24	adantl	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = {Poly}_{1} (R)$
26	25 4	eqtr4di	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = P$
27	18 26	oveq12d	$⊢ (n = N \land r = R) \to n Mat {Poly}_{1} (r) = N Mat P$
28	27 5	eqtr4di	$⊢ (n = N \land r = R) \to n Mat {Poly}_{1} (r) = Y$
29	28	fveq2d	$⊢ (n = N \land r = R) \to -_{(n Mat {Poly}_{1} (r))} = -_{Y}$
30	29 7	eqtr4di	$⊢ (n = N \land r = R) \to -_{(n Mat {Poly}_{1} (r))} = \underset{˙}{-}$
31	28	fveq2d	$⊢ (n = N \land r = R) \to \cdot_{(n Mat {Poly}_{1} (r))} = \cdot_{Y}$
32	31 9	eqtr4di	$⊢ (n = N \land r = R) \to \cdot_{(n Mat {Poly}_{1} (r))} = \underset{˙}{\cdot}$
33		fveq2	$⊢ r = R \to {var}_{1} (r) = {var}_{1} (R)$
34	33 8	eqtr4di	$⊢ r = R \to {var}_{1} (r) = X$
35	34	adantl	$⊢ (n = N \land r = R) \to {var}_{1} (r) = X$
36	28	fveq2d	$⊢ (n = N \land r = R) \to 1_{(n Mat {Poly}_{1} (r))} = 1_{Y}$
37	36 11	eqtr4di	$⊢ (n = N \land r = R) \to 1_{(n Mat {Poly}_{1} (r))} = \underset{˙}{1}$
38	32 35 37	oveq123d	$⊢ (n = N \land r = R) \to {var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))} = X \underset{˙}{\cdot} \underset{˙}{1}$
39		oveq12	$⊢ (n = N \land r = R) \to n matToPolyMat r = N matToPolyMat R$
40	39 10	eqtr4di	$⊢ (n = N \land r = R) \to n matToPolyMat r = T$
41	40	fveq1d	$⊢ (n = N \land r = R) \to (n matToPolyMat r) (m) = T (m)$
42	30 38 41	oveq123d	$⊢ (n = N \land r = R) \to ({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m) = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)$
43	23 42	fveq12d	$⊢ (n = N \land r = R) \to (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m)) = D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m))$
44	17 43	mpteq12dv	$⊢ (n = N \land r = R) \to (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m))) = (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)))$
45	44	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to (m \in {Base}_{(n Mat r)} ⟼ (n maDet {Poly}_{1} (r)) (({var}_{1} (r) \cdot_{(n Mat {Poly}_{1} (r))} 1_{(n Mat {Poly}_{1} (r))}) -_{(n Mat {Poly}_{1} (r))} (n matToPolyMat r) (m))) = (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)))$
46		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
47		elex	$⊢ R \in V \to R \in V$
48	47	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
49	3	fvexi	$⊢ B \in V$
50		mptexg	$⊢ B \in V \to (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m))) \in V$
51	49 50	mp1i	$⊢ (N \in Fin \land R \in V) \to (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m))) \in V$
52	13 45 46 48 51	ovmpod	$⊢ (N \in Fin \land R \in V) \to N CharPlyMat R = (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)))$
53	1 52	syl5eq	$⊢ (N \in Fin \land R \in V) \to C = (m \in B ⟼ D ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (m)))$

Metamath Proof Explorer

Theorem chpmatfval

Proof