Step |
Hyp |
Ref |
Expression |
1 |
|
ringneglmul.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
ringneglmul.t |
โข ยท = ( .r โ ๐
) |
3 |
|
ringneglmul.n |
โข ๐ = ( invg โ ๐
) |
4 |
|
ringneglmul.r |
โข ( ๐ โ ๐
โ Ring ) |
5 |
|
ringneglmul.x |
โข ( ๐ โ ๐ โ ๐ต ) |
6 |
|
ringneglmul.y |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
ringgrp |
โข ( ๐
โ Ring โ ๐
โ Grp ) |
8 |
4 7
|
syl |
โข ( ๐ โ ๐
โ Grp ) |
9 |
|
eqid |
โข ( 1r โ ๐
) = ( 1r โ ๐
) |
10 |
1 9
|
ringidcl |
โข ( ๐
โ Ring โ ( 1r โ ๐
) โ ๐ต ) |
11 |
4 10
|
syl |
โข ( ๐ โ ( 1r โ ๐
) โ ๐ต ) |
12 |
1 3
|
grpinvcl |
โข ( ( ๐
โ Grp โง ( 1r โ ๐
) โ ๐ต ) โ ( ๐ โ ( 1r โ ๐
) ) โ ๐ต ) |
13 |
8 11 12
|
syl2anc |
โข ( ๐ โ ( ๐ โ ( 1r โ ๐
) ) โ ๐ต ) |
14 |
1 2
|
ringass |
โข ( ( ๐
โ Ring โง ( ( ๐ โ ( 1r โ ๐
) ) โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ( ( ๐ โ ( 1r โ ๐
) ) ยท ๐ ) ยท ๐ ) = ( ( ๐ โ ( 1r โ ๐
) ) ยท ( ๐ ยท ๐ ) ) ) |
15 |
4 13 5 6 14
|
syl13anc |
โข ( ๐ โ ( ( ( ๐ โ ( 1r โ ๐
) ) ยท ๐ ) ยท ๐ ) = ( ( ๐ โ ( 1r โ ๐
) ) ยท ( ๐ ยท ๐ ) ) ) |
16 |
1 2 9 3 4 5
|
ringnegl |
โข ( ๐ โ ( ( ๐ โ ( 1r โ ๐
) ) ยท ๐ ) = ( ๐ โ ๐ ) ) |
17 |
16
|
oveq1d |
โข ( ๐ โ ( ( ( ๐ โ ( 1r โ ๐
) ) ยท ๐ ) ยท ๐ ) = ( ( ๐ โ ๐ ) ยท ๐ ) ) |
18 |
1 2
|
ringcl |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต ) โ ( ๐ ยท ๐ ) โ ๐ต ) |
19 |
4 5 6 18
|
syl3anc |
โข ( ๐ โ ( ๐ ยท ๐ ) โ ๐ต ) |
20 |
1 2 9 3 4 19
|
ringnegl |
โข ( ๐ โ ( ( ๐ โ ( 1r โ ๐
) ) ยท ( ๐ ยท ๐ ) ) = ( ๐ โ ( ๐ ยท ๐ ) ) ) |
21 |
15 17 20
|
3eqtr3d |
โข ( ๐ โ ( ( ๐ โ ๐ ) ยท ๐ ) = ( ๐ โ ( ๐ ยท ๐ ) ) ) |