Metamath Proof Explorer

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 ‘ 𝑌 ) )