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