Step | Hyp | Ref
| Expression |
1 | | ringlghm.b |
. 2
โข ๐ต = (Baseโ๐
) |
2 | | eqid 2733 |
. 2
โข
(+gโ๐
) = (+gโ๐
) |
3 | | ringgrp 19977 |
. . 3
โข (๐
โ Ring โ ๐
โ Grp) |
4 | 3 | adantr 482 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Grp) |
5 | | ringlghm.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
6 | 1, 5 | ringcl 19989 |
. . . . 5
โข ((๐
โ Ring โง ๐ฅ โ ๐ต โง ๐ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
7 | 6 | 3expa 1119 |
. . . 4
โข (((๐
โ Ring โง ๐ฅ โ ๐ต) โง ๐ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
8 | 7 | an32s 651 |
. . 3
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
9 | 8 | fmpttd 7067 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)):๐ตโถ๐ต) |
10 | | df-3an 1090 |
. . . . 5
โข ((๐ฆ โ ๐ต โง ๐ง โ ๐ต โง ๐ โ ๐ต) โ ((๐ฆ โ ๐ต โง ๐ง โ ๐ต) โง ๐ โ ๐ต)) |
11 | 1, 2, 5 | ringdir 19996 |
. . . . 5
โข ((๐
โ Ring โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต โง ๐ โ ๐ต)) โ ((๐ฆ(+gโ๐
)๐ง) ยท ๐) = ((๐ฆ ยท ๐)(+gโ๐
)(๐ง ยท ๐))) |
12 | 10, 11 | sylan2br 596 |
. . . 4
โข ((๐
โ Ring โง ((๐ฆ โ ๐ต โง ๐ง โ ๐ต) โง ๐ โ ๐ต)) โ ((๐ฆ(+gโ๐
)๐ง) ยท ๐) = ((๐ฆ ยท ๐)(+gโ๐
)(๐ง ยท ๐))) |
13 | 12 | anass1rs 654 |
. . 3
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฆ(+gโ๐
)๐ง) ยท ๐) = ((๐ฆ ยท ๐)(+gโ๐
)(๐ง ยท ๐))) |
14 | 1, 2 | ringacl 20007 |
. . . . . 6
โข ((๐
โ Ring โง ๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (๐ฆ(+gโ๐
)๐ง) โ ๐ต) |
15 | 14 | 3expb 1121 |
. . . . 5
โข ((๐
โ Ring โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฆ(+gโ๐
)๐ง) โ ๐ต) |
16 | 15 | adantlr 714 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (๐ฆ(+gโ๐
)๐ง) โ ๐ต) |
17 | | oveq1 7368 |
. . . . 5
โข (๐ฅ = (๐ฆ(+gโ๐
)๐ง) โ (๐ฅ ยท ๐) = ((๐ฆ(+gโ๐
)๐ง) ยท ๐)) |
18 | | eqid 2733 |
. . . . 5
โข (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) = (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) |
19 | | ovex 7394 |
. . . . 5
โข ((๐ฆ(+gโ๐
)๐ง) ยท ๐) โ V |
20 | 17, 18, 19 | fvmpt 6952 |
. . . 4
โข ((๐ฆ(+gโ๐
)๐ง) โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐ฆ(+gโ๐
)๐ง)) = ((๐ฆ(+gโ๐
)๐ง) ยท ๐)) |
21 | 16, 20 | syl 17 |
. . 3
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐ฆ(+gโ๐
)๐ง)) = ((๐ฆ(+gโ๐
)๐ง) ยท ๐)) |
22 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐) = (๐ฆ ยท ๐)) |
23 | | ovex 7394 |
. . . . . 6
โข (๐ฆ ยท ๐) โ V |
24 | 22, 18, 23 | fvmpt 6952 |
. . . . 5
โข (๐ฆ โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ฆ) = (๐ฆ ยท ๐)) |
25 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = ๐ง โ (๐ฅ ยท ๐) = (๐ง ยท ๐)) |
26 | | ovex 7394 |
. . . . . 6
โข (๐ง ยท ๐) โ V |
27 | 25, 18, 26 | fvmpt 6952 |
. . . . 5
โข (๐ง โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ง) = (๐ง ยท ๐)) |
28 | 24, 27 | oveqan12d 7380 |
. . . 4
โข ((๐ฆ โ ๐ต โง ๐ง โ ๐ต) โ (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ฆ)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ง)) = ((๐ฆ ยท ๐)(+gโ๐
)(๐ง ยท ๐))) |
29 | 28 | adantl 483 |
. . 3
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ฆ)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ง)) = ((๐ฆ ยท ๐)(+gโ๐
)(๐ง ยท ๐))) |
30 | 13, 21, 29 | 3eqtr4d 2783 |
. 2
โข (((๐
โ Ring โง ๐ โ ๐ต) โง (๐ฆ โ ๐ต โง ๐ง โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐ฆ(+gโ๐
)๐ง)) = (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ฆ)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐ง))) |
31 | 1, 1, 2, 2, 4, 4, 9, 30 | isghmd 19025 |
1
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) โ (๐
GrpHom ๐
)) |