Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐บ โ Abel) |
2 | | simpr1 1195 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ โค) |
3 | | simpr2 1196 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
4 | | ablgrp 19574 |
. . . . . 6
โข (๐บ โ Abel โ ๐บ โ Grp) |
5 | 4 | adantr 482 |
. . . . 5
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐บ โ Grp) |
6 | | simpr3 1197 |
. . . . 5
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
7 | | mulgsubdi.b |
. . . . . 6
โข ๐ต = (Baseโ๐บ) |
8 | | eqid 2737 |
. . . . . 6
โข
(invgโ๐บ) = (invgโ๐บ) |
9 | 7, 8 | grpinvcl 18805 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ ๐ต) โ ((invgโ๐บ)โ๐) โ ๐ต) |
10 | 5, 6, 9 | syl2anc 585 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ๐) โ ๐ต) |
11 | | mulgsubdi.t |
. . . . 5
โข ยท =
(.gโ๐บ) |
12 | | eqid 2737 |
. . . . 5
โข
(+gโ๐บ) = (+gโ๐บ) |
13 | 7, 11, 12 | mulgdi 19612 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ((invgโ๐บ)โ๐) โ ๐ต)) โ (๐ ยท (๐(+gโ๐บ)((invgโ๐บ)โ๐))) = ((๐ ยท ๐)(+gโ๐บ)(๐ ยท
((invgโ๐บ)โ๐)))) |
14 | 1, 2, 3, 10, 13 | syl13anc 1373 |
. . 3
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐(+gโ๐บ)((invgโ๐บ)โ๐))) = ((๐ ยท ๐)(+gโ๐บ)(๐ ยท
((invgโ๐บ)โ๐)))) |
15 | 7, 11, 8 | mulginvcom 18908 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท
((invgโ๐บ)โ๐)) = ((invgโ๐บ)โ(๐ ยท ๐))) |
16 | 5, 2, 6, 15 | syl3anc 1372 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท
((invgโ๐บ)โ๐)) = ((invgโ๐บ)โ(๐ ยท ๐))) |
17 | 16 | oveq2d 7378 |
. . 3
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐)(+gโ๐บ)(๐ ยท
((invgโ๐บ)โ๐))) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
18 | 14, 17 | eqtrd 2777 |
. 2
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐(+gโ๐บ)((invgโ๐บ)โ๐))) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
19 | | mulgsubdi.d |
. . . . 5
โข โ =
(-gโ๐บ) |
20 | 7, 12, 8, 19 | grpsubval 18803 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐(+gโ๐บ)((invgโ๐บ)โ๐))) |
21 | 3, 6, 20 | syl2anc 585 |
. . 3
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐) = (๐(+gโ๐บ)((invgโ๐บ)โ๐))) |
22 | 21 | oveq2d 7378 |
. 2
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ โ ๐)) = (๐ ยท (๐(+gโ๐บ)((invgโ๐บ)โ๐)))) |
23 | 7, 11 | mulgcl 18900 |
. . . 4
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
24 | 5, 2, 3, 23 | syl3anc 1372 |
. . 3
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
25 | 7, 11 | mulgcl 18900 |
. . . 4
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
26 | 5, 2, 6, 25 | syl3anc 1372 |
. . 3
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
27 | 7, 12, 8, 19 | grpsubval 18803 |
. . 3
โข (((๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
28 | 24, 26, 27 | syl2anc 585 |
. 2
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
29 | 18, 22, 28 | 3eqtr4d 2787 |
1
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ โ ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) |