Step | Hyp | Ref
| Expression |
1 | | znegcl 9286 |
. . 3
โข (๐ โ โค โ -๐ โ
โค) |
2 | | mulgsubdir.b |
. . . 4
โข ๐ต = (Baseโ๐บ) |
3 | | mulgsubdir.t |
. . . 4
โข ยท =
(.gโ๐บ) |
4 | | eqid 2177 |
. . . 4
โข
(+gโ๐บ) = (+gโ๐บ) |
5 | 2, 3, 4 | mulgdir 13020 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง -๐ โ โค โง ๐ โ ๐ต)) โ ((๐ + -๐) ยท ๐) = ((๐ ยท ๐)(+gโ๐บ)(-๐ ยท ๐))) |
6 | 1, 5 | syl3anr2 1291 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ + -๐) ยท ๐) = ((๐ ยท ๐)(+gโ๐บ)(-๐ ยท ๐))) |
7 | | simpr1 1003 |
. . . . 5
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โค) |
8 | 7 | zcnd 9378 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โ) |
9 | | simpr2 1004 |
. . . . 5
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โค) |
10 | 9 | zcnd 9378 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โ) |
11 | 8, 10 | negsubd 8276 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ + -๐) = (๐ โ ๐)) |
12 | 11 | oveq1d 5892 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ + -๐) ยท ๐) = ((๐ โ ๐) ยท ๐)) |
13 | | eqid 2177 |
. . . . . 6
โข
(invgโ๐บ) = (invgโ๐บ) |
14 | 2, 3, 13 | mulgneg 13006 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
15 | 14 | 3adant3r1 1212 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
16 | 15 | oveq2d 5893 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐)(+gโ๐บ)(-๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
17 | 2, 3 | mulgcl 13005 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
18 | 17 | 3adant3r2 1213 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
19 | 2, 3 | mulgcl 13005 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
20 | 19 | 3adant3r1 1212 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
21 | | mulgsubdir.d |
. . . . 5
โข โ =
(-gโ๐บ) |
22 | 2, 4, 13, 21 | grpsubval 12924 |
. . . 4
โข (((๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
23 | 18, 20, 22 | syl2anc 411 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐บ)((invgโ๐บ)โ(๐ ยท ๐)))) |
24 | 16, 23 | eqtr4d 2213 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐)(+gโ๐บ)(-๐ ยท ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) |
25 | 6, 12, 24 | 3eqtr3d 2218 |
1
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ โ ๐) ยท ๐) = ((๐ ยท ๐) โ (๐ ยท ๐))) |