Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ ๐บ โ Grp) |
2 | 1 | adantr 481 |
. . . . 5
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ๐บ โ Grp) |
3 | | simp3 1138 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
4 | 3 | adantr 481 |
. . . . 5
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ๐ โ ๐ต) |
5 | | znegcl 12596 |
. . . . . . 7
โข (๐ฆ โ โค โ -๐ฆ โ
โค) |
6 | | mulgaddcom.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐บ) |
7 | | mulgaddcom.t |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
8 | 6, 7 | mulgcl 18970 |
. . . . . . 7
โข ((๐บ โ Grp โง -๐ฆ โ โค โง ๐ โ ๐ต) โ (-๐ฆ ยท ๐) โ ๐ต) |
9 | 5, 8 | syl3an2 1164 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ (-๐ฆ ยท ๐) โ ๐ต) |
10 | 9 | adantr 481 |
. . . . 5
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (-๐ฆ ยท ๐) โ ๐ต) |
11 | | eqid 2732 |
. . . . . . . 8
โข
(invgโ๐บ) = (invgโ๐บ) |
12 | 6, 11 | grpinvcl 18871 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ โ ๐ต) โ ((invgโ๐บ)โ๐) โ ๐ต) |
13 | 12 | 3adant2 1131 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ ((invgโ๐บ)โ๐) โ ๐ต) |
14 | 13 | adantr 481 |
. . . . 5
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((invgโ๐บ)โ๐) โ ๐ต) |
15 | | mulgaddcom.p |
. . . . . 6
โข + =
(+gโ๐บ) |
16 | 6, 15 | grpass 18827 |
. . . . 5
โข ((๐บ โ Grp โง (๐ โ ๐ต โง (-๐ฆ ยท ๐) โ ๐ต โง ((invgโ๐บ)โ๐) โ ๐ต)) โ ((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) = (๐ + ((-๐ฆ ยท ๐) +
((invgโ๐บ)โ๐)))) |
17 | 2, 4, 10, 14, 16 | syl13anc 1372 |
. . . 4
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) = (๐ + ((-๐ฆ ยท ๐) +
((invgโ๐บ)โ๐)))) |
18 | 6, 7, 11 | mulgneg 18971 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ (-๐ฆ ยท ๐) = ((invgโ๐บ)โ(๐ฆ ยท ๐))) |
19 | 18 | adantr 481 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (-๐ฆ ยท ๐) = ((invgโ๐บ)โ(๐ฆ ยท ๐))) |
20 | 19 | oveq1d 7423 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((-๐ฆ ยท ๐) +
((invgโ๐บ)โ๐)) = (((invgโ๐บ)โ(๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐))) |
21 | 6, 7 | mulgcl 18970 |
. . . . . . . 8
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ (๐ฆ ยท ๐) โ ๐ต) |
22 | 21 | adantr 481 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (๐ฆ ยท ๐) โ ๐ต) |
23 | 6, 15, 11 | grpinvadd 18900 |
. . . . . . 7
โข ((๐บ โ Grp โง ๐ โ ๐ต โง (๐ฆ ยท ๐) โ ๐ต) โ ((invgโ๐บ)โ(๐ + (๐ฆ ยท ๐))) = (((invgโ๐บ)โ(๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐))) |
24 | 2, 4, 22, 23 | syl3anc 1371 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((invgโ๐บ)โ(๐ + (๐ฆ ยท ๐))) = (((invgโ๐บ)โ(๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐))) |
25 | 19 | oveq2d 7424 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐)) = (((invgโ๐บ)โ๐) +
((invgโ๐บ)โ(๐ฆ ยท ๐)))) |
26 | 6, 15, 11 | grpinvadd 18900 |
. . . . . . . 8
โข ((๐บ โ Grp โง (๐ฆ ยท ๐) โ ๐ต โง ๐ โ ๐ต) โ ((invgโ๐บ)โ((๐ฆ ยท ๐) + ๐)) = (((invgโ๐บ)โ๐) +
((invgโ๐บ)โ(๐ฆ ยท ๐)))) |
27 | 2, 22, 4, 26 | syl3anc 1371 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((invgโ๐บ)โ((๐ฆ ยท ๐) + ๐)) = (((invgโ๐บ)โ๐) +
((invgโ๐บ)โ(๐ฆ ยท ๐)))) |
28 | | fveq2 6891 |
. . . . . . . 8
โข (((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐)) โ ((invgโ๐บ)โ((๐ฆ ยท ๐) + ๐)) = ((invgโ๐บ)โ(๐ + (๐ฆ ยท ๐)))) |
29 | 28 | adantl 482 |
. . . . . . 7
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((invgโ๐บ)โ((๐ฆ ยท ๐) + ๐)) = ((invgโ๐บ)โ(๐ + (๐ฆ ยท ๐)))) |
30 | 25, 27, 29 | 3eqtr2rd 2779 |
. . . . . 6
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((invgโ๐บ)โ(๐ + (๐ฆ ยท ๐))) = (((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐))) |
31 | 20, 24, 30 | 3eqtr2d 2778 |
. . . . 5
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((-๐ฆ ยท ๐) +
((invgโ๐บ)โ๐)) = (((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐))) |
32 | 31 | oveq2d 7424 |
. . . 4
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (๐ + ((-๐ฆ ยท ๐) +
((invgโ๐บ)โ๐))) = (๐ +
(((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐)))) |
33 | 6, 15, 11 | grpasscan1 18885 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ ๐ต โง (-๐ฆ ยท ๐) โ ๐ต) โ (๐ +
(((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐))) = (-๐ฆ ยท ๐)) |
34 | 2, 4, 10, 33 | syl3anc 1371 |
. . . 4
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (๐ +
(((invgโ๐บ)โ๐) + (-๐ฆ ยท ๐))) = (-๐ฆ ยท ๐)) |
35 | 17, 32, 34 | 3eqtrd 2776 |
. . 3
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) = (-๐ฆ ยท ๐)) |
36 | 35 | oveq1d 7423 |
. 2
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) + ๐) = ((-๐ฆ ยท ๐) + ๐)) |
37 | 6, 15 | grpcl 18826 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ ๐ต โง (-๐ฆ ยท ๐) โ ๐ต) โ (๐ + (-๐ฆ ยท ๐)) โ ๐ต) |
38 | 1, 3, 9, 37 | syl3anc 1371 |
. . . 4
โข ((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โ (๐ + (-๐ฆ ยท ๐)) โ ๐ต) |
39 | 38 | adantr 481 |
. . 3
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (๐ + (-๐ฆ ยท ๐)) โ ๐ต) |
40 | 6, 15, 11 | grpasscan2 18886 |
. . 3
โข ((๐บ โ Grp โง (๐ + (-๐ฆ ยท ๐)) โ ๐ต โง ๐ โ ๐ต) โ (((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) + ๐) = (๐ + (-๐ฆ ยท ๐))) |
41 | 2, 39, 4, 40 | syl3anc 1371 |
. 2
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ (((๐ + (-๐ฆ ยท ๐)) +
((invgโ๐บ)โ๐)) + ๐) = (๐ + (-๐ฆ ยท ๐))) |
42 | 36, 41 | eqtr3d 2774 |
1
โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((-๐ฆ ยท ๐) + ๐) = (๐ + (-๐ฆ ยท ๐))) |