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=NMatR
chmatcl.b B=BaseA
chmatcl.p P=Poly1R
chmatcl.y Y=NMatP
chmatcl.x X=var1R
chmatcl.t T=NmatToPolyMatR
chmatcl.s -˙=-Y
chmatcl.m ·˙=Y
chmatcl.1 1˙=1Y
chmatcl.h H=X·˙1˙-˙TM
Assertion chmatcl NFinRRingMBHBaseY

Proof

Step Hyp Ref Expression
1 chmatcl.a A=NMatR
2 chmatcl.b B=BaseA
3 chmatcl.p P=Poly1R
4 chmatcl.y Y=NMatP
5 chmatcl.x X=var1R
6 chmatcl.t T=NmatToPolyMatR
7 chmatcl.s -˙=-Y
8 chmatcl.m ·˙=Y
9 chmatcl.1 1˙=1Y
10 chmatcl.h H=X·˙1˙-˙TM
11 3 4 pmatring NFinRRingYRing
12 ringgrp YRingYGrp
13 11 12 syl NFinRRingYGrp
14 13 3adant3 NFinRRingMBYGrp
15 3 ply1ring RRingPRing
16 15 anim2i NFinRRingNFinPRing
17 16 3adant3 NFinRRingMBNFinPRing
18 eqid BaseP=BaseP
19 5 3 18 vr1cl RRingXBaseP
20 19 3ad2ant2 NFinRRingMBXBaseP
21 11 3adant3 NFinRRingMBYRing
22 eqid BaseY=BaseY
23 22 9 ringidcl YRing1˙BaseY
24 21 23 syl NFinRRingMB1˙BaseY
25 18 4 22 8 matvscl NFinPRingXBaseP1˙BaseYX·˙1˙BaseY
26 17 20 24 25 syl12anc NFinRRingMBX·˙1˙BaseY
27 6 1 2 3 4 mat2pmatbas NFinRRingMBTMBaseY
28 22 7 grpsubcl YGrpX·˙1˙BaseYTMBaseYX·˙1˙-˙TMBaseY
29 14 26 27 28 syl3anc NFinRRingMBX·˙1˙-˙TMBaseY
30 10 29 eqeltrid NFinRRingMBHBaseY