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 mulgnn0cl 
 |-  ( ( G e. Mnd /\ M e. NN0 /\ X e. B ) -> ( M .x. X ) e. B )
18 13 15 16 17 syl3anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M .x. X ) e. B )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 1 3 19 mndrid 
 |-  ( ( G e. Mnd /\ ( M .x. X ) e. B ) -> ( ( M .x. X ) .+ ( 0g ` G ) ) = ( M .x. X ) )
21 13 18 20 syl2anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M .x. X ) .+ ( 0g ` G ) ) = ( M .x. X ) )
22 simpr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> N = 0 )
23 22 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( N .x. X ) = ( 0 .x. X ) )
24 1 19 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
25 16 24 syl 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
26 23 25 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( N .x. X ) = ( 0g ` G ) )
27 26 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 ) ) )
28 22 oveq2d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + N ) = ( M + 0 ) )
29 15 nn0cnd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> M e. CC )
30 29 addid1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + 0 ) = M )
31 28 30 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( M + N ) = M )
32 31 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ N = 0 ) -> ( ( M + N ) .x. X ) = ( M .x. X ) )
33 21 27 32 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 ) ) )
34 33 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 ) ) )
35 simpr2 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> N e. NN0 )
36 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
37 35 36 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( N e. NN \/ N = 0 ) )
38 37 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( N e. NN \/ N = 0 ) )
39 12 34 38 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 ) ) )
40 simpll 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> G e. Mnd )
41 simplr2 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> N e. NN0 )
42 simplr3 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> X e. B )
43 1 2 mulgnn0cl 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )
44 40 41 42 43 syl3anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( N .x. X ) e. B )
45 1 3 19 mndlid 
 |-  ( ( G e. Mnd /\ ( N .x. X ) e. B ) -> ( ( 0g ` G ) .+ ( N .x. X ) ) = ( N .x. X ) )
46 40 44 45 syl2anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( 0g ` G ) .+ ( N .x. X ) ) = ( N .x. X ) )
47 simpr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> M = 0 )
48 47 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0 .x. X ) )
49 42 24 syl 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
50 48 49 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M .x. X ) = ( 0g ` G ) )
51 50 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 ) ) )
52 47 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M + N ) = ( 0 + N ) )
53 41 nn0cnd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> N e. CC )
54 53 addid2d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( 0 + N ) = N )
55 52 54 eqtrd 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( M + N ) = N )
56 55 oveq1d 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M = 0 ) -> ( ( M + N ) .x. X ) = ( N .x. X ) )
57 46 51 56 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 ) ) )
58 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
59 14 58 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M e. NN \/ M = 0 ) )
60 39 57 59 mpjaodan 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )