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 26 grpmndd 
 |-  ( W e. CMod -> W e. Mnd )
28 27 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> W e. Mnd )
29 simpr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. NN0 )
30 simplr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> B e. V )
31 eqid 
 |-  ( +g ` W ) = ( +g ` W )
32 1 2 31 mulgnn0p1 
 |-  ( ( W e. Mnd /\ y e. NN0 /\ B e. V ) -> ( ( y + 1 ) .xb B ) = ( ( y .xb B ) ( +g ` W ) B ) )
33 28 29 30 32 syl3anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .xb B ) = ( ( y .xb B ) ( +g ` W ) B ) )
34 simpll 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> W e. CMod )
35 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
36 22 35 clmzss 
 |-  ( W e. CMod -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
37 36 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
38 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
39 38 adantl 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. ZZ )
40 37 39 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> y e. ( Base ` ( Scalar ` W ) ) )
41 1zzd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> 1 e. ZZ )
42 37 41 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> 1 e. ( Base ` ( Scalar ` W ) ) )
43 1 22 3 35 31 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 ) ) )
44 34 40 42 30 43 syl13anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .x. B ) = ( ( y .x. B ) ( +g ` W ) ( 1 .x. B ) ) )
45 1 3 clmvs1 
 |-  ( ( W e. CMod /\ B e. V ) -> ( 1 .x. B ) = B )
46 45 adantr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( 1 .x. B ) = B )
47 46 oveq2d 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y .x. B ) ( +g ` W ) ( 1 .x. B ) ) = ( ( y .x. B ) ( +g ` W ) B ) )
48 44 47 eqtrd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y + 1 ) .x. B ) = ( ( y .x. B ) ( +g ` W ) B ) )
49 33 48 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 ) ) )
50 25 49 imbitrrid 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN0 ) -> ( ( y .xb B ) = ( y .x. B ) -> ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) ) )
51 50 ex 
 |-  ( ( W e. CMod /\ B e. V ) -> ( y e. NN0 -> ( ( y .xb B ) = ( y .x. B ) -> ( ( y + 1 ) .xb B ) = ( ( y + 1 ) .x. B ) ) ) )
52 fveq2 
 |-  ( ( y .xb B ) = ( y .x. B ) -> ( ( invg ` W ) ` ( y .xb B ) ) = ( ( invg ` W ) ` ( y .x. B ) ) )
53 26 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> W e. Grp )
54 nnz 
 |-  ( y e. NN -> y e. ZZ )
55 54 adantl 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> y e. ZZ )
56 simplr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> B e. V )
57 eqid 
 |-  ( invg ` W ) = ( invg ` W )
58 1 2 57 mulgneg 
 |-  ( ( W e. Grp /\ y e. ZZ /\ B e. V ) -> ( -u y .xb B ) = ( ( invg ` W ) ` ( y .xb B ) ) )
59 53 55 56 58 syl3anc 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( -u y .xb B ) = ( ( invg ` W ) ` ( y .xb B ) ) )
60 simpll 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> W e. CMod )
61 36 ad2antrr 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ZZ C_ ( Base ` ( Scalar ` W ) ) )
62 61 55 sseldd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> y e. ( Base ` ( Scalar ` W ) ) )
63 1 22 3 57 35 60 56 62 clmvsneg 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( ( invg ` W ) ` ( y .x. B ) ) = ( -u y .x. B ) )
64 63 eqcomd 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( -u y .x. B ) = ( ( invg ` W ) ` ( y .x. B ) ) )
65 59 64 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 ) ) ) )
66 52 65 imbitrrid 
 |-  ( ( ( W e. CMod /\ B e. V ) /\ y e. NN ) -> ( ( y .xb B ) = ( y .x. B ) -> ( -u y .xb B ) = ( -u y .x. B ) ) )
67 66 ex 
 |-  ( ( W e. CMod /\ B e. V ) -> ( y e. NN -> ( ( y .xb B ) = ( y .x. B ) -> ( -u y .xb B ) = ( -u y .x. B ) ) ) )
68 6 9 12 15 18 24 51 67 zindd 
 |-  ( ( W e. CMod /\ B e. V ) -> ( A e. ZZ -> ( A .xb B ) = ( A .x. B ) ) )
69 68 3impia 
 |-  ( ( W e. CMod /\ B e. V /\ A e. ZZ ) -> ( A .xb B ) = ( A .x. B ) )
70 69 3com23 
 |-  ( ( W e. CMod /\ A e. ZZ /\ B e. V ) -> ( A .xb B ) = ( A .x. B ) )