Metamath Proof Explorer

Theorem clmmulg

Description: The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses clmmulg.1 
|- V = ( Base ` W )
clmmulg.2 
|- .xb = ( .g ` W )
clmmulg.3 
|- .x. = ( .s ` W )
Assertion clmmulg 
|- ( ( W e. CMod /\ A e. ZZ /\ B e. V ) -> ( A .xb B ) = ( A .x. B ) )

Proof

Step Hyp Ref Expression
1 clmmulg.1 
 |-  V = ( Base ` W )
2 clmmulg.2 
 |-  .xb = ( .g ` W )
3 clmmulg.3 
 |-  .x. = ( .s ` W )
4 oveq1 
 |-  ( x = 0 -> ( x .xb B ) = ( 0 .xb B ) )
5 oveq1 
 |-  ( x = 0 -> ( x .x. B ) = ( 0 .x. B ) )
6 4 5 eqeq12d 
 |-  ( x = 0 -> ( ( x .xb B ) = ( x .x. B ) <-> ( 0 .xb B ) = ( 0 .x. B ) ) )
7 oveq1 
 |-  ( x = y -> ( x .xb B ) = ( y .xb B ) )
8 oveq1 
 |-  ( x = y -> ( x .x. B ) = ( y .x. B ) )
9 7 8 eqeq12d 
 |-  ( x = y -> ( ( x .xb B ) = ( x .x. B ) <-> ( y .xb B ) = ( y .x. B ) ) )
10 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .xb B ) = ( ( y + 1 ) .xb B ) )
11 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .x. B ) = ( ( y + 1 ) .x. B ) )
12 10 11 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .xb B ) = ( x .x. B ) <-> ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) ) )
13 oveq1 
 |-  ( x = -u y -> ( x .xb B ) = ( -u y .xb B ) )
14 oveq1 
 |-  ( x = -u y -> ( x .x. B ) = ( -u y .x. B ) )
15 13 14 eqeq12d 
 |-  ( x = -u y -> ( ( x .xb B ) = ( x .x. B ) <-> ( -u y .xb B ) = ( -u y .x. B ) ) )
16 oveq1 
 |-  ( x = A -> ( x .xb B ) = ( A .xb B ) )
17 oveq1 
 |-  ( x = A -> ( x .x. B ) = ( A .x. B ) )
18 16 17 eqeq12d 
 |-  ( x = A -> ( ( x .xb B ) = ( x .x. B ) <-> ( A .xb B ) = ( A .x. B ) ) )
19 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
20 1 19 2 mulg0 
 |-  ( B e. V -> ( 0 .xb B ) = ( 0g ` W ) )
21 20 adantl 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 0 .xb B ) = ( 0g ` W ) )
22 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
23 1 22 3 19 clm0vs 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 0 .x. B ) = ( 0g ` W ) )
24 21 23 eqtr4d 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 0 .xb B ) = ( 0 .x. B ) )
25 oveq1 
 |-  ( ( y .xb B ) = ( y .x. B ) -> ( ( y .xb B ) ( +g ` W ) B ) = ( ( y .x. B ) ( +g ` W ) B ) )
26 clmgrp 
 |-  ( W e. CMod -> W e. Grp )
27 grpmnd 
 |-  ( W e. Grp -> W e. Mnd )
28 26 27 syl 
 |-  ( W e. CMod -> W e. Mnd )
29 28 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> W e. Mnd )
30 simpr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. NN0 )
31 simplr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> B e. V )
32 eqid 
 |-  ( +g ` W ) = ( +g ` W )
33 1 2 32 mulgnn0p1 
 |-  ( ( W e. Mnd /\ y e. NN0 /\ B e. V ) -> ( ( y + 1 ) .xb B ) = ( ( y .xb B ) ( +g ` W ) B ) )
34 29 30 31 33 syl3anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .xb B ) = ( ( y .xb B ) ( +g ` W ) B ) )
35 simpll 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> W e. CMod )
36 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
37 22 36 clmzss 
 |-  ( W e. CMod -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
38 37 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
39 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
40 39 adantl 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. ZZ )
41 38 40 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. ( Base ` ( Scalar ` W ) ) )
42 1zzd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> 1 e. ZZ )
43 38 42 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> 1 e. ( Base ` ( Scalar ` W ) ) )
44 1 22 3 36 32 clmvsdir 
 |-  ( ( W e. CMod /\ ( y e. ( Base ` ( Scalar ` W ) ) /\ 1 e. ( Base ` ( Scalar ` W ) ) /\ B e. V ) ) -> ( ( y + 1 ) .x. B ) = ( ( y .x. B ) ( +g ` W ) ( 1 .x. B ) ) )
45 35 41 43 31 44 syl13anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .x. B ) = ( ( y .x. B ) ( +g ` W ) ( 1 .x. B ) ) )
46 1 3 clmvs1 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 1 .x. B ) = B )
47 46 adantr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( 1 .x. B ) = B )
48 47 oveq2d 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y .x. B ) ( +g ` W ) ( 1 .x. B ) ) = ( ( y .x. B ) ( +g ` W ) B ) )
49 45 48 eqtrd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .x. B ) = ( ( y .x. B ) ( +g ` W ) B ) )
50 34 49 eqeq12d 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) <-> ( ( y .xb B ) ( +g ` W ) B ) = ( ( y .x. B ) ( +g ` W ) B ) ) )
51 25 50 syl5ibr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y .xb B ) = ( y .x. B ) -> ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) ) )
52 51 ex 
 |-  ( ( W e. CMod /\ B e. V ) -> ( y e. NN0 -> ( ( y .xb B ) = ( y .x. B ) -> ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) ) ) )
53 fveq2 
 |-  ( ( y .xb B ) = ( y .x. B ) -> ( ( invg ` W ) ` ( y .xb B ) ) = ( ( invg ` W ) ` ( y .x. B ) ) )
54 26 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> W e. Grp )
55 nnz 
 |-  ( y e. NN -> y e. ZZ )
56 55 adantl 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> y e. ZZ )
57 simplr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> B e. V )
58 eqid 
 |-  ( invg ` W ) = ( invg ` W )
59 1 2 58 mulgneg 
 |-  ( ( W e. Grp /\ y e. ZZ /\ B e. V ) -> ( -u y .xb B ) = ( ( invg ` W ) ` ( y .xb B ) ) )
60 54 56 57 59 syl3anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( -u y .xb B ) = ( ( invg ` W ) ` ( y .xb B ) ) )
61 simpll 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> W e. CMod )
62 37 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
63 62 56 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> y e. ( Base ` ( Scalar ` W ) ) )
64 1 22 3 58 36 61 57 63 clmvsneg 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( ( invg ` W ) ` ( y .x. B ) ) = ( -u y .x. B ) )
65 64 eqcomd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( -u y .x. B ) = ( ( invg ` W ) ` ( y .x. B ) ) )
66 60 65 eqeq12d 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( ( -u y .xb B ) = ( -u y .x. B ) <-> ( ( invg ` W ) ` ( y .xb B ) ) = ( ( invg ` W ) ` ( y .x. B ) ) ) )
67 53 66 syl5ibr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( ( y .xb B ) = ( y .x. B ) -> ( -u y .xb B ) = ( -u y .x. B ) ) )
68 67 ex 
 |-  ( ( W e. CMod /\ B e. V ) -> ( y e. NN -> ( ( y .xb B ) = ( y .x. B ) -> ( -u y .xb B ) = ( -u y .x. B ) ) ) )
69 6 9 12 15 18 24 52 68 zindd 
 |-  ( ( W e. CMod /\ B e. V ) -> ( A e. ZZ -> ( A .xb B ) = ( A .x. B ) ) )
70 69 3impia 
 |-  ( ( W e. CMod /\ B e. V /\ A e. ZZ ) -> ( A .xb B ) = ( A .x. B ) )
71 70 3com23 
 |-  ( ( W e. CMod /\ A e. ZZ /\ B e. V ) -> ( A .xb B ) = ( A .x. B ) )