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
26 cnfldadd 
 |-  + = ( +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 )
30 29 adantr 
 |-  ( ( y e. NN0 /\ B e. CC ) -> y e. CC )
31 simpr 
 |-  ( ( y e. NN0 /\ B e. CC ) -> B e. CC )
32 30 31 adddirp1d 
 |-  ( ( 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 imbitrrid 
 |-  ( ( 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 imbitrrid 
 |-  ( ( 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 ) )