Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ๐บ โ Grp) |
2 | 1 | grpmndd 18767 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ๐บ โ Mnd) |
3 | | simprl 770 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ๐ โ
โ0) |
4 | | simprr 772 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ๐ โ
โ0) |
5 | | simpl23 1254 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ๐ โ ๐ต) |
6 | | mulgnndir.b |
. . . . . 6
โข ๐ต = (Baseโ๐บ) |
7 | | mulgnndir.t |
. . . . . 6
โข ยท =
(.gโ๐บ) |
8 | | mulgnndir.p |
. . . . . 6
โข + =
(+gโ๐บ) |
9 | 6, 7, 8 | mulgnn0dir 18913 |
. . . . 5
โข ((๐บ โ Mnd โง (๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
10 | 2, 3, 4, 5, 9 | syl13anc 1373 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง ๐ โ
โ0)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
11 | 10 | anassrs 469 |
. . 3
โข ((((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
12 | | simpl1 1192 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐บ โ Grp) |
13 | | simp22 1208 |
. . . . . . . . . . 11
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ๐ โ
โค) |
14 | 13 | adantr 482 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐ โ โค) |
15 | | simpl23 1254 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐ โ ๐ต) |
16 | | eqid 2737 |
. . . . . . . . . . 11
โข
(invgโ๐บ) = (invgโ๐บ) |
17 | 6, 7, 16 | mulgneg 18901 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
18 | 12, 14, 15, 17 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
19 | 18 | oveq1d 7377 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((-๐ ยท ๐) + (๐ ยท ๐)) = (((invgโ๐บ)โ(๐ ยท ๐)) + (๐ ยท ๐))) |
20 | 6, 7 | mulgcl 18900 |
. . . . . . . . . 10
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
21 | 12, 14, 15, 20 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (๐ ยท ๐) โ ๐ต) |
22 | | eqid 2737 |
. . . . . . . . . 10
โข
(0gโ๐บ) = (0gโ๐บ) |
23 | 6, 8, 22, 16 | grplinv 18807 |
. . . . . . . . 9
โข ((๐บ โ Grp โง (๐ ยท ๐) โ ๐ต) โ (((invgโ๐บ)โ(๐ ยท ๐)) + (๐ ยท ๐)) = (0gโ๐บ)) |
24 | 12, 21, 23 | syl2anc 585 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((invgโ๐บ)โ(๐ ยท ๐)) + (๐ ยท ๐)) = (0gโ๐บ)) |
25 | 19, 24 | eqtrd 2777 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((-๐ ยท ๐) + (๐ ยท ๐)) = (0gโ๐บ)) |
26 | 25 | oveq2d 7378 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) ยท ๐) + ((-๐ ยท ๐) + (๐ ยท ๐))) = (((๐ + ๐) ยท ๐) + (0gโ๐บ))) |
27 | | simpl3 1194 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (๐ + ๐) โ
โ0) |
28 | | nn0z 12531 |
. . . . . . . . 9
โข ((๐ + ๐) โ โ0 โ (๐ + ๐) โ โค) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (๐ + ๐) โ โค) |
30 | 6, 7 | mulgcl 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ + ๐) โ โค โง ๐ โ ๐ต) โ ((๐ + ๐) ยท ๐) โ ๐ต) |
31 | 12, 29, 15, 30 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((๐ + ๐) ยท ๐) โ ๐ต) |
32 | 6, 8, 22 | grprid 18788 |
. . . . . . 7
โข ((๐บ โ Grp โง ((๐ + ๐) ยท ๐) โ ๐ต) โ (((๐ + ๐) ยท ๐) + (0gโ๐บ)) = ((๐ + ๐) ยท ๐)) |
33 | 12, 31, 32 | syl2anc 585 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) ยท ๐) + (0gโ๐บ)) = ((๐ + ๐) ยท ๐)) |
34 | 26, 33 | eqtrd 2777 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) ยท ๐) + ((-๐ ยท ๐) + (๐ ยท ๐))) = ((๐ + ๐) ยท ๐)) |
35 | | nn0z 12531 |
. . . . . . . . 9
โข (-๐ โ โ0
โ -๐ โ
โค) |
36 | 35 | ad2antll 728 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ -๐ โ โค) |
37 | 6, 7 | mulgcl 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) โ ๐ต) |
38 | 12, 36, 15, 37 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (-๐ ยท ๐) โ ๐ต) |
39 | 6, 8 | grpass 18764 |
. . . . . . 7
โข ((๐บ โ Grp โง (((๐ + ๐) ยท ๐) โ ๐ต โง (-๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต)) โ ((((๐ + ๐) ยท ๐) + (-๐ ยท ๐)) + (๐ ยท ๐)) = (((๐ + ๐) ยท ๐) + ((-๐ ยท ๐) + (๐ ยท ๐)))) |
40 | 12, 31, 38, 21, 39 | syl13anc 1373 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((((๐ + ๐) ยท ๐) + (-๐ ยท ๐)) + (๐ ยท ๐)) = (((๐ + ๐) ยท ๐) + ((-๐ ยท ๐) + (๐ ยท ๐)))) |
41 | 12 | grpmndd 18767 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐บ โ Mnd) |
42 | | simprr 772 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ -๐ โ
โ0) |
43 | 6, 7, 8 | mulgnn0dir 18913 |
. . . . . . . . 9
โข ((๐บ โ Mnd โง ((๐ + ๐) โ โ0 โง -๐ โ โ0
โง ๐ โ ๐ต)) โ (((๐ + ๐) + -๐) ยท ๐) = (((๐ + ๐) ยท ๐) + (-๐ ยท ๐))) |
44 | 41, 27, 42, 15, 43 | syl13anc 1373 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) + -๐) ยท ๐) = (((๐ + ๐) ยท ๐) + (-๐ ยท ๐))) |
45 | | simp21 1207 |
. . . . . . . . . . . . . 14
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ๐ โ
โค) |
46 | 45 | zcnd 12615 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ๐ โ
โ) |
47 | 13 | zcnd 12615 |
. . . . . . . . . . . . 13
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ๐ โ
โ) |
48 | 46, 47 | addcld 11181 |
. . . . . . . . . . . 12
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ (๐ + ๐) โ โ) |
49 | 48 | adantr 482 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (๐ + ๐) โ โ) |
50 | 47 | adantr 482 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐ โ โ) |
51 | 49, 50 | negsubd 11525 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((๐ + ๐) + -๐) = ((๐ + ๐) โ ๐)) |
52 | 46 | adantr 482 |
. . . . . . . . . . 11
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ๐ โ โ) |
53 | 52, 50 | pncand 11520 |
. . . . . . . . . 10
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((๐ + ๐) โ ๐) = ๐) |
54 | 51, 53 | eqtrd 2777 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((๐ + ๐) + -๐) = ๐) |
55 | 54 | oveq1d 7377 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) + -๐) ยท ๐) = (๐ ยท ๐)) |
56 | 44, 55 | eqtr3d 2779 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) ยท ๐) + (-๐ ยท ๐)) = (๐ ยท ๐)) |
57 | 56 | oveq1d 7377 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((((๐ + ๐) ยท ๐) + (-๐ ยท ๐)) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
58 | 40, 57 | eqtr3d 2779 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ (((๐ + ๐) ยท ๐) + ((-๐ ยท ๐) + (๐ ยท ๐))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
59 | 34, 58 | eqtr3d 2779 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง (๐ โ โ0
โง -๐ โ
โ0)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
60 | 59 | anassrs 469 |
. . 3
โข ((((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง ๐ โ โ0)
โง -๐ โ
โ0) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
61 | | elznn0 12521 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
62 | 61 | simprbi 498 |
. . . . 5
โข (๐ โ โค โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
63 | 13, 62 | syl 17 |
. . . 4
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
64 | 63 | adantr 482 |
. . 3
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง ๐ โ โ0)
โ (๐ โ
โ0 โจ -๐
โ โ0)) |
65 | 11, 60, 64 | mpjaodan 958 |
. 2
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง ๐ โ โ0)
โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
66 | | simpl1 1192 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐บ โ
Grp) |
67 | 45 | adantr 482 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐ โ
โค) |
68 | | simpl23 1254 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐ โ ๐ต) |
69 | 6, 7 | mulgcl 18900 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
70 | 66, 67, 68, 69 | syl3anc 1372 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (๐ ยท ๐) โ ๐ต) |
71 | 67 | znegcld 12616 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ -๐ โ
โค) |
72 | 6, 7 | mulgcl 18900 |
. . . . 5
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) โ ๐ต) |
73 | 66, 71, 68, 72 | syl3anc 1372 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (-๐ ยท ๐) โ ๐ต) |
74 | 28 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ (๐ + ๐) โ โค) |
75 | 74 | adantr 482 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (๐ + ๐) โ
โค) |
76 | 66, 75, 68, 30 | syl3anc 1372 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ + ๐) ยท ๐) โ ๐ต) |
77 | 6, 8 | grpass 18764 |
. . . 4
โข ((๐บ โ Grp โง ((๐ ยท ๐) โ ๐ต โง (-๐ ยท ๐) โ ๐ต โง ((๐ + ๐) ยท ๐) โ ๐ต)) โ (((๐ ยท ๐) + (-๐ ยท ๐)) + ((๐ + ๐) ยท ๐)) = ((๐ ยท ๐) + ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐)))) |
78 | 66, 70, 73, 76, 77 | syl13anc 1373 |
. . 3
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (((๐ ยท ๐) + (-๐ ยท ๐)) + ((๐ + ๐) ยท ๐)) = ((๐ ยท ๐) + ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐)))) |
79 | 6, 7, 16 | mulgneg 18901 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = ((invgโ๐บ)โ(๐ ยท ๐))) |
80 | 66, 67, 68, 79 | syl3anc 1372 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (-๐ ยท ๐) =
((invgโ๐บ)โ(๐ ยท ๐))) |
81 | 80 | oveq2d 7378 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ ยท ๐) + (-๐ ยท ๐)) = ((๐ ยท ๐) +
((invgโ๐บ)โ(๐ ยท ๐)))) |
82 | 6, 8, 22, 16 | grprinv 18808 |
. . . . . . 7
โข ((๐บ โ Grp โง (๐ ยท ๐) โ ๐ต) โ ((๐ ยท ๐) +
((invgโ๐บ)โ(๐ ยท ๐))) = (0gโ๐บ)) |
83 | 66, 70, 82 | syl2anc 585 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ ยท ๐) +
((invgโ๐บ)โ(๐ ยท ๐))) = (0gโ๐บ)) |
84 | 81, 83 | eqtrd 2777 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ ยท ๐) + (-๐ ยท ๐)) = (0gโ๐บ)) |
85 | 84 | oveq1d 7377 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (((๐ ยท ๐) + (-๐ ยท ๐)) + ((๐ + ๐) ยท ๐)) = ((0gโ๐บ) + ((๐ + ๐) ยท ๐))) |
86 | 6, 8, 22 | grplid 18787 |
. . . . 5
โข ((๐บ โ Grp โง ((๐ + ๐) ยท ๐) โ ๐ต) โ ((0gโ๐บ) + ((๐ + ๐) ยท ๐)) = ((๐ + ๐) ยท ๐)) |
87 | 66, 76, 86 | syl2anc 585 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((0gโ๐บ) + ((๐ + ๐) ยท ๐)) = ((๐ + ๐) ยท ๐)) |
88 | 85, 87 | eqtrd 2777 |
. . 3
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (((๐ ยท ๐) + (-๐ ยท ๐)) + ((๐ + ๐) ยท ๐)) = ((๐ + ๐) ยท ๐)) |
89 | 66 | grpmndd 18767 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐บ โ
Mnd) |
90 | | simpr 486 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ -๐ โ
โ0) |
91 | | simpl3 1194 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (๐ + ๐) โ
โ0) |
92 | 6, 7, 8 | mulgnn0dir 18913 |
. . . . . 6
โข ((๐บ โ Mnd โง (-๐ โ โ0
โง (๐ + ๐) โ โ0
โง ๐ โ ๐ต)) โ ((-๐ + (๐ + ๐)) ยท ๐) = ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐))) |
93 | 89, 90, 91, 68, 92 | syl13anc 1373 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((-๐ + (๐ + ๐)) ยท ๐) = ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐))) |
94 | 46 | adantr 482 |
. . . . . . . . 9
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐ โ
โ) |
95 | 94 | negcld 11506 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ -๐ โ
โ) |
96 | 48 | adantr 482 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (๐ + ๐) โ
โ) |
97 | 95, 96 | addcomd 11364 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (-๐ + (๐ + ๐)) = ((๐ + ๐) + -๐)) |
98 | 96, 94 | negsubd 11525 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ + ๐) + -๐) = ((๐ + ๐) โ ๐)) |
99 | 47 | adantr 482 |
. . . . . . . 8
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ๐ โ
โ) |
100 | 94, 99 | pncan2d 11521 |
. . . . . . 7
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ + ๐) โ ๐) = ๐) |
101 | 97, 98, 100 | 3eqtrd 2781 |
. . . . . 6
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ (-๐ + (๐ + ๐)) = ๐) |
102 | 101 | oveq1d 7377 |
. . . . 5
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((-๐ + (๐ + ๐)) ยท ๐) = (๐ ยท ๐)) |
103 | 93, 102 | eqtr3d 2779 |
. . . 4
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐)) = (๐ ยท ๐)) |
104 | 103 | oveq2d 7378 |
. . 3
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ ยท ๐) + ((-๐ ยท ๐) + ((๐ + ๐) ยท ๐))) = ((๐ ยท ๐) + (๐ ยท ๐))) |
105 | 78, 88, 104 | 3eqtr3d 2785 |
. 2
โข (((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โง -๐ โ โ0)
โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
106 | | elznn0 12521 |
. . . 4
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
107 | 106 | simprbi 498 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
108 | 45, 107 | syl 17 |
. 2
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ (๐ โ โ0 โจ
-๐ โ
โ0)) |
109 | 65, 105, 108 | mpjaodan 958 |
1
โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |