This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgnn0dir

Description: Sum of group multiples, generalized to NN0 . (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b 
|- B = ( Base ` G )
mulgnndir.t 
|- .x. = ( .g ` G )
mulgnndir.p 
|- .+ = ( +g ` G )
Assertion mulgnn0dir 
|- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b 
 |-  B = ( Base ` G )
2 mulgnndir.t 
 |-  .x. = ( .g ` G )
3 mulgnndir.p 
 |-  .+ = ( +g ` G )
4 mndsgrp 
 |-  ( G e. Mnd -> G e. Smgrp )
5 4 adantr 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp )
6 5 ad2antrr 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> G e. Smgrp )
7 simplr 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> M e. NN )
8 simpr 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> N e. NN )
9 simpr3 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> X e. B )
10 9 ad2antrr 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> X e. B )
11 1 2 3 mulgnndir 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
12 6 7 8 10 11 syl13anc 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
13 simpll 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> G e. Mnd )
14 simpr1 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> M e. NN0 )
15 14 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> M e. NN0 )
16 simplr3 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> X e. B )
17 1 2 13 15 16 mulgnn0cld 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M .x. X ) e. B )
18 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
19 1 3 18 mndrid 
 |-  ( ( G e. Mnd /\ ( M .x. X ) e. B ) -> ( ( M .x. X ) .+ ( 0g ` G ) ) = ( M .x. X ) )
20 13 17 19 syl2anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M .x. X ) .+ ( 0g ` G ) ) = ( M .x. X ) )
21 simpr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> N = 0 )
22 21 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( N .x. X ) = ( 0 .x. X ) )
23 1 18 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
24 16 23 syl 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
25 22 24 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( N .x. X ) = ( 0g ` G ) )
26 25 oveq2d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M .x. X ) .+ ( N .x. X ) ) = ( ( M .x. X ) .+ ( 0g ` G ) ) )
27 21 oveq2d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + N ) = ( M + 0 ) )
28 15 nn0cnd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> M e. CC )
29 28 addridd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + 0 ) = M )
30 27 29 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + N ) = M )
31 30 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M + N ) .x. X ) = ( M .x. X ) )
32 20 26 31 3eqtr4rd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
33 32 adantlr 
 |-  ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N = 0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
34 simpr2 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> N e. NN0 )
35 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
36 34 35 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( N e. NN \/ N = 0 ) )
37 36 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( N e. NN \/ N = 0 ) )
38 12 33 37 mpjaodan 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
39 simpll 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> G e. Mnd )
40 simplr2 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> N e. NN0 )
41 simplr3 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> X e. B )
42 1 2 39 40 41 mulgnn0cld 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( N .x. X ) e. B )
43 1 3 18 mndlid 
 |-  ( ( G e. Mnd /\ ( N .x. X ) e. B ) -> ( ( 0g ` G ) .+ ( N .x. X ) ) = ( N .x. X ) )
44 39 42 43 syl2anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( 0g ` G ) .+ ( N .x. X ) ) = ( N .x. X ) )
45 simpr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> M = 0 )
46 45 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0 .x. X ) )
47 41 23 syl 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
48 46 47 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0g ` G ) )
49 48 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( M .x. X ) .+ ( N .x. X ) ) = ( ( 0g ` G ) .+ ( N .x. X ) ) )
50 45 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M + N ) = ( 0 + N ) )
51 40 nn0cnd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> N e. CC )
52 51 addlidd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( 0 + N ) = N )
53 50 52 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M + N ) = N )
54 53 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( M + N ) .x. X ) = ( N .x. X ) )
55 44 49 54 3eqtr4rd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
56 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
57 14 56 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M e. NN \/ M = 0 ) )
58 38 55 57 mpjaodan 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )