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 โŠข ๐ต = ( Base โ€˜ ๐บ )
mulgass.t โŠข ยท = ( .g โ€˜ ๐บ )
Assertion mulgnn0ass ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) )

Proof

Step Hyp Ref Expression
1 mulgass.b โŠข ๐ต = ( Base โ€˜ ๐บ )
2 mulgass.t โŠข ยท = ( .g โ€˜ ๐บ )
3 mndsgrp โŠข ( ๐บ โˆˆ Mnd โ†’ ๐บ โˆˆ Smgrp )
4 3 adantr โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐บ โˆˆ Smgrp )
5 4 adantr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ๐บ โˆˆ Smgrp )
6 simprl โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ๐‘€ โˆˆ โ„• )
7 simprr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ๐‘ โˆˆ โ„• )
8 simpr3 โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
9 8 adantr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
10 1 2 mulgnnass โŠข ( ( ๐บ โˆˆ Smgrp โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) )
11 5 6 7 9 10 syl13anc โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) )
12 11 expr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) ) )
13 eqid โŠข ( 0g โ€˜ ๐บ ) = ( 0g โ€˜ ๐บ )
14 1 13 2 mulg0 โŠข ( ๐‘‹ โˆˆ ๐ต โ†’ ( 0 ยท ๐‘‹ ) = ( 0g โ€˜ ๐บ ) )
15 8 14 syl โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( 0 ยท ๐‘‹ ) = ( 0g โ€˜ ๐บ ) )
16 simpr1 โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐‘€ โˆˆ โ„•0 )
17 16 nn0cnd โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐‘€ โˆˆ โ„‚ )
18 17 mul01d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท 0 ) = 0 )
19 18 oveq1d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท 0 ) ยท ๐‘‹ ) = ( 0 ยท ๐‘‹ ) )
20 15 oveq2d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) = ( ๐‘€ ยท ( 0g โ€˜ ๐บ ) ) )
21 1 2 13 mulgnn0z โŠข ( ( ๐บ โˆˆ Mnd โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ ยท ( 0g โ€˜ ๐บ ) ) = ( 0g โ€˜ ๐บ ) )
22 21 3ad2antr1 โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( 0g โ€˜ ๐บ ) ) = ( 0g โ€˜ ๐บ ) )
23 20 22 eqtrd โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) = ( 0g โ€˜ ๐บ ) )
24 15 19 23 3eqtr4d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท 0 ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) )
25 24 adantr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( ๐‘€ ยท 0 ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) )
26 oveq2 โŠข ( ๐‘ = 0 โ†’ ( ๐‘€ ยท ๐‘ ) = ( ๐‘€ ยท 0 ) )
27 26 oveq1d โŠข ( ๐‘ = 0 โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ( ๐‘€ ยท 0 ) ยท ๐‘‹ ) )
28 oveq1 โŠข ( ๐‘ = 0 โ†’ ( ๐‘ ยท ๐‘‹ ) = ( 0 ยท ๐‘‹ ) )
29 28 oveq2d โŠข ( ๐‘ = 0 โ†’ ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) = ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) )
30 27 29 eqeq12d โŠข ( ๐‘ = 0 โ†’ ( ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) โ†” ( ( ๐‘€ ยท 0 ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( 0 ยท ๐‘‹ ) ) ) )
31 25 30 syl5ibrcom โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐‘ = 0 โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) ) )
32 simpr2 โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐‘ โˆˆ โ„•0 )
33 elnn0 โŠข ( ๐‘ โˆˆ โ„•0 โ†” ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) )
34 32 33 sylib โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) )
35 34 adantr โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ๐‘ โˆˆ โ„• โˆจ ๐‘ = 0 ) )
36 12 31 35 mpjaod โŠข ( ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„• ) โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) )
37 36 ex โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ โˆˆ โ„• โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) ) )
38 32 nn0cnd โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ๐‘ โˆˆ โ„‚ )
39 38 mul02d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( 0 ยท ๐‘ ) = 0 )
40 39 oveq1d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( 0 ยท ๐‘ ) ยท ๐‘‹ ) = ( 0 ยท ๐‘‹ ) )
41 1 2 mulgnn0cl โŠข ( ( ๐บ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘ ยท ๐‘‹ ) โˆˆ ๐ต )
42 41 3adant3r1 โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘ ยท ๐‘‹ ) โˆˆ ๐ต )
43 1 13 2 mulg0 โŠข ( ( ๐‘ ยท ๐‘‹ ) โˆˆ ๐ต โ†’ ( 0 ยท ( ๐‘ ยท ๐‘‹ ) ) = ( 0g โ€˜ ๐บ ) )
44 42 43 syl โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( 0 ยท ( ๐‘ ยท ๐‘‹ ) ) = ( 0g โ€˜ ๐บ ) )
45 15 40 44 3eqtr4d โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( 0 ยท ๐‘ ) ยท ๐‘‹ ) = ( 0 ยท ( ๐‘ ยท ๐‘‹ ) ) )
46 oveq1 โŠข ( ๐‘€ = 0 โ†’ ( ๐‘€ ยท ๐‘ ) = ( 0 ยท ๐‘ ) )
47 46 oveq1d โŠข ( ๐‘€ = 0 โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ( 0 ยท ๐‘ ) ยท ๐‘‹ ) )
48 oveq1 โŠข ( ๐‘€ = 0 โ†’ ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) = ( 0 ยท ( ๐‘ ยท ๐‘‹ ) ) )
49 47 48 eqeq12d โŠข ( ๐‘€ = 0 โ†’ ( ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) โ†” ( ( 0 ยท ๐‘ ) ยท ๐‘‹ ) = ( 0 ยท ( ๐‘ ยท ๐‘‹ ) ) ) )
50 45 49 syl5ibrcom โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ = 0 โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) ) )
51 elnn0 โŠข ( ๐‘€ โˆˆ โ„•0 โ†” ( ๐‘€ โˆˆ โ„• โˆจ ๐‘€ = 0 ) )
52 16 51 sylib โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ โˆˆ โ„• โˆจ ๐‘€ = 0 ) )
53 37 50 52 mpjaod โŠข ( ( ๐บ โˆˆ Mnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท ๐‘ ) ยท ๐‘‹ ) = ( ๐‘€ ยท ( ๐‘ ยท ๐‘‹ ) ) )