Metamath Proof Explorer

Theorem mulgnn0ass

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

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

Proof

Step Hyp Ref Expression
1 mulgass.b 
 |-  B = ( Base ` G )
2 mulgass.t 
 |-  .x. = ( .g ` G )
3 mndsgrp 
 |-  ( G e. Mnd -> G e. Smgrp )
4 3 adantr 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp )
5 4 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> G e. Smgrp )
6 simprl 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> M e. NN )
7 simprr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> N e. NN )
8 simpr3 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> X e. B )
9 8 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> X e. B )
10 1 2 mulgnnass 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
11 5 6 7 9 10 syl13anc 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
12 11 expr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( N e. NN -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 1 13 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
15 8 14 syl 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( 0 .x. X ) = ( 0g ` G ) )
16 simpr1 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> M e. NN0 )
17 16 nn0cnd 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> M e. CC )
18 17 mul01d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M x. 0 ) = 0 )
19 18 oveq1d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M x. 0 ) .x. X ) = ( 0 .x. X ) )
20 15 oveq2d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M .x. ( 0 .x. X ) ) = ( M .x. ( 0g ` G ) ) )
21 1 2 13 mulgnn0z 
 |-  ( ( G e. Mnd /\ M e. NN0 ) -> ( M .x. ( 0g ` G ) ) = ( 0g ` G ) )
22 21 3ad2antr1 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M .x. ( 0g ` G ) ) = ( 0g ` G ) )
23 20 22 eqtrd 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M .x. ( 0 .x. X ) ) = ( 0g ` G ) )
24 15 19 23 3eqtr4d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M x. 0 ) .x. X ) = ( M .x. ( 0 .x. X ) ) )
25 24 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( ( M x. 0 ) .x. X ) = ( M .x. ( 0 .x. X ) ) )
26 oveq2 
 |-  ( N = 0 -> ( M x. N ) = ( M x. 0 ) )
27 26 oveq1d 
 |-  ( N = 0 -> ( ( M x. N ) .x. X ) = ( ( M x. 0 ) .x. X ) )
28 oveq1 
 |-  ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
29 28 oveq2d 
 |-  ( N = 0 -> ( M .x. ( N .x. X ) ) = ( M .x. ( 0 .x. X ) ) )
30 27 29 eqeq12d 
 |-  ( N = 0 -> ( ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) <-> ( ( M x. 0 ) .x. X ) = ( M .x. ( 0 .x. X ) ) ) )
31 25 30 syl5ibrcom 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( N = 0 -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
32 simpr2 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> N e. NN0 )
33 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
34 32 33 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( N e. NN \/ N = 0 ) )
35 34 adantr 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( N e. NN \/ N = 0 ) )
36 12 31 35 mpjaod 
 |-  ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
37 36 ex 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M e. NN -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
38 32 nn0cnd 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> N e. CC )
39 38 mul02d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( 0 x. N ) = 0 )
40 39 oveq1d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( 0 x. N ) .x. X ) = ( 0 .x. X ) )
41 1 2 mulgnn0cl 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> ( N .x. X ) e. B )
42 41 3adant3r1 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( N .x. X ) e. B )
43 1 13 2 mulg0 
 |-  ( ( N .x. X ) e. B -> ( 0 .x. ( N .x. X ) ) = ( 0g ` G ) )
44 42 43 syl 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( 0 .x. ( N .x. X ) ) = ( 0g ` G ) )
45 15 40 44 3eqtr4d 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( 0 x. N ) .x. X ) = ( 0 .x. ( N .x. X ) ) )
46 oveq1 
 |-  ( M = 0 -> ( M x. N ) = ( 0 x. N ) )
47 46 oveq1d 
 |-  ( M = 0 -> ( ( M x. N ) .x. X ) = ( ( 0 x. N ) .x. X ) )
48 oveq1 
 |-  ( M = 0 -> ( M .x. ( N .x. X ) ) = ( 0 .x. ( N .x. X ) ) )
49 47 48 eqeq12d 
 |-  ( M = 0 -> ( ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) <-> ( ( 0 x. N ) .x. X ) = ( 0 .x. ( N .x. X ) ) ) )
50 45 49 syl5ibrcom 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M = 0 -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
51 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
52 16 51 sylib 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( M e. NN \/ M = 0 ) )
53 37 50 52 mpjaod 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )