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
|- A = ( N Mat R )
chmatcl.b
|- B = ( Base ` A )
chmatcl.p
|- P = ( Poly1 ` R )
chmatcl.y
|- Y = ( N Mat P )
chmatcl.x
|- X = ( var1 ` R )
chmatcl.t
|- T = ( N matToPolyMat R )
chmatcl.s
|- .- = ( -g ` Y )
chmatcl.m
|- .x. = ( .s ` Y )
chmatcl.1
|- .1. = ( 1r ` Y )
chmatcl.h
|- H = ( ( X .x. .1. ) .- ( T ` M ) )
Assertion chmatcl
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> H e. ( Base ` Y ) )

Proof

Step Hyp Ref Expression
1 chmatcl.a
 |-  A = ( N Mat R )
2 chmatcl.b
 |-  B = ( Base ` A )
3 chmatcl.p
 |-  P = ( Poly1 ` R )
4 chmatcl.y
 |-  Y = ( N Mat P )
5 chmatcl.x
 |-  X = ( var1 ` R )
6 chmatcl.t
 |-  T = ( N matToPolyMat R )
7 chmatcl.s
 |-  .- = ( -g ` Y )
8 chmatcl.m
 |-  .x. = ( .s ` Y )
9 chmatcl.1
 |-  .1. = ( 1r ` Y )
10 chmatcl.h
 |-  H = ( ( X .x. .1. ) .- ( T ` M ) )
11 3 4 pmatring
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
12 ringgrp
 |-  ( Y e. Ring -> Y e. Grp )
13 11 12 syl
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Grp )
14 13 3adant3
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Grp )
15 3 ply1ring
 |-  ( R e. Ring -> P e. Ring )
16 15 anim2i
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) )
17 16 3adant3
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
18 eqid
 |-  ( Base ` P ) = ( Base ` P )
19 5 3 18 vr1cl
 |-  ( R e. Ring -> X e. ( Base ` P ) )
20 19 3ad2ant2
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> X e. ( Base ` P ) )
21 11 3adant3
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Ring )
22 eqid
 |-  ( Base ` Y ) = ( Base ` Y )
23 22 9 ringidcl
 |-  ( Y e. Ring -> .1. e. ( Base ` Y ) )
24 21 23 syl
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .1. e. ( Base ` Y ) )
25 18 4 22 8 matvscl
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( X e. ( Base ` P ) /\ .1. e. ( Base ` Y ) ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
26 17 20 24 25 syl12anc
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )
27 6 1 2 3 4 mat2pmatbas
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
28 22 7 grpsubcl
 |-  ( ( Y e. Grp /\ ( X .x. .1. ) e. ( Base ` Y ) /\ ( T ` M ) e. ( Base ` Y ) ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) )
29 14 26 27 28 syl3anc
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) )
30 10 29 eqeltrid
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> H e. ( Base ` Y ) )