Metamath Proof Explorer

Theorem mulgdi

Description: Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgdi.b โŠข ๐ต = ( Base โ€˜ ๐บ )
mulgdi.m โŠข ยท = ( .g โ€˜ ๐บ )
mulgdi.p โŠข + = ( +g โ€˜ ๐บ )
Assertion mulgdi ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 mulgdi.b โŠข ๐ต = ( Base โ€˜ ๐บ )
2 mulgdi.m โŠข ยท = ( .g โ€˜ ๐บ )
3 mulgdi.p โŠข + = ( +g โ€˜ ๐บ )
4 ablcmn โŠข ( ๐บ โˆˆ Abel โ†’ ๐บ โˆˆ CMnd )
5 4 ad2antrr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐บ โˆˆ CMnd )
6 simpr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘€ โˆˆ โ„•0 )
7 simplr2 โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘‹ โˆˆ ๐ต )
8 simplr3 โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘Œ โˆˆ ๐ต )
9 1 2 3 mulgnn0di โŠข ( ( ๐บ โˆˆ CMnd โˆง ( ๐‘€ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )
10 5 6 7 8 9 syl13anc โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )
11 4 ad2antrr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ๐บ โˆˆ CMnd )
12 simpr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ - ๐‘€ โˆˆ โ„•0 )
13 simpr2 โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
14 13 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘‹ โˆˆ ๐ต )
15 simpr3 โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘Œ โˆˆ ๐ต )
16 15 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘Œ โˆˆ ๐ต )
17 1 2 3 mulgnn0di โŠข ( ( ๐บ โˆˆ CMnd โˆง ( - ๐‘€ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( - ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( - ๐‘€ ยท ๐‘‹ ) + ( - ๐‘€ ยท ๐‘Œ ) ) )
18 11 12 14 16 17 syl13anc โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( - ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( - ๐‘€ ยท ๐‘‹ ) + ( - ๐‘€ ยท ๐‘Œ ) ) )
19 ablgrp โŠข ( ๐บ โˆˆ Abel โ†’ ๐บ โˆˆ Grp )
20 19 adantr โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐บ โˆˆ Grp )
21 simpr1 โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘€ โˆˆ โ„ค )
22 1 3 grpcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ๐‘‹ + ๐‘Œ ) โˆˆ ๐ต )
23 20 13 15 22 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘‹ + ๐‘Œ ) โˆˆ ๐ต )
24 eqid โŠข ( invg โ€˜ ๐บ ) = ( invg โ€˜ ๐บ )
25 1 2 24 mulgneg โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ( ๐‘‹ + ๐‘Œ ) โˆˆ ๐ต ) โ†’ ( - ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) )
26 20 21 23 25 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( - ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) )
27 26 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( - ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) )
28 1 2 24 mulgneg โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( - ๐‘€ ยท ๐‘‹ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) )
29 20 21 13 28 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( - ๐‘€ ยท ๐‘‹ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) )
30 1 2 24 mulgneg โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( - ๐‘€ ยท ๐‘Œ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) )
31 20 21 15 30 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( - ๐‘€ ยท ๐‘Œ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) )
32 29 31 oveq12d โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( - ๐‘€ ยท ๐‘‹ ) + ( - ๐‘€ ยท ๐‘Œ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
33 32 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( - ๐‘€ ยท ๐‘‹ ) + ( - ๐‘€ ยท ๐‘Œ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
34 18 27 33 3eqtr3d โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
35 simpl โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐บ โˆˆ Abel )
36 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ๐‘‹ ) โˆˆ ๐ต )
37 20 21 13 36 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ๐‘‹ ) โˆˆ ๐ต )
38 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ๐‘Œ ) โˆˆ ๐ต )
39 20 21 15 38 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ๐‘Œ ) โˆˆ ๐ต )
40 1 3 24 ablinvadd โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ ยท ๐‘‹ ) โˆˆ ๐ต โˆง ( ๐‘€ ยท ๐‘Œ ) โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
41 35 37 39 40 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
42 41 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ๐‘Œ ) ) ) )
43 34 42 eqtr4d โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) )
44 43 fveq2d โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) ) )
45 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ( ๐‘‹ + ๐‘Œ ) โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) โˆˆ ๐ต )
46 20 21 23 45 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) โˆˆ ๐ต )
47 46 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) โˆˆ ๐ต )
48 1 24 grpinvinv โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) ) = ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) )
49 20 47 48 syl2an2r โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) ) ) = ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) )
50 1 3 grpcl โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘€ ยท ๐‘‹ ) โˆˆ ๐ต โˆง ( ๐‘€ ยท ๐‘Œ ) โˆˆ ๐ต ) โ†’ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) โˆˆ ๐ต )
51 20 37 39 50 syl3anc โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) โˆˆ ๐ต )
52 51 adantr โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) โˆˆ ๐ต )
53 1 24 grpinvinv โŠข ( ( ๐บ โˆˆ Grp โˆง ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )
54 20 52 53 syl2an2r โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )
55 44 49 54 3eqtr3d โŠข ( ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง - ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )
56 elznn0 โŠข ( ๐‘€ โˆˆ โ„ค โ†” ( ๐‘€ โˆˆ โ„ โˆง ( ๐‘€ โˆˆ โ„•0 โˆจ - ๐‘€ โˆˆ โ„•0 ) ) )
57 56 simprbi โŠข ( ๐‘€ โˆˆ โ„ค โ†’ ( ๐‘€ โˆˆ โ„•0 โˆจ - ๐‘€ โˆˆ โ„•0 ) )
58 21 57 syl โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ โˆˆ โ„•0 โˆจ - ๐‘€ โˆˆ โ„•0 ) )
59 10 55 58 mpjaodan โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘‹ + ๐‘Œ ) ) = ( ( ๐‘€ ยท ๐‘‹ ) + ( ๐‘€ ยท ๐‘Œ ) ) )