# Metamath Proof Explorer

## Theorem cnfldmulg

Description: The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Assertion cnfldmulg
`|- ( ( A e. ZZ /\ B e. CC ) -> ( A ( .g ` CCfld ) B ) = ( A x. B ) )`

### Proof

Step Hyp Ref Expression
1 oveq1
` |-  ( x = 0 -> ( x ( .g ` CCfld ) B ) = ( 0 ( .g ` CCfld ) B ) )`
2 oveq1
` |-  ( x = 0 -> ( x x. B ) = ( 0 x. B ) )`
3 1 2 eqeq12d
` |-  ( x = 0 -> ( ( x ( .g ` CCfld ) B ) = ( x x. B ) <-> ( 0 ( .g ` CCfld ) B ) = ( 0 x. B ) ) )`
4 oveq1
` |-  ( x = y -> ( x ( .g ` CCfld ) B ) = ( y ( .g ` CCfld ) B ) )`
5 oveq1
` |-  ( x = y -> ( x x. B ) = ( y x. B ) )`
6 4 5 eqeq12d
` |-  ( x = y -> ( ( x ( .g ` CCfld ) B ) = ( x x. B ) <-> ( y ( .g ` CCfld ) B ) = ( y x. B ) ) )`
7 oveq1
` |-  ( x = ( y + 1 ) -> ( x ( .g ` CCfld ) B ) = ( ( y + 1 ) ( .g ` CCfld ) B ) )`
8 oveq1
` |-  ( x = ( y + 1 ) -> ( x x. B ) = ( ( y + 1 ) x. B ) )`
9 7 8 eqeq12d
` |-  ( x = ( y + 1 ) -> ( ( x ( .g ` CCfld ) B ) = ( x x. B ) <-> ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y + 1 ) x. B ) ) )`
10 oveq1
` |-  ( x = -u y -> ( x ( .g ` CCfld ) B ) = ( -u y ( .g ` CCfld ) B ) )`
11 oveq1
` |-  ( x = -u y -> ( x x. B ) = ( -u y x. B ) )`
12 10 11 eqeq12d
` |-  ( x = -u y -> ( ( x ( .g ` CCfld ) B ) = ( x x. B ) <-> ( -u y ( .g ` CCfld ) B ) = ( -u y x. B ) ) )`
13 oveq1
` |-  ( x = A -> ( x ( .g ` CCfld ) B ) = ( A ( .g ` CCfld ) B ) )`
14 oveq1
` |-  ( x = A -> ( x x. B ) = ( A x. B ) )`
15 13 14 eqeq12d
` |-  ( x = A -> ( ( x ( .g ` CCfld ) B ) = ( x x. B ) <-> ( A ( .g ` CCfld ) B ) = ( A x. B ) ) )`
16 cnfldbas
` |-  CC = ( Base ` CCfld )`
17 cnfld0
` |-  0 = ( 0g ` CCfld )`
18 eqid
` |-  ( .g ` CCfld ) = ( .g ` CCfld )`
19 16 17 18 mulg0
` |-  ( B e. CC -> ( 0 ( .g ` CCfld ) B ) = 0 )`
20 mul02
` |-  ( B e. CC -> ( 0 x. B ) = 0 )`
21 19 20 eqtr4d
` |-  ( B e. CC -> ( 0 ( .g ` CCfld ) B ) = ( 0 x. B ) )`
22 oveq1
` |-  ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( ( y ( .g ` CCfld ) B ) + B ) = ( ( y x. B ) + B ) )`
23 cnring
` |-  CCfld e. Ring`
24 ringmnd
` |-  ( CCfld e. Ring -> CCfld e. Mnd )`
25 23 24 ax-mp
` |-  CCfld e. Mnd`
` |-  + = ( +g ` CCfld )`
27 16 18 26 mulgnn0p1
` |-  ( ( CCfld e. Mnd /\ y e. NN0 /\ B e. CC ) -> ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y ( .g ` CCfld ) B ) + B ) )`
28 25 27 mp3an1
` |-  ( ( y e. NN0 /\ B e. CC ) -> ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y ( .g ` CCfld ) B ) + B ) )`
29 nn0cn
` |-  ( y e. NN0 -> y e. CC )`
` |-  ( ( y e. NN0 /\ B e. CC ) -> y e. CC )`
31 simpr
` |-  ( ( y e. NN0 /\ B e. CC ) -> B e. CC )`
` |-  ( ( y e. NN0 /\ B e. CC ) -> ( ( y + 1 ) x. B ) = ( ( y x. B ) + B ) )`
33 28 32 eqeq12d
` |-  ( ( y e. NN0 /\ B e. CC ) -> ( ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y + 1 ) x. B ) <-> ( ( y ( .g ` CCfld ) B ) + B ) = ( ( y x. B ) + B ) ) )`
34 22 33 syl5ibr
` |-  ( ( y e. NN0 /\ B e. CC ) -> ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y + 1 ) x. B ) ) )`
35 34 expcom
` |-  ( B e. CC -> ( y e. NN0 -> ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( ( y + 1 ) ( .g ` CCfld ) B ) = ( ( y + 1 ) x. B ) ) ) )`
36 fveq2
` |-  ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( ( invg ` CCfld ) ` ( y ( .g ` CCfld ) B ) ) = ( ( invg ` CCfld ) ` ( y x. B ) ) )`
37 eqid
` |-  ( invg ` CCfld ) = ( invg ` CCfld )`
38 16 18 37 mulgnegnn
` |-  ( ( y e. NN /\ B e. CC ) -> ( -u y ( .g ` CCfld ) B ) = ( ( invg ` CCfld ) ` ( y ( .g ` CCfld ) B ) ) )`
39 nncn
` |-  ( y e. NN -> y e. CC )`
40 mulneg1
` |-  ( ( y e. CC /\ B e. CC ) -> ( -u y x. B ) = -u ( y x. B ) )`
41 39 40 sylan
` |-  ( ( y e. NN /\ B e. CC ) -> ( -u y x. B ) = -u ( y x. B ) )`
42 mulcl
` |-  ( ( y e. CC /\ B e. CC ) -> ( y x. B ) e. CC )`
43 39 42 sylan
` |-  ( ( y e. NN /\ B e. CC ) -> ( y x. B ) e. CC )`
44 cnfldneg
` |-  ( ( y x. B ) e. CC -> ( ( invg ` CCfld ) ` ( y x. B ) ) = -u ( y x. B ) )`
45 43 44 syl
` |-  ( ( y e. NN /\ B e. CC ) -> ( ( invg ` CCfld ) ` ( y x. B ) ) = -u ( y x. B ) )`
46 41 45 eqtr4d
` |-  ( ( y e. NN /\ B e. CC ) -> ( -u y x. B ) = ( ( invg ` CCfld ) ` ( y x. B ) ) )`
47 38 46 eqeq12d
` |-  ( ( y e. NN /\ B e. CC ) -> ( ( -u y ( .g ` CCfld ) B ) = ( -u y x. B ) <-> ( ( invg ` CCfld ) ` ( y ( .g ` CCfld ) B ) ) = ( ( invg ` CCfld ) ` ( y x. B ) ) ) )`
48 36 47 syl5ibr
` |-  ( ( y e. NN /\ B e. CC ) -> ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( -u y ( .g ` CCfld ) B ) = ( -u y x. B ) ) )`
49 48 expcom
` |-  ( B e. CC -> ( y e. NN -> ( ( y ( .g ` CCfld ) B ) = ( y x. B ) -> ( -u y ( .g ` CCfld ) B ) = ( -u y x. B ) ) ) )`
50 3 6 9 12 15 21 35 49 zindd
` |-  ( B e. CC -> ( A e. ZZ -> ( A ( .g ` CCfld ) B ) = ( A x. B ) ) )`
51 50 impcom
` |-  ( ( A e. ZZ /\ B e. CC ) -> ( A ( .g ` CCfld ) B ) = ( A x. B ) )`