Step |
Hyp |
Ref |
Expression |
1 |
|
m2cpminv.a |
|- A = ( N Mat R ) |
2 |
|
m2cpminv.k |
|- K = ( Base ` A ) |
3 |
|
m2cpminv.s |
|- S = ( N ConstPolyMat R ) |
4 |
|
m2cpminv.i |
|- I = ( N cPolyMatToMat R ) |
5 |
|
m2cpminv.t |
|- T = ( N matToPolyMat R ) |
6 |
1 2 3 4
|
cpm2mf |
|- ( ( N e. Fin /\ R e. Ring ) -> I : S --> K ) |
7 |
3 5 1 2
|
m2cpmf |
|- ( ( N e. Fin /\ R e. Ring ) -> T : K --> S ) |
8 |
3 4 5
|
m2cpminvid2 |
|- ( ( N e. Fin /\ R e. Ring /\ s e. S ) -> ( T ` ( I ` s ) ) = s ) |
9 |
8
|
3expa |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ s e. S ) -> ( T ` ( I ` s ) ) = s ) |
10 |
9
|
ralrimiva |
|- ( ( N e. Fin /\ R e. Ring ) -> A. s e. S ( T ` ( I ` s ) ) = s ) |
11 |
4 1 2 5
|
m2cpminvid |
|- ( ( N e. Fin /\ R e. Ring /\ k e. K ) -> ( I ` ( T ` k ) ) = k ) |
12 |
11
|
3expa |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ k e. K ) -> ( I ` ( T ` k ) ) = k ) |
13 |
12
|
ralrimiva |
|- ( ( N e. Fin /\ R e. Ring ) -> A. k e. K ( I ` ( T ` k ) ) = k ) |
14 |
6 7 10 13
|
2fvidf1od |
|- ( ( N e. Fin /\ R e. Ring ) -> I : S -1-1-onto-> K ) |
15 |
6 7 10 13
|
2fvidinvd |
|- ( ( N e. Fin /\ R e. Ring ) -> `' I = T ) |
16 |
14 15
|
jca |
|- ( ( N e. Fin /\ R e. Ring ) -> ( I : S -1-1-onto-> K /\ `' I = T ) ) |