Step | Hyp | Ref
| Expression |
1 | | srgmnd 20092 |
. . . 4
โข (๐
โ SRing โ ๐
โ Mnd) |
2 | 1, 1 | jca 511 |
. . 3
โข (๐
โ SRing โ (๐
โ Mnd โง ๐
โ Mnd)) |
3 | 2 | adantr 480 |
. 2
โข ((๐
โ SRing โง ๐ โ ๐ต) โ (๐
โ Mnd โง ๐
โ Mnd)) |
4 | | srglmhm.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
5 | | srglmhm.t |
. . . . . . 7
โข ยท =
(.rโ๐
) |
6 | 4, 5 | srgcl 20095 |
. . . . . 6
โข ((๐
โ SRing โง ๐ฅ โ ๐ต โง ๐ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
7 | 6 | 3com23 1123 |
. . . . 5
โข ((๐
โ SRing โง ๐ โ ๐ต โง ๐ฅ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
8 | 7 | 3expa 1115 |
. . . 4
โข (((๐
โ SRing โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ฅ ยท ๐) โ ๐ต) |
9 | 8 | fmpttd 7109 |
. . 3
โข ((๐
โ SRing โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)):๐ตโถ๐ต) |
10 | | 3anrot 1097 |
. . . . . . . 8
โข ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) |
11 | | 3anass 1092 |
. . . . . . . 8
โข ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐ต โง (๐ โ ๐ต โง ๐ โ ๐ต))) |
12 | 10, 11 | bitr3i 277 |
. . . . . . 7
โข ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐ต โง (๐ โ ๐ต โง ๐ โ ๐ต))) |
13 | | eqid 2726 |
. . . . . . . 8
โข
(+gโ๐
) = (+gโ๐
) |
14 | 4, 13, 5 | srgdir 20100 |
. . . . . . 7
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(+gโ๐
)๐) ยท ๐) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท ๐))) |
15 | 12, 14 | sylan2br 594 |
. . . . . 6
โข ((๐
โ SRing โง (๐ โ ๐ต โง (๐ โ ๐ต โง ๐ โ ๐ต))) โ ((๐(+gโ๐
)๐) ยท ๐) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท ๐))) |
16 | 15 | anassrs 467 |
. . . . 5
โข (((๐
โ SRing โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(+gโ๐
)๐) ยท ๐) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท ๐))) |
17 | 4, 13 | srgacl 20107 |
. . . . . . . 8
โข ((๐
โ SRing โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(+gโ๐
)๐) โ ๐ต) |
18 | 17 | 3expb 1117 |
. . . . . . 7
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(+gโ๐
)๐) โ ๐ต) |
19 | 18 | adantlr 712 |
. . . . . 6
โข (((๐
โ SRing โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(+gโ๐
)๐) โ ๐ต) |
20 | | oveq1 7411 |
. . . . . . 7
โข (๐ฅ = (๐(+gโ๐
)๐) โ (๐ฅ ยท ๐) = ((๐(+gโ๐
)๐) ยท ๐)) |
21 | | eqid 2726 |
. . . . . . 7
โข (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) = (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) |
22 | | ovex 7437 |
. . . . . . 7
โข ((๐(+gโ๐
)๐) ยท ๐) โ V |
23 | 20, 21, 22 | fvmpt 6991 |
. . . . . 6
โข ((๐(+gโ๐
)๐) โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = ((๐(+gโ๐
)๐) ยท ๐)) |
24 | 19, 23 | syl 17 |
. . . . 5
โข (((๐
โ SRing โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = ((๐(+gโ๐
)๐) ยท ๐)) |
25 | | oveq1 7411 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐) = (๐ ยท ๐)) |
26 | | ovex 7437 |
. . . . . . . 8
โข (๐ ยท ๐) โ V |
27 | 25, 21, 26 | fvmpt 6991 |
. . . . . . 7
โข (๐ โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐) = (๐ ยท ๐)) |
28 | | oveq1 7411 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅ ยท ๐) = (๐ ยท ๐)) |
29 | | ovex 7437 |
. . . . . . . 8
โข (๐ ยท ๐) โ V |
30 | 28, 21, 29 | fvmpt 6991 |
. . . . . . 7
โข (๐ โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐) = (๐ ยท ๐)) |
31 | 27, 30 | oveqan12d 7423 |
. . . . . 6
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท ๐))) |
32 | 31 | adantl 481 |
. . . . 5
โข (((๐
โ SRing โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท ๐))) |
33 | 16, 24, 32 | 3eqtr4d 2776 |
. . . 4
โข (((๐
โ SRing โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐))) |
34 | 33 | ralrimivva 3194 |
. . 3
โข ((๐
โ SRing โง ๐ โ ๐ต) โ โ๐ โ ๐ต โ๐ โ ๐ต ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐))) |
35 | | eqid 2726 |
. . . . . . 7
โข
(0gโ๐
) = (0gโ๐
) |
36 | 4, 35 | srg0cl 20102 |
. . . . . 6
โข (๐
โ SRing โ
(0gโ๐
)
โ ๐ต) |
37 | 36 | adantr 480 |
. . . . 5
โข ((๐
โ SRing โง ๐ โ ๐ต) โ (0gโ๐
) โ ๐ต) |
38 | | oveq1 7411 |
. . . . . 6
โข (๐ฅ = (0gโ๐
) โ (๐ฅ ยท ๐) = ((0gโ๐
) ยท ๐)) |
39 | | ovex 7437 |
. . . . . 6
โข
((0gโ๐
) ยท ๐) โ V |
40 | 38, 21, 39 | fvmpt 6991 |
. . . . 5
โข
((0gโ๐
) โ ๐ต โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(0gโ๐
)) = ((0gโ๐
) ยท ๐)) |
41 | 37, 40 | syl 17 |
. . . 4
โข ((๐
โ SRing โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(0gโ๐
)) = ((0gโ๐
) ยท ๐)) |
42 | 4, 5, 35 | srglz 20110 |
. . . 4
โข ((๐
โ SRing โง ๐ โ ๐ต) โ ((0gโ๐
) ยท ๐) = (0gโ๐
)) |
43 | 41, 42 | eqtrd 2766 |
. . 3
โข ((๐
โ SRing โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(0gโ๐
)) = (0gโ๐
)) |
44 | 9, 34, 43 | 3jca 1125 |
. 2
โข ((๐
โ SRing โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)):๐ตโถ๐ต โง โ๐ โ ๐ต โ๐ โ ๐ต ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)) โง ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(0gโ๐
)) = (0gโ๐
))) |
45 | 4, 4, 13, 13, 35, 35 | ismhm 18712 |
. 2
โข ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) โ (๐
MndHom ๐
) โ ((๐
โ Mnd โง ๐
โ Mnd) โง ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)):๐ตโถ๐ต โง โ๐ โ ๐ต โ๐ โ ๐ต ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(๐(+gโ๐
)๐)) = (((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)(+gโ๐
)((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ๐)) โง ((๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐))โ(0gโ๐
)) = (0gโ๐
)))) |
46 | 3, 44, 45 | sylanbrc 582 |
1
โข ((๐
โ SRing โง ๐ โ ๐ต) โ (๐ฅ โ ๐ต โฆ (๐ฅ ยท ๐)) โ (๐
MndHom ๐
)) |