Step | Hyp | Ref
| Expression |
1 | | ablcmn 19576 |
. . . 4
โข (๐บ โ Abel โ ๐บ โ CMnd) |
2 | 1 | ad2antrr 725 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐บ โ CMnd) |
3 | | simpr 486 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ
โ0) |
4 | | simplr2 1217 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ ๐ต) |
5 | | simplr3 1218 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ ๐ต) |
6 | | mulgdi.b |
. . . 4
โข ๐ต = (Baseโ๐บ) |
7 | | mulgdi.m |
. . . 4
โข ยท =
(.gโ๐บ) |
8 | | mulgdi.p |
. . . 4
โข + =
(+gโ๐บ) |
9 | 6, 7, 8 | mulgnn0di 19611 |
. . 3
โข ((๐บ โ CMnd โง (๐ โ โ0
โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
10 | 2, 3, 4, 5, 9 | syl13anc 1373 |
. 2
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
11 | 1 | ad2antrr 725 |
. . . . . . 7
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ ๐บ โ CMnd) |
12 | | simpr 486 |
. . . . . . 7
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ -๐ โ
โ0) |
13 | | simpr2 1196 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
14 | 13 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ ๐ โ ๐ต) |
15 | | simpr3 1197 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
16 | 15 | adantr 482 |
. . . . . . 7
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ ๐ โ ๐ต) |
17 | 6, 7, 8 | mulgnn0di 19611 |
. . . . . . 7
โข ((๐บ โ CMnd โง (-๐ โ โ0
โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (-๐ ยท (๐ + ๐)) = ((-๐ ยท ๐) + (-๐ ยท ๐))) |
18 | 11, 12, 14, 16, 17 | syl13anc 1373 |
. . . . . 6
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ (-๐ ยท (๐ + ๐)) = ((-๐ ยท ๐) + (-๐ ยท ๐))) |
19 | | ablgrp 19574 |
. . . . . . . . 9
โข (๐บ โ Abel โ ๐บ โ Grp) |
20 | 19 | adantr 482 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐บ โ Grp) |
21 | | simpr1 1195 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ โค) |
22 | 6, 8 | grpcl 18763 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) โ ๐ต) |
23 | 20, 13, 15, 22 | syl3anc 1372 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ + ๐) โ ๐ต) |
24 | | eqid 2737 |
. . . . . . . . 9
โข
(invgโ๐บ) = (invgโ๐บ) |
25 | 6, 7, 24 | mulgneg 18901 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ โ โค โง (๐ + ๐) โ ๐ต) โ (-๐ ยท (๐ + ๐)) = ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) |
26 | 20, 21, 23, 25 | syl3anc 1372 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (-๐ ยท (๐ + ๐)) = ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) |
27 | 26 | adantr 482 |
. . . . . 6
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ (-๐ ยท (๐ + ๐)) = ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) |
28 | 6, 7, 24 | mulgneg 18901 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
29 | 20, 21, 13, 28 | syl3anc 1372 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
30 | 6, 7, 24 | mulgneg 18901 |
. . . . . . . . 9
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
31 | 20, 21, 15, 30 | syl3anc 1372 |
. . . . . . . 8
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
32 | 29, 31 | oveq12d 7380 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((-๐ ยท ๐) + (-๐ ยท ๐)) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
33 | 32 | adantr 482 |
. . . . . 6
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ ((-๐ ยท ๐) + (-๐ ยท ๐)) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
34 | 18, 27, 33 | 3eqtr3d 2785 |
. . . . 5
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ(๐ ยท (๐ + ๐))) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
35 | | simpl 484 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐บ โ Abel) |
36 | 6, 7 | mulgcl 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
37 | 20, 21, 13, 36 | syl3anc 1372 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
38 | 6, 7 | mulgcl 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
39 | 20, 21, 15, 38 | syl3anc 1372 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
40 | 6, 8, 24 | ablinvadd 19595 |
. . . . . . 7
โข ((๐บ โ Abel โง (๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐))) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
41 | 35, 37, 39, 40 | syl3anc 1372 |
. . . . . 6
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐))) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
42 | 41 | adantr 482 |
. . . . 5
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐))) = (((invgโ๐บ)โ(๐ ยท ๐)) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
43 | 34, 42 | eqtr4d 2780 |
. . . 4
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ(๐ ยท (๐ + ๐))) = ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐)))) |
44 | 43 | fveq2d 6851 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) = ((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐))))) |
45 | 6, 7 | mulgcl 18900 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ โ โค โง (๐ + ๐) โ ๐ต) โ (๐ ยท (๐ + ๐)) โ ๐ต) |
46 | 20, 21, 23, 45 | syl3anc 1372 |
. . . . 5
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) โ ๐ต) |
47 | 46 | adantr 482 |
. . . 4
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ (๐ ยท (๐ + ๐)) โ ๐ต) |
48 | 6, 24 | grpinvinv 18821 |
. . . 4
โข ((๐บ โ Grp โง (๐ ยท (๐ + ๐)) โ ๐ต) โ ((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) = (๐ ยท (๐ + ๐))) |
49 | 20, 47, 48 | syl2an2r 684 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ((invgโ๐บ)โ(๐ ยท (๐ + ๐)))) = (๐ ยท (๐ + ๐))) |
50 | 6, 8 | grpcl 18763 |
. . . . . 6
โข ((๐บ โ Grp โง (๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ ((๐ ยท ๐) + (๐ ยท ๐)) โ ๐ต) |
51 | 20, 37, 39, 50 | syl3anc 1372 |
. . . . 5
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) + (๐ ยท ๐)) โ ๐ต) |
52 | 51 | adantr 482 |
. . . 4
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ ((๐ ยท ๐) + (๐ ยท ๐)) โ ๐ต) |
53 | 6, 24 | grpinvinv 18821 |
. . . 4
โข ((๐บ โ Grp โง ((๐ ยท ๐) + (๐ ยท ๐)) โ ๐ต) โ ((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐)))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
54 | 20, 52, 53 | syl2an2r 684 |
. . 3
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ
((invgโ๐บ)โ((invgโ๐บ)โ((๐ ยท ๐) + (๐ ยท ๐)))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
55 | 44, 49, 54 | 3eqtr3d 2785 |
. 2
โข (((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง -๐ โ โ0) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
56 | | elznn0 12521 |
. . . 4
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
57 | 56 | simprbi 498 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
58 | 21, 57 | syl 17 |
. 2
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โจ -๐ โ
โ0)) |
59 | 10, 55, 58 | mpjaodan 958 |
1
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |