chmatval

Description: The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019) (Proof shortened by AV, 10-Dec-2019)

	Ref	Expression
Hypotheses	chmatcl.a	$⊢ A = N Mat R$
	chmatcl.b	$⊢ B = {Base}_{A}$
	chmatcl.p	$⊢ P = {Poly}_{1} (R)$
	chmatcl.y	$⊢ Y = N Mat P$
	chmatcl.x	$⊢ X = {var}_{1} (R)$
	chmatcl.t	$⊢ T = N matToPolyMat R$
	chmatcl.s	$⊢ \underset{˙}{-} = -_{Y}$
	chmatcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	chmatcl.1	$⊢ \underset{˙}{1} = 1_{Y}$
	chmatcl.h	$⊢ H = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
	chmatval.s	$⊢ \underset{˙}{\sim} = -_{P}$
	chmatval.0	$⊢ \underset{˙}{0} = 0_{P}$
Assertion	chmatval	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I H J = if (I = J, X \underset{˙}{\sim} (I T (M) J), \underset{˙}{0} \underset{˙}{\sim} (I T (M) J))$

Proof

Step	Hyp	Ref	Expression
1		chmatcl.a	$⊢ A = N Mat R$
2		chmatcl.b	$⊢ B = {Base}_{A}$
3		chmatcl.p	$⊢ P = {Poly}_{1} (R)$
4		chmatcl.y	$⊢ Y = N Mat P$
5		chmatcl.x	$⊢ X = {var}_{1} (R)$
6		chmatcl.t	$⊢ T = N matToPolyMat R$
7		chmatcl.s	$⊢ \underset{˙}{-} = -_{Y}$
8		chmatcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		chmatcl.1	$⊢ \underset{˙}{1} = 1_{Y}$
10		chmatcl.h	$⊢ H = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)$
11		chmatval.s	$⊢ \underset{˙}{\sim} = -_{P}$
12		chmatval.0	$⊢ \underset{˙}{0} = 0_{P}$
13	10	oveqi	$⊢ I H J = I ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) J$
14	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	14	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to P \in Ring$
16	15	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to P \in Ring$
17	14	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land P \in Ring)$
18	17	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land P \in Ring)$
19		eqid	$⊢ {Base}_{P} = {Base}_{P}$
20	5 3 19	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
21	20	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \in {Base}_{P}$
22	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
23	22	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to Y \in Ring$
24		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
25	24 9	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in {Base}_{Y}$
26	23 25	syl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to \underset{˙}{1} \in {Base}_{Y}$
27	19 4 24 8	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (X \in {Base}_{P} \land \underset{˙}{1} \in {Base}_{Y})) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
28	18 21 26 27	syl12anc	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
29	28	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
30	6 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
31	30	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to T (M) \in {Base}_{Y}$
32		simpr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to (I \in N \land J \in N)$
33	4 24 7 11	matsubgcell	$⊢ (P \in Ring \land (X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y} \land T (M) \in {Base}_{Y}) \land (I \in N \land J \in N)) \to I ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) J = (I (X \underset{˙}{\cdot} \underset{˙}{1}) J) \underset{˙}{\sim} (I T (M) J)$
34	16 29 31 32 33	syl121anc	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{-} T (M)) J = (I (X \underset{˙}{\cdot} \underset{˙}{1}) J) \underset{˙}{\sim} (I T (M) J)$
35	13 34	syl5eq	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I H J = (I (X \underset{˙}{\cdot} \underset{˙}{1}) J) \underset{˙}{\sim} (I T (M) J)$
36	9	a1i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to \underset{˙}{1} = 1_{Y}$
37	36	oveq2d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to X \underset{˙}{\cdot} \underset{˙}{1} = X \underset{˙}{\cdot} 1_{Y}$
38		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
39	14	adantl	$⊢ (N \in Fin \land R \in Ring) \to P \in Ring$
40	20	adantl	$⊢ (N \in Fin \land R \in Ring) \to X \in {Base}_{P}$
41	38 39 40	3jca	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land P \in Ring \land X \in {Base}_{P})$
42	41	3adant3	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N \in Fin \land P \in Ring \land X \in {Base}_{P})$
43	42	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to (N \in Fin \land P \in Ring \land X \in {Base}_{P})$
44	4 19 8 12	matsc	$⊢ (N \in Fin \land P \in Ring \land X \in {Base}_{P}) \to X \underset{˙}{\cdot} 1_{Y} = (i \in N, j \in N ⟼ if (i = j, X, \underset{˙}{0}))$
45	43 44	syl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to X \underset{˙}{\cdot} 1_{Y} = (i \in N, j \in N ⟼ if (i = j, X, \underset{˙}{0}))$
46	37 45	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to X \underset{˙}{\cdot} \underset{˙}{1} = (i \in N, j \in N ⟼ if (i = j, X, \underset{˙}{0}))$
47		eqeq12	$⊢ (i = I \land j = J) \to (i = j \leftrightarrow I = J)$
48	47	ifbid	$⊢ (i = I \land j = J) \to if (i = j, X, \underset{˙}{0}) = if (I = J, X, \underset{˙}{0})$
49	48	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \land (i = I \land j = J)) \to if (i = j, X, \underset{˙}{0}) = if (I = J, X, \underset{˙}{0})$
50		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I \in N$
51		simpr	$⊢ (I \in N \land J \in N) \to J \in N$
52	51	adantl	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to J \in N$
53	5	fvexi	$⊢ X \in V$
54	12	fvexi	$⊢ \underset{˙}{0} \in V$
55	53 54	ifex	$⊢ if (I = J, X, \underset{˙}{0}) \in V$
56	55	a1i	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to if (I = J, X, \underset{˙}{0}) \in V$
57	46 49 50 52 56	ovmpod	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I (X \underset{˙}{\cdot} \underset{˙}{1}) J = if (I = J, X, \underset{˙}{0})$
58	57	oveq1d	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to (I (X \underset{˙}{\cdot} \underset{˙}{1}) J) \underset{˙}{\sim} (I T (M) J) = if (I = J, X, \underset{˙}{0}) \underset{˙}{\sim} (I T (M) J)$
59		ovif	$⊢ if (I = J, X, \underset{˙}{0}) \underset{˙}{\sim} (I T (M) J) = if (I = J, X \underset{˙}{\sim} (I T (M) J), \underset{˙}{0} \underset{˙}{\sim} (I T (M) J))$
60	58 59	eqtrdi	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to (I (X \underset{˙}{\cdot} \underset{˙}{1}) J) \underset{˙}{\sim} (I T (M) J) = if (I = J, X \underset{˙}{\sim} (I T (M) J), \underset{˙}{0} \underset{˙}{\sim} (I T (M) J))$
61	35 60	eqtrd	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (I \in N \land J \in N)) \to I H J = if (I = J, X \underset{˙}{\sim} (I T (M) J), \underset{˙}{0} \underset{˙}{\sim} (I T (M) J))$

Metamath Proof Explorer

Theorem chmatval

Proof