This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zringmulg

Description: The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringmulg 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A ( .g ` ZZring ) B ) = ( A x. B ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( x e. ZZ -> x e. CC )
2 zaddcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
3 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
4 1z 
 |-  1 e. ZZ
5 1 2 3 4 cnsubglem 
 |-  ZZ e. ( SubGrp ` CCfld )
6 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
7 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
8 eqid 
 |-  ( .g ` ZZring ) = ( .g ` ZZring )
9 6 7 8 subgmulg 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ A e. ZZ /\ B e. ZZ ) -> ( A ( .g ` CCfld ) B ) = ( A ( .g ` ZZring ) B ) )
10 5 9 mp3an1 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A ( .g ` CCfld ) B ) = ( A ( .g ` ZZring ) B ) )
11 simpr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
12 11 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
13 cnfldmulg 
 |-  ( ( A e. ZZ /\ B e. CC ) -> ( A ( .g ` CCfld ) B ) = ( A x. B ) )
14 12 13 syldan 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A ( .g ` CCfld ) B ) = ( A x. B ) )
15 10 14 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A ( .g ` ZZring ) B ) = ( A x. B ) )