Step |
Hyp |
Ref |
Expression |
1 |
|
imasaddf.f |
โข ( ๐ โ ๐น : ๐ โontoโ ๐ต ) |
2 |
|
imasaddf.e |
โข ( ( ๐ โง ( ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ( ( ๐น โ ๐ ) = ( ๐น โ ๐ ) โง ( ๐น โ ๐ ) = ( ๐น โ ๐ ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
3 |
|
imasaddf.u |
โข ( ๐ โ ๐ = ( ๐น โs ๐
) ) |
4 |
|
imasaddf.v |
โข ( ๐ โ ๐ = ( Base โ ๐
) ) |
5 |
|
imasaddf.r |
โข ( ๐ โ ๐
โ ๐ ) |
6 |
|
imasmulf.p |
โข ยท = ( .r โ ๐
) |
7 |
|
imasmulf.a |
โข โ = ( .r โ ๐ ) |
8 |
3 4 1 5 6 7
|
imasmulr |
โข ( ๐ โ โ = โช ๐ โ ๐ โช ๐ โ ๐ { โจ โจ ( ๐น โ ๐ ) , ( ๐น โ ๐ ) โฉ , ( ๐น โ ( ๐ ยท ๐ ) ) โฉ } ) |
9 |
1 2 8
|
imasaddfnlem |
โข ( ๐ โ โ Fn ( ๐ต ร ๐ต ) ) |