Metamath Proof Explorer

Theorem mulgnn0di

Description: Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgdi.b 
|- B = ( Base ` G )
mulgdi.m 
|- .x. = ( .g ` G )
mulgdi.p 
|- .+ = ( +g ` G )
Assertion mulgnn0di 
|- ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 mulgdi.b 
 |-  B = ( Base ` G )
2 mulgdi.m 
 |-  .x. = ( .g ` G )
3 mulgdi.p 
 |-  .+ = ( +g ` G )
4 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
5 4 ad2antrr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> G e. Mnd )
6 1 3 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
7 6 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
8 5 7 sylan 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
9 1 3 cmncom 
 |-  ( ( G e. CMnd /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )
10 9 3expb 
 |-  ( ( G e. CMnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) = ( y .+ x ) )
11 10 ad4ant14 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) = ( y .+ x ) )
12 1 3 mndass 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
13 5 12 sylan 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
14 simpr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> M e. NN )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 eleqtrdi 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> M e. ( ZZ>= ` 1 ) )
17 simplr2 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> X e. B )
18 elfznn 
 |-  ( k e. ( 1 ... M ) -> k e. NN )
19 fvconst2g 
 |-  ( ( X e. B /\ k e. NN ) -> ( ( NN X. { X } ) ` k ) = X )
20 17 18 19 syl2an 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { X } ) ` k ) = X )
21 17 adantr 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> X e. B )
22 20 21 eqeltrd 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { X } ) ` k ) e. B )
23 simplr3 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> Y e. B )
24 fvconst2g 
 |-  ( ( Y e. B /\ k e. NN ) -> ( ( NN X. { Y } ) ` k ) = Y )
25 23 18 24 syl2an 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { Y } ) ` k ) = Y )
26 23 adantr 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> Y e. B )
27 25 26 eqeltrd 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { Y } ) ` k ) e. B )
28 1 3 mndcl 
 |-  ( ( G e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
29 5 17 23 28 syl3anc 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( X .+ Y ) e. B )
30 fvconst2g 
 |-  ( ( ( X .+ Y ) e. B /\ k e. NN ) -> ( ( NN X. { ( X .+ Y ) } ) ` k ) = ( X .+ Y ) )
31 29 18 30 syl2an 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { ( X .+ Y ) } ) ` k ) = ( X .+ Y ) )
32 20 25 oveq12d 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( ( NN X. { X } ) ` k ) .+ ( ( NN X. { Y } ) ` k ) ) = ( X .+ Y ) )
33 31 32 eqtr4d 
 |-  ( ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) /\ k e. ( 1 ... M ) ) -> ( ( NN X. { ( X .+ Y ) } ) ` k ) = ( ( ( NN X. { X } ) ` k ) .+ ( ( NN X. { Y } ) ` k ) ) )
34 8 11 13 16 22 27 33 seqcaopr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( seq 1 ( .+ , ( NN X. { ( X .+ Y ) } ) ) ` M ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq 1 ( .+ , ( NN X. { Y } ) ) ` M ) ) )
35 eqid 
 |-  seq 1 ( .+ , ( NN X. { ( X .+ Y ) } ) ) = seq 1 ( .+ , ( NN X. { ( X .+ Y ) } ) )
36 1 3 2 35 mulgnn 
 |-  ( ( M e. NN /\ ( X .+ Y ) e. B ) -> ( M .x. ( X .+ Y ) ) = ( seq 1 ( .+ , ( NN X. { ( X .+ Y ) } ) ) ` M ) )
37 14 29 36 syl2anc 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( M .x. ( X .+ Y ) ) = ( seq 1 ( .+ , ( NN X. { ( X .+ Y ) } ) ) ` M ) )
38 eqid 
 |-  seq 1 ( .+ , ( NN X. { X } ) ) = seq 1 ( .+ , ( NN X. { X } ) )
39 1 3 2 38 mulgnn 
 |-  ( ( M e. NN /\ X e. B ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) )
40 14 17 39 syl2anc 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) )
41 eqid 
 |-  seq 1 ( .+ , ( NN X. { Y } ) ) = seq 1 ( .+ , ( NN X. { Y } ) )
42 1 3 2 41 mulgnn 
 |-  ( ( M e. NN /\ Y e. B ) -> ( M .x. Y ) = ( seq 1 ( .+ , ( NN X. { Y } ) ) ` M ) )
43 14 23 42 syl2anc 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( M .x. Y ) = ( seq 1 ( .+ , ( NN X. { Y } ) ) ` M ) )
44 40 43 oveq12d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( ( M .x. X ) .+ ( M .x. Y ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq 1 ( .+ , ( NN X. { Y } ) ) ` M ) ) )
45 34 37 44 3eqtr4d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M e. NN ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
46 4 ad2antrr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> G e. Mnd )
47 simplr2 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> X e. B )
48 simplr3 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> Y e. B )
49 46 47 48 28 syl3anc 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( X .+ Y ) e. B )
50 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
51 1 50 2 mulg0 
 |-  ( ( X .+ Y ) e. B -> ( 0 .x. ( X .+ Y ) ) = ( 0g ` G ) )
52 49 51 syl 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( 0 .x. ( X .+ Y ) ) = ( 0g ` G ) )
53 eqid 
 |-  ( Base ` G ) = ( Base ` G )
54 53 50 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. ( Base ` G ) )
55 53 3 50 mndlid 
 |-  ( ( G e. Mnd /\ ( 0g ` G ) e. ( Base ` G ) ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
56 4 54 55 syl2anc2 
 |-  ( G e. CMnd -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
57 56 ad2antrr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
58 52 57 eqtr4d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( 0 .x. ( X .+ Y ) ) = ( ( 0g ` G ) .+ ( 0g ` G ) ) )
59 simpr 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> M = 0 )
60 59 oveq1d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. ( X .+ Y ) ) = ( 0 .x. ( X .+ Y ) ) )
61 59 oveq1d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0 .x. X ) )
62 1 50 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
63 47 62 syl 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
64 61 63 eqtrd 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0g ` G ) )
65 59 oveq1d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. Y ) = ( 0 .x. Y ) )
66 1 50 2 mulg0 
 |-  ( Y e. B -> ( 0 .x. Y ) = ( 0g ` G ) )
67 48 66 syl 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( 0 .x. Y ) = ( 0g ` G ) )
68 65 67 eqtrd 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. Y ) = ( 0g ` G ) )
69 64 68 oveq12d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( ( M .x. X ) .+ ( M .x. Y ) ) = ( ( 0g ` G ) .+ ( 0g ` G ) ) )
70 58 60 69 3eqtr4d 
 |-  ( ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) /\ M = 0 ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
71 simpr1 
 |-  ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> M e. NN0 )
72 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
73 71 72 sylib 
 |-  ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( M e. NN \/ M = 0 ) )
74 45 70 73 mpjaodan 
 |-  ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )