Description: The scalar product of a subcomplex module matches the scalar product of the derived ZZ -module, which implies, together with zlmbas and zlmplusg , that any module over ZZ is structure-equivalent to the canonical ZZ -module ZModG . (Contributed by Mario Carneiro, 30-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | zlmclm.w | |- W = ( ZMod ` G ) |
|
| clmzlmvsca.x | |- X = ( Base ` G ) |
||
| Assertion | clmzlmvsca | |- ( ( G e. CMod /\ ( A e. ZZ /\ B e. X ) ) -> ( A ( .s ` G ) B ) = ( A ( .s ` W ) B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zlmclm.w | |- W = ( ZMod ` G ) |
|
| 2 | clmzlmvsca.x | |- X = ( Base ` G ) |
|
| 3 | eqid | |- ( .g ` G ) = ( .g ` G ) |
|
| 4 | 1 3 | zlmvsca | |- ( .g ` G ) = ( .s ` W ) |
| 5 | 4 | eqcomi | |- ( .s ` W ) = ( .g ` G ) |
| 6 | eqid | |- ( .s ` G ) = ( .s ` G ) |
|
| 7 | 2 5 6 | clmmulg | |- ( ( G e. CMod /\ A e. ZZ /\ B e. X ) -> ( A ( .s ` W ) B ) = ( A ( .s ` G ) B ) ) |
| 8 | 7 | eqcomd | |- ( ( G e. CMod /\ A e. ZZ /\ B e. X ) -> ( A ( .s ` G ) B ) = ( A ( .s ` W ) B ) ) |
| 9 | 8 | 3expb | |- ( ( G e. CMod /\ ( A e. ZZ /\ B e. X ) ) -> ( A ( .s ` G ) B ) = ( A ( .s ` W ) B ) ) |