Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  chfacfpmmulcl Structured version   Unicode version

Theorem chfacfpmmulcl 19809
 Description: Closure of the value of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.)
Hypotheses
Ref Expression
cayhamlem1.a Mat
cayhamlem1.b
cayhamlem1.p Poly1
cayhamlem1.y Mat
cayhamlem1.r
cayhamlem1.s
cayhamlem1.0
cayhamlem1.t matToPolyMat
cayhamlem1.g
cayhamlem1.e .gmulGrp
Assertion
Ref Expression
chfacfpmmulcl
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,)   (,)   (,,)   (,)   (,,)   (,,)   (,,)   (,,)   (,,)   (,)   (,,)   (,)   (,)   (,,)

Proof of Theorem chfacfpmmulcl
StepHypRef Expression
1 crngring 17719 . . . . 5
2 cayhamlem1.p . . . . . 6 Poly1
3 cayhamlem1.y . . . . . 6 Mat
42, 3pmatring 19641 . . . . 5
51, 4sylan2 476 . . . 4
8 eqid 2420 . . . . . 6 mulGrp mulGrp
98ringmgp 17714 . . . . 5 mulGrp
106, 9syl 17 . . . 4 mulGrp
11103ad2ant1 1026 . . 3 mulGrp
12 simp3 1007 . . 3
13 cayhamlem1.t . . . . . 6 matToPolyMat
14 cayhamlem1.a . . . . . 6 Mat
15 cayhamlem1.b . . . . . 6
1613, 14, 15, 2, 3mat2pmatbas 19674 . . . . 5
171, 16syl3an2 1298 . . . 4
19 eqid 2420 . . . . 5
208, 19mgpbas 17657 . . . 4 mulGrp
21 cayhamlem1.e . . . 4 .gmulGrp
2220, 21mulgnn0cl 16718 . . 3 mulGrp
2311, 12, 18, 22syl3anc 1264 . 2
24 cayhamlem1.r . . . . . 6
25 cayhamlem1.s . . . . . 6
26 cayhamlem1.0 . . . . . 6
27 cayhamlem1.g . . . . . 6
2814, 15, 2, 3, 24, 25, 26, 13, 27chfacfisf 19802 . . . . 5
291, 28syl3anl2 1313 . . . 4