Step |
Hyp |
Ref |
Expression |
1 |
|
asclinvg.a |
|- A = ( algSc ` W ) |
2 |
|
asclinvg.r |
|- R = ( Scalar ` W ) |
3 |
|
asclinvg.k |
|- B = ( Base ` R ) |
4 |
|
asclinvg.i |
|- I = ( invg ` R ) |
5 |
|
asclinvg.j |
|- J = ( invg ` W ) |
6 |
|
simp2 |
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> W e. Ring ) |
7 |
|
simp1 |
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> W e. LMod ) |
8 |
1 2 6 7
|
asclghm |
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> A e. ( R GrpHom W ) ) |
9 |
|
simp3 |
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> C e. B ) |
10 |
3 4 5
|
ghminv |
|- ( ( A e. ( R GrpHom W ) /\ C e. B ) -> ( A ` ( I ` C ) ) = ( J ` ( A ` C ) ) ) |
11 |
10
|
eqcomd |
|- ( ( A e. ( R GrpHom W ) /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) ) |
12 |
8 9 11
|
syl2anc |
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) ) |