Step |
Hyp |
Ref |
Expression |
1 |
|
matbas.a |
|- A = ( N Mat R ) |
2 |
|
matbas.g |
|- G = ( R freeLMod ( N X. N ) ) |
3 |
|
eqidd |
|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` G ) ) |
4 |
1 2
|
matbas |
|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` A ) ) |
5 |
1 2
|
matplusg |
|- ( ( N e. Fin /\ R e. V ) -> ( +g ` G ) = ( +g ` A ) ) |
6 |
5
|
oveqdr |
|- ( ( ( N e. Fin /\ R e. V ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` A ) y ) ) |
7 |
3 4 6
|
grpidpropd |
|- ( ( N e. Fin /\ R e. V ) -> ( 0g ` G ) = ( 0g ` A ) ) |