Theorem 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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chmatcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chmatcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chmatcl.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	chmatcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chmatcl.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	chmatcl.s	⊢ − = ( -g ‘ 𝑌 )
	chmatcl.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	chmatcl.1	⊢ 1 = ( 1r ‘ 𝑌 )
	chmatcl.h	⊢ 𝐻 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
	chmatval.s	⊢ ∼ = ( -g ‘ 𝑃 )
	chmatval.0	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	chmatval	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chmatcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		chmatcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		chmatcl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		chmatcl.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		chmatcl.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
6		chmatcl.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
7		chmatcl.s	⊢ − = ( -g ‘ 𝑌 )
8		chmatcl.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
9		chmatcl.1	⊢ 1 = ( 1r ‘ 𝑌 )
10		chmatcl.h	⊢ 𝐻 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
11		chmatval.s	⊢ ∼ = ( -g ‘ 𝑃 )
12		chmatval.0	⊢ 0 = ( 0g ‘ 𝑃 )
13	10	oveqi	⊢ ( 𝐼 𝐻 𝐽 ) = ( 𝐼 ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝐽 )
14	3	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	14	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
16	15	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑃 ∈ Ring )
17	14	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
18	17	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
19		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20	5 3 19	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21	20	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
22	3 4	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
23	22	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
24		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
25	24 9	ringidcl	⊢ ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
26	23 25	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝑌 ) )
27	19 4 24 8	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
28	18 21 26 27	syl12anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
29	28	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
30	6 1 2 3 4	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
31	30	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
32		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
33	4 24 7 11	matsubgcell	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) )
34	16 29 31 32 33	syl121anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) )
35	13 34	eqtrid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) )
36	9	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 1 = ( 1r ‘ 𝑌 ) )
37	36	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 · 1 ) = ( 𝑋 · ( 1r ‘ 𝑌 ) ) )
38		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
39	14	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
40	20	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
41	38 39 40	3jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
42	41	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
43	42	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) )
44	4 19 8 12	matsc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 · ( 1r ‘ 𝑌 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
45	43 44	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 · ( 1r ‘ 𝑌 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
46	37 45	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 · 1 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 𝑋 , 0 ) ) )
47		eqeq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 = 𝑗 ↔ 𝐼 = 𝐽 ) )
48	47	ifbid	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
49	48	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝑗 , 𝑋 , 0 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
50		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
51		simpr	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
52	51	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
53	5	fvexi	⊢ 𝑋 ∈ V
54	12	fvexi	⊢ 0 ∈ V
55	53 54	ifex	⊢ if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∈ V
56	55	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∈ V )
57	46 49 50 52 56	ovmpod	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑋 , 0 ) )
58	57	oveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) = ( if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) )
59		ovif	⊢ ( if ( 𝐼 = 𝐽 , 𝑋 , 0 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) )
60	58 59	eqtrdi	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝐼 ( 𝑋 · 1 ) 𝐽 ) ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) ) )
61	35 60	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝐻 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝑋 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) , ( 0 ∼ ( 𝐼 ( 𝑇 ‘ 𝑀 ) 𝐽 ) ) ) )