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 | |
|
chmatcl.b | |
||
chmatcl.p | |
||
chmatcl.y | |
||
chmatcl.x | |
||
chmatcl.t | |
||
chmatcl.s | |
||
chmatcl.m | |
||
chmatcl.1 | |
||
chmatcl.h | |
||
Assertion | chmatcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chmatcl.a | |
|
2 | chmatcl.b | |
|
3 | chmatcl.p | |
|
4 | chmatcl.y | |
|
5 | chmatcl.x | |
|
6 | chmatcl.t | |
|
7 | chmatcl.s | |
|
8 | chmatcl.m | |
|
9 | chmatcl.1 | |
|
10 | chmatcl.h | |
|
11 | 3 4 | pmatring | |
12 | ringgrp | |
|
13 | 11 12 | syl | |
14 | 13 | 3adant3 | |
15 | 3 | ply1ring | |
16 | 15 | anim2i | |
17 | 16 | 3adant3 | |
18 | eqid | |
|
19 | 5 3 18 | vr1cl | |
20 | 19 | 3ad2ant2 | |
21 | 11 | 3adant3 | |
22 | eqid | |
|
23 | 22 9 | ringidcl | |
24 | 21 23 | syl | |
25 | 18 4 22 8 | matvscl | |
26 | 17 20 24 25 | syl12anc | |
27 | 6 1 2 3 4 | mat2pmatbas | |
28 | 22 7 | grpsubcl | |
29 | 14 26 27 28 | syl3anc | |
30 | 10 29 | eqeltrid | |