Step |
Hyp |
Ref |
Expression |
1 |
|
matbas.a |
|- A = ( N Mat R ) |
2 |
|
matbas.g |
|- G = ( R freeLMod ( N X. N ) ) |
3 |
|
plusgid |
|- +g = Slot ( +g ` ndx ) |
4 |
|
plusgndxnmulrndx |
|- ( +g ` ndx ) =/= ( .r ` ndx ) |
5 |
3 4
|
setsnid |
|- ( +g ` G ) = ( +g ` ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) ) |
6 |
|
eqid |
|- ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. ) |
7 |
1 2 6
|
matval |
|- ( ( N e. Fin /\ R e. V ) -> A = ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) ) |
8 |
7
|
fveq2d |
|- ( ( N e. Fin /\ R e. V ) -> ( +g ` A ) = ( +g ` ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) ) ) |
9 |
5 8
|
eqtr4id |
|- ( ( N e. Fin /\ R e. V ) -> ( +g ` G ) = ( +g ` A ) ) |