Theorem chmatcl

Description: Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019) (Proof shortened by AV, 29-Nov-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 ) − ( 𝑇 ‘ 𝑀 ) )
Assertion	chmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐻 ∈ ( Base ‘ 𝑌 ) )

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	3 4	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
12		ringgrp	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Grp )
13	11 12	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Grp )
14	13	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Grp )
15	3	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
16	15	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
17	16	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
18		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19	5 3 18	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
20	19	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21	11	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ Ring )
22		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
23	22 9	ringidcl	⊢ ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
24	21 23	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝑌 ) )
25	18 4 22 8	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
26	17 20 24 25	syl12anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
27	6 1 2 3 4	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
28	22 7	grpsubcl	⊢ ( ( 𝑌 ∈ Grp ∧ ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
29	14 26 27 28	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑌 ) )
30	10 29	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐻 ∈ ( Base ‘ 𝑌 ) )