Step | Hyp | Ref
| Expression |
1 | | mulgmhm.b |
. 2
โข ๐ต = (Baseโ๐บ) |
2 | | eqid 2737 |
. 2
โข
(+gโ๐บ) = (+gโ๐บ) |
3 | | ablgrp 19574 |
. . 3
โข (๐บ โ Abel โ ๐บ โ Grp) |
4 | 3 | adantr 482 |
. 2
โข ((๐บ โ Abel โง ๐ โ โค) โ ๐บ โ Grp) |
5 | | mulgmhm.m |
. . . . . 6
โข ยท =
(.gโ๐บ) |
6 | 1, 5 | mulgcl 18900 |
. . . . 5
โข ((๐บ โ Grp โง ๐ โ โค โง ๐ฅ โ ๐ต) โ (๐ ยท ๐ฅ) โ ๐ต) |
7 | 3, 6 | syl3an1 1164 |
. . . 4
โข ((๐บ โ Abel โง ๐ โ โค โง ๐ฅ โ ๐ต) โ (๐ ยท ๐ฅ) โ ๐ต) |
8 | 7 | 3expa 1119 |
. . 3
โข (((๐บ โ Abel โง ๐ โ โค) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐ฅ) โ ๐ต) |
9 | 8 | fmpttd 7068 |
. 2
โข ((๐บ โ Abel โง ๐ โ โค) โ (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)):๐ตโถ๐ต) |
10 | | 3anass 1096 |
. . . . 5
โข ((๐ โ โค โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (๐ โ โค โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต))) |
11 | 1, 5, 2 | mulgdi 19612 |
. . . . 5
โข ((๐บ โ Abel โง (๐ โ โค โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ ยท (๐ฆ(+gโ๐บ)๐ง)) = ((๐ ยท ๐ฆ)(+gโ๐บ)(๐ ยท ๐ง))) |
12 | 10, 11 | sylan2br 596 |
. . . 4
โข ((๐บ โ Abel โง (๐ โ โค โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต))) โ (๐ ยท (๐ฆ(+gโ๐บ)๐ง)) = ((๐ ยท ๐ฆ)(+gโ๐บ)(๐ ยท ๐ง))) |
13 | 12 | anassrs 469 |
. . 3
โข (((๐บ โ Abel โง ๐ โ โค) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ ยท (๐ฆ(+gโ๐บ)๐ง)) = ((๐ ยท ๐ฆ)(+gโ๐บ)(๐ ยท ๐ง))) |
14 | 1, 2 | grpcl 18763 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (๐ฆ(+gโ๐บ)๐ง) โ ๐ต) |
15 | 14 | 3expb 1121 |
. . . . 5
โข ((๐บ โ Grp โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฆ(+gโ๐บ)๐ง) โ ๐ต) |
16 | 4, 15 | sylan 581 |
. . . 4
โข (((๐บ โ Abel โง ๐ โ โค) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฆ(+gโ๐บ)๐ง) โ ๐ต) |
17 | | oveq2 7370 |
. . . . 5
โข (๐ฅ = (๐ฆ(+gโ๐บ)๐ง) โ (๐ ยท ๐ฅ) = (๐ ยท (๐ฆ(+gโ๐บ)๐ง))) |
18 | | eqid 2737 |
. . . . 5
โข (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) = (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) |
19 | | ovex 7395 |
. . . . 5
โข (๐ ยท (๐ฆ(+gโ๐บ)๐ง)) โ V |
20 | 17, 18, 19 | fvmpt 6953 |
. . . 4
โข ((๐ฆ(+gโ๐บ)๐ง) โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ(๐ฆ(+gโ๐บ)๐ง)) = (๐ ยท (๐ฆ(+gโ๐บ)๐ง))) |
21 | 16, 20 | syl 17 |
. . 3
โข (((๐บ โ Abel โง ๐ โ โค) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ(๐ฆ(+gโ๐บ)๐ง)) = (๐ ยท (๐ฆ(+gโ๐บ)๐ง))) |
22 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ ยท ๐ฅ) = (๐ ยท ๐ฆ)) |
23 | | ovex 7395 |
. . . . . 6
โข (๐ ยท ๐ฆ) โ V |
24 | 22, 18, 23 | fvmpt 6953 |
. . . . 5
โข (๐ฆ โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ฆ) = (๐ ยท ๐ฆ)) |
25 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ง โ (๐ ยท ๐ฅ) = (๐ ยท ๐ง)) |
26 | | ovex 7395 |
. . . . . 6
โข (๐ ยท ๐ง) โ V |
27 | 25, 18, 26 | fvmpt 6953 |
. . . . 5
โข (๐ง โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ง) = (๐ ยท ๐ง)) |
28 | 24, 27 | oveqan12d 7381 |
. . . 4
โข ((๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ฆ)(+gโ๐บ)((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ง)) = ((๐ ยท ๐ฆ)(+gโ๐บ)(๐ ยท ๐ง))) |
29 | 28 | adantl 483 |
. . 3
โข (((๐บ โ Abel โง ๐ โ โค) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ฆ)(+gโ๐บ)((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ง)) = ((๐ ยท ๐ฆ)(+gโ๐บ)(๐ ยท ๐ง))) |
30 | 13, 21, 29 | 3eqtr4d 2787 |
. 2
โข (((๐บ โ Abel โง ๐ โ โค) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ(๐ฆ(+gโ๐บ)๐ง)) = (((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ฆ)(+gโ๐บ)((๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ))โ๐ง))) |
31 | 1, 1, 2, 2, 4, 4, 9, 30 | isghmd 19024 |
1
โข ((๐บ โ Abel โง ๐ โ โค) โ (๐ฅ โ ๐ต โฆ (๐ ยท ๐ฅ)) โ (๐บ GrpHom ๐บ)) |