Step | Hyp | Ref
| Expression |
1 | | ghmmhm 19019 |
. . . . . 6
โข (๐น โ (๐บ GrpHom ๐ป) โ ๐น โ (๐บ MndHom ๐ป)) |
2 | | ghmmulg.b |
. . . . . . 7
โข ๐ต = (Baseโ๐บ) |
3 | | ghmmulg.s |
. . . . . . 7
โข ยท =
(.gโ๐บ) |
4 | | ghmmulg.t |
. . . . . . 7
โข ร =
(.gโ๐ป) |
5 | 2, 3, 4 | mhmmulg 18918 |
. . . . . 6
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
6 | 1, 5 | syl3an1 1164 |
. . . . 5
โข ((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
7 | 6 | 3expa 1119 |
. . . 4
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
8 | 7 | an32s 651 |
. . 3
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
9 | 8 | 3adantl2 1168 |
. 2
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
10 | | simpl1 1192 |
. . . . . . . 8
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐น โ (๐บ GrpHom ๐ป)) |
11 | 10, 1 | syl 17 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐น โ (๐บ MndHom ๐ป)) |
12 | | nnnn0 12421 |
. . . . . . . 8
โข (-๐ โ โ โ -๐ โ
โ0) |
13 | 12 | ad2antll 728 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ
โ0) |
14 | | simpl3 1194 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ ๐ต) |
15 | 2, 3, 4 | mhmmulg 18918 |
. . . . . . 7
โข ((๐น โ (๐บ MndHom ๐ป) โง -๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(-๐ ยท ๐)) = (-๐ ร (๐นโ๐))) |
16 | 11, 13, 14, 15 | syl3anc 1372 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ(-๐ ยท ๐)) = (-๐ ร (๐นโ๐))) |
17 | 16 | fveq2d 6847 |
. . . . 5
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ
((invgโ๐ป)โ(๐นโ(-๐ ยท ๐))) = ((invgโ๐ป)โ(-๐ ร (๐นโ๐)))) |
18 | | ghmgrp1 19011 |
. . . . . . . 8
โข (๐น โ (๐บ GrpHom ๐ป) โ ๐บ โ Grp) |
19 | 10, 18 | syl 17 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐บ โ Grp) |
20 | | nnz 12521 |
. . . . . . . 8
โข (-๐ โ โ โ -๐ โ
โค) |
21 | 20 | ad2antll 728 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ โค) |
22 | 2, 3 | mulgcl 18894 |
. . . . . . 7
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) โ ๐ต) |
23 | 19, 21, 14, 22 | syl3anc 1372 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (-๐ ยท ๐) โ ๐ต) |
24 | | eqid 2737 |
. . . . . . 7
โข
(invgโ๐บ) = (invgโ๐บ) |
25 | | eqid 2737 |
. . . . . . 7
โข
(invgโ๐ป) = (invgโ๐ป) |
26 | 2, 24, 25 | ghminv 19016 |
. . . . . 6
โข ((๐น โ (๐บ GrpHom ๐ป) โง (-๐ ยท ๐) โ ๐ต) โ (๐นโ((invgโ๐บ)โ(-๐ ยท ๐))) = ((invgโ๐ป)โ(๐นโ(-๐ ยท ๐)))) |
27 | 10, 23, 26 | syl2anc 585 |
. . . . 5
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ((invgโ๐บ)โ(-๐ ยท ๐))) = ((invgโ๐ป)โ(๐นโ(-๐ ยท ๐)))) |
28 | | ghmgrp2 19012 |
. . . . . . 7
โข (๐น โ (๐บ GrpHom ๐ป) โ ๐ป โ Grp) |
29 | 10, 28 | syl 17 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐ป โ Grp) |
30 | | eqid 2737 |
. . . . . . . . 9
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
31 | 2, 30 | ghmf 19013 |
. . . . . . . 8
โข (๐น โ (๐บ GrpHom ๐ป) โ ๐น:๐ตโถ(Baseโ๐ป)) |
32 | 10, 31 | syl 17 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐น:๐ตโถ(Baseโ๐ป)) |
33 | 32, 14 | ffvelcdmd 7037 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ๐) โ (Baseโ๐ป)) |
34 | 30, 4, 25 | mulgneg 18895 |
. . . . . 6
โข ((๐ป โ Grp โง -๐ โ โค โง (๐นโ๐) โ (Baseโ๐ป)) โ (--๐ ร (๐นโ๐)) = ((invgโ๐ป)โ(-๐ ร (๐นโ๐)))) |
35 | 29, 21, 33, 34 | syl3anc 1372 |
. . . . 5
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (--๐ ร (๐นโ๐)) = ((invgโ๐ป)โ(-๐ ร (๐นโ๐)))) |
36 | 17, 27, 35 | 3eqtr4d 2787 |
. . . 4
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ((invgโ๐บ)โ(-๐ ยท ๐))) = (--๐ ร (๐นโ๐))) |
37 | 2, 3, 24 | mulgneg 18895 |
. . . . . . 7
โข ((๐บ โ Grp โง -๐ โ โค โง ๐ โ ๐ต) โ (--๐ ยท ๐) = ((invgโ๐บ)โ(-๐ ยท ๐))) |
38 | 19, 21, 14, 37 | syl3anc 1372 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (--๐ ยท ๐) = ((invgโ๐บ)โ(-๐ ยท ๐))) |
39 | | simprl 770 |
. . . . . . . . 9
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
40 | 39 | recnd 11184 |
. . . . . . . 8
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ โ) |
41 | 40 | negnegd 11504 |
. . . . . . 7
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ --๐ = ๐) |
42 | 41 | oveq1d 7373 |
. . . . . 6
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (--๐ ยท ๐) = (๐ ยท ๐)) |
43 | 38, 42 | eqtr3d 2779 |
. . . . 5
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ
((invgโ๐บ)โ(-๐ ยท ๐)) = (๐ ยท ๐)) |
44 | 43 | fveq2d 6847 |
. . . 4
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ((invgโ๐บ)โ(-๐ ยท ๐))) = (๐นโ(๐ ยท ๐))) |
45 | 36, 44 | eqtr3d 2779 |
. . 3
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (--๐ ร (๐นโ๐)) = (๐นโ(๐ ยท ๐))) |
46 | 41 | oveq1d 7373 |
. . 3
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (--๐ ร (๐นโ๐)) = (๐ ร (๐นโ๐))) |
47 | 45, 46 | eqtr3d 2779 |
. 2
โข (((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ โ โ โง -๐ โ โ)) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
48 | | simp2 1138 |
. . 3
โข ((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โ ๐ โ โค) |
49 | | elznn0nn 12514 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ
โ))) |
50 | 48, 49 | sylib 217 |
. 2
โข ((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ โ โ0 โจ (๐ โ โ โง -๐ โ
โ))) |
51 | 9, 47, 50 | mpjaodan 958 |
1
โข ((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |