Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โค) |
2 | | elznn0 12521 |
. . . 4
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
3 | 2 | simprbi 498 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
4 | 1, 3 | syl 17 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ โ โ0 โจ -๐ โ
โ0)) |
5 | | simpr2 1196 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โค) |
6 | | elznn0 12521 |
. . . 4
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
7 | 6 | simprbi 498 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
8 | 5, 7 | syl 17 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ โ โ0 โจ -๐ โ
โ0)) |
9 | | grpmnd 18762 |
. . . . . 6
โข (๐บ โ Grp โ ๐บ โ Mnd) |
10 | 9 | ad2antrr 725 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐บ โ
Mnd) |
11 | | simprl 770 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ0) |
12 | | simprr 772 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ0) |
13 | | simplr3 1218 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ ๐ต) |
14 | | mulgass.b |
. . . . . 6
โข ๐ต = (Baseโ๐บ) |
15 | | mulgass.t |
. . . . . 6
โข ยท =
(.gโ๐บ) |
16 | 14, 15 | mulgnn0ass 18919 |
. . . . 5
โข ((๐บ โ Mnd โง (๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
17 | 10, 11, 12, 13, 16 | syl13anc 1373 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง ๐ โ โ0))
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
18 | 17 | ex 414 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ โ โ0 โง ๐ โ โ0)
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
19 | 1 | zcnd 12615 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โ) |
20 | 5 | zcnd 12615 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ โ) |
21 | 19, 20 | mulneg1d 11615 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท ๐) = -(๐ ยท ๐)) |
22 | 21 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ (-๐ ยท ๐) = -(๐ ยท ๐)) |
23 | 22 | oveq1d 7377 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ((-๐ ยท ๐) ยท ๐) = (-(๐ ยท ๐) ยท ๐)) |
24 | 9 | ad2antrr 725 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ๐บ โ
Mnd) |
25 | | simprl 770 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ -๐ โ
โ0) |
26 | | simprr 772 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ
โ0) |
27 | | simpr3 1197 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
28 | 27 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ๐ โ ๐ต) |
29 | 14, 15 | mulgnn0ass 18919 |
. . . . . . 7
โข ((๐บ โ Mnd โง (-๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ ๐ต)) โ ((-๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐))) |
30 | 24, 25, 26, 28, 29 | syl13anc 1373 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ((-๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐))) |
31 | 23, 30 | eqtr3d 2779 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ (-(๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐))) |
32 | | fveq2 6847 |
. . . . . . 7
โข ((-(๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐)) โ ((invgโ๐บ)โ(-(๐ ยท ๐) ยท ๐)) = ((invgโ๐บ)โ(-๐ ยท (๐ ยท ๐)))) |
33 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ๐บ โ Grp) |
34 | 1, 5 | zmulcld 12620 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ โค) |
35 | | eqid 2737 |
. . . . . . . . . . . 12
โข
(invgโ๐บ) = (invgโ๐บ) |
36 | 14, 15, 35 | mulgneg 18901 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ ยท ๐) โ โค โง ๐ โ ๐ต) โ (-(๐ ยท ๐) ยท ๐) = ((invgโ๐บ)โ((๐ ยท ๐) ยท ๐))) |
37 | 33, 34, 27, 36 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-(๐ ยท ๐) ยท ๐) = ((invgโ๐บ)โ((๐ ยท ๐) ยท ๐))) |
38 | 37 | fveq2d 6851 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ(-(๐ ยท ๐) ยท ๐)) = ((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) ยท ๐)))) |
39 | 14, 15 | mulgcl 18900 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ ยท ๐) โ โค โง ๐ โ ๐ต) โ ((๐ ยท ๐) ยท ๐) โ ๐ต) |
40 | 33, 34, 27, 39 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) โ ๐ต) |
41 | 14, 35 | grpinvinv 18821 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ((๐ ยท ๐) ยท ๐) โ ๐ต) โ ((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) ยท ๐))) = ((๐ ยท ๐) ยท ๐)) |
42 | 40, 41 | syldan 592 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) ยท ๐))) = ((๐ ยท ๐) ยท ๐)) |
43 | 38, 42 | eqtrd 2777 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ(-(๐ ยท ๐) ยท ๐)) = ((๐ ยท ๐) ยท ๐)) |
44 | 14, 15 | mulgcl 18900 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
45 | 33, 5, 27, 44 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
46 | 14, 15, 35 | mulgneg 18901 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง ๐ โ โค โง (๐ ยท ๐) โ ๐ต) โ (-๐ ยท (๐ ยท ๐)) = ((invgโ๐บ)โ(๐ ยท (๐ ยท ๐)))) |
47 | 33, 1, 45, 46 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท (๐ ยท ๐)) = ((invgโ๐บ)โ(๐ ยท (๐ ยท ๐)))) |
48 | 47 | fveq2d 6851 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ(-๐ ยท (๐ ยท ๐))) = ((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ ยท ๐))))) |
49 | 14, 15 | mulgcl 18900 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง ๐ โ โค โง (๐ ยท ๐) โ ๐ต) โ (๐ ยท (๐ ยท ๐)) โ ๐ต) |
50 | 33, 1, 45, 49 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท (๐ ยท ๐)) โ ๐ต) |
51 | 14, 35 | grpinvinv 18821 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ ยท (๐ ยท ๐)) โ ๐ต) โ ((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ ยท ๐)))) = (๐ ยท (๐ ยท ๐))) |
52 | 50, 51 | syldan 592 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ ยท ๐)))) = (๐ ยท (๐ ยท ๐))) |
53 | 48, 52 | eqtrd 2777 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ(-๐ ยท (๐ ยท ๐))) = (๐ ยท (๐ ยท ๐))) |
54 | 43, 53 | eqeq12d 2753 |
. . . . . . 7
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (((invgโ๐บ)โ(-(๐ ยท ๐) ยท ๐)) = ((invgโ๐บ)โ(-๐ ยท (๐ ยท ๐))) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
55 | 32, 54 | imbitrid 243 |
. . . . . 6
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((-(๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
56 | 55 | imp 408 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-(๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐))) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
57 | 31, 56 | syldan 592 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง ๐ โ โ0))
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
58 | 57 | ex 414 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((-๐ โ โ0 โง ๐ โ โ0)
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
59 | 9 | ad2antrr 725 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ๐บ โ
Mnd) |
60 | | simprl 770 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ๐ โ
โ0) |
61 | | simprr 772 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ -๐ โ
โ0) |
62 | 27 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ๐ โ ๐ต) |
63 | 14, 15 | mulgnn0ass 18919 |
. . . . . . 7
โข ((๐บ โ Mnd โง (๐ โ โ0
โง -๐ โ
โ0 โง ๐
โ ๐ต)) โ ((๐ ยท -๐) ยท ๐) = (๐ ยท (-๐ ยท ๐))) |
64 | 59, 60, 61, 62, 63 | syl13anc 1373 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ((๐ ยท -๐) ยท ๐) = (๐ ยท (-๐ ยท ๐))) |
65 | 19, 20 | mulneg2d 11616 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท -๐) = -(๐ ยท ๐)) |
66 | 65 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ (๐ ยท -๐) = -(๐ ยท ๐)) |
67 | 66 | oveq1d 7377 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ((๐ ยท -๐) ยท ๐) = (-(๐ ยท ๐) ยท ๐)) |
68 | 14, 15, 35 | mulgneg 18901 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
69 | 33, 5, 27, 68 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
70 | 69 | oveq2d 7378 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท (-๐ ยท ๐)) = (๐ ยท
((invgโ๐บ)โ(๐ ยท ๐)))) |
71 | 14, 15, 35 | mulgneg2 18917 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ โ โค โง (๐ ยท ๐) โ ๐ต) โ (-๐ ยท (๐ ยท ๐)) = (๐ ยท
((invgโ๐บ)โ(๐ ยท ๐)))) |
72 | 33, 1, 45, 71 | syl3anc 1372 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท (๐ ยท ๐)) = (๐ ยท
((invgโ๐บ)โ(๐ ยท ๐)))) |
73 | 70, 72 | eqtr4d 2780 |
. . . . . . 7
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (๐ ยท (-๐ ยท ๐)) = (-๐ ยท (๐ ยท ๐))) |
74 | 73 | adantr 482 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ (๐ ยท
(-๐ ยท ๐)) = (-๐ ยท (๐ ยท ๐))) |
75 | 64, 67, 74 | 3eqtr3d 2785 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ (-(๐ ยท ๐) ยท ๐) = (-๐ ยท (๐ ยท ๐))) |
76 | 75, 56 | syldan 592 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (๐ โ โ0 โง -๐ โ โ0))
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
77 | 76 | ex 414 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ โ โ0 โง -๐ โ โ0)
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
78 | 9 | ad2antrr 725 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ๐บ โ
Mnd) |
79 | | simprl 770 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ -๐ โ
โ0) |
80 | | simprr 772 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ -๐ โ
โ0) |
81 | 27 | adantr 482 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ๐ โ ๐ต) |
82 | 14, 15 | mulgnn0ass 18919 |
. . . . . 6
โข ((๐บ โ Mnd โง (-๐ โ โ0
โง -๐ โ
โ0 โง ๐
โ ๐ต)) โ ((-๐ ยท -๐) ยท ๐) = (-๐ ยท (-๐ ยท ๐))) |
83 | 78, 79, 80, 81, 82 | syl13anc 1373 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ((-๐ ยท -๐) ยท ๐) = (-๐ ยท (-๐ ยท ๐))) |
84 | 19, 20 | mul2negd 11617 |
. . . . . . 7
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (-๐ ยท -๐) = (๐ ยท ๐)) |
85 | 84 | oveq1d 7377 |
. . . . . 6
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((-๐ ยท -๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
86 | 85 | adantr 482 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ((-๐ ยท -๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
87 | 33 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ๐บ โ
Grp) |
88 | 1 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ๐ โ
โค) |
89 | | nn0z 12531 |
. . . . . . . . 9
โข (-๐ โ โ0
โ -๐ โ
โค) |
90 | 89 | ad2antll 728 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ -๐ โ
โค) |
91 | 14, 15 | mulgcl 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) โ ๐ต) |
92 | 87, 90, 81, 91 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (-๐ ยท ๐) โ ๐ต) |
93 | 14, 15, 35 | mulgneg2 18917 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ โ โค โง (-๐ ยท ๐) โ ๐ต) โ (-๐ ยท (-๐ ยท ๐)) = (๐ ยท
((invgโ๐บ)โ(-๐ ยท ๐)))) |
94 | 87, 88, 92, 93 | syl3anc 1372 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (-๐ ยท
(-๐ ยท ๐)) = (๐ ยท
((invgโ๐บ)โ(-๐ ยท ๐)))) |
95 | 14, 15, 35 | mulgneg 18901 |
. . . . . . . . 9
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (--๐ ยท ๐) = ((invgโ๐บ)โ(-๐ ยท ๐))) |
96 | 87, 90, 81, 95 | syl3anc 1372 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (--๐ ยท ๐) =
((invgโ๐บ)โ(-๐ ยท ๐))) |
97 | 20 | negnegd 11510 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ --๐ = ๐) |
98 | 97 | adantr 482 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ --๐ = ๐) |
99 | 98 | oveq1d 7377 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (--๐ ยท ๐) = (๐ ยท ๐)) |
100 | 96, 99 | eqtr3d 2779 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ((invgโ๐บ)โ(-๐ ยท ๐)) = (๐ ยท ๐)) |
101 | 100 | oveq2d 7378 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (๐ ยท
((invgโ๐บ)โ(-๐ ยท ๐))) = (๐ ยท (๐ ยท ๐))) |
102 | 94, 101 | eqtrd 2777 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ (-๐ ยท
(-๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
103 | 83, 86, 102 | 3eqtr3d 2785 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โง (-๐ โ โ0 โง -๐ โ โ0))
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
104 | 103 | ex 414 |
. . 3
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((-๐ โ โ0 โง -๐ โ โ0)
โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
105 | 18, 58, 77, 104 | ccased 1038 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ (((๐ โ โ0 โจ -๐ โ โ0)
โง (๐ โ
โ0 โจ -๐
โ โ0)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
106 | 4, 8, 105 | mp2and 698 |
1
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |