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=BaseG
mulgass.t ·˙=G
Assertion mulgnn0ass GMndM0N0XB M N·˙X=M·˙N·˙X

Proof

Step Hyp Ref Expression
1 mulgass.b B=BaseG
2 mulgass.t ·˙=G
3 mndsgrp Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-
4 3 adantr Could not format ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) with typecode |-
5 4 adantr Could not format ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ ( M e. NN /\ N e. NN ) ) -> G e. Smgrp ) with typecode |-
6 simprl GMndM0N0XBMNM
7 simprr GMndM0N0XBMNN
8 simpr3 GMndM0N0XBXB
9 8 adantr GMndM0N0XBMNXB
10 1 2 mulgnnass Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) with typecode |-
11 5 6 7 9 10 syl13anc GMndM0N0XBMN M N·˙X=M·˙N·˙X
12 11 expr GMndM0N0XBMN M N·˙X=M·˙N·˙X
13 eqid 0G=0G
14 1 13 2 mulg0 XB0·˙X=0G
15 8 14 syl GMndM0N0XB0·˙X=0G
16 simpr1 GMndM0N0XBM0
17 16 nn0cnd GMndM0N0XBM
18 17 mul01d GMndM0N0XB M0=0
19 18 oveq1d GMndM0N0XB M0·˙X=0·˙X
20 15 oveq2d GMndM0N0XBM·˙0·˙X=M·˙0G
21 1 2 13 mulgnn0z GMndM0M·˙0G=0G
22 21 3ad2antr1 GMndM0N0XBM·˙0G=0G
23 20 22 eqtrd GMndM0N0XBM·˙0·˙X=0G
24 15 19 23 3eqtr4d GMndM0N0XB M0·˙X=M·˙0·˙X
25 24 adantr GMndM0N0XBM M0·˙X=M·˙0·˙X
26 oveq2 N=0 M N= M0
27 26 oveq1d N=0 M N·˙X= M0·˙X
28 oveq1 N=0N·˙X=0·˙X
29 28 oveq2d N=0M·˙N·˙X=M·˙0·˙X
30 27 29 eqeq12d N=0 M N·˙X=M·˙N·˙X M0·˙X=M·˙0·˙X
31 25 30 syl5ibrcom GMndM0N0XBMN=0 M N·˙X=M·˙N·˙X
32 simpr2 GMndM0N0XBN0
33 elnn0 N0NN=0
34 32 33 sylib GMndM0N0XBNN=0
35 34 adantr GMndM0N0XBMNN=0
36 12 31 35 mpjaod GMndM0N0XBM M N·˙X=M·˙N·˙X
37 36 ex GMndM0N0XBM M N·˙X=M·˙N·˙X
38 32 nn0cnd GMndM0N0XBN
39 38 mul02d GMndM0N0XB0 N=0
40 39 oveq1d GMndM0N0XB0 N·˙X=0·˙X
41 1 2 mulgnn0cl GMndN0XBN·˙XB
42 41 3adant3r1 GMndM0N0XBN·˙XB
43 1 13 2 mulg0 N·˙XB0·˙N·˙X=0G
44 42 43 syl GMndM0N0XB0·˙N·˙X=0G
45 15 40 44 3eqtr4d GMndM0N0XB0 N·˙X=0·˙N·˙X
46 oveq1 M=0 M N=0 N
47 46 oveq1d M=0 M N·˙X=0 N·˙X
48 oveq1 M=0M·˙N·˙X=0·˙N·˙X
49 47 48 eqeq12d M=0 M N·˙X=M·˙N·˙X0 N·˙X=0·˙N·˙X
50 45 49 syl5ibrcom GMndM0N0XBM=0 M N·˙X=M·˙N·˙X
51 elnn0 M0MM=0
52 16 51 sylib GMndM0N0XBMM=0
53 37 50 52 mpjaod GMndM0N0XB M N·˙X=M·˙N·˙X