Step | Hyp | Ref
| Expression |
1 | | ringsubdi.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
2 | | ringsubdi.x |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
3 | | ringsubdi.y |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
4 | | ringgrp 13238 |
. . . . . 6
โข (๐
โ Ring โ ๐
โ Grp) |
5 | 1, 4 | syl 14 |
. . . . 5
โข (๐ โ ๐
โ Grp) |
6 | | ringsubdi.z |
. . . . 5
โข (๐ โ ๐ โ ๐ต) |
7 | | ringsubdi.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
8 | | eqid 2187 |
. . . . . 6
โข
(invgโ๐
) = (invgโ๐
) |
9 | 7, 8 | grpinvcl 12942 |
. . . . 5
โข ((๐
โ Grp โง ๐ โ ๐ต) โ ((invgโ๐
)โ๐) โ ๐ต) |
10 | 5, 6, 9 | syl2anc 411 |
. . . 4
โข (๐ โ
((invgโ๐
)โ๐) โ ๐ต) |
11 | | eqid 2187 |
. . . . 5
โข
(+gโ๐
) = (+gโ๐
) |
12 | | ringsubdi.t |
. . . . 5
โข ยท =
(.rโ๐
) |
13 | 7, 11, 12 | ringdi 13255 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ((invgโ๐
)โ๐) โ ๐ต)) โ (๐ ยท (๐(+gโ๐
)((invgโ๐
)โ๐))) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท
((invgโ๐
)โ๐)))) |
14 | 1, 2, 3, 10, 13 | syl13anc 1250 |
. . 3
โข (๐ โ (๐ ยท (๐(+gโ๐
)((invgโ๐
)โ๐))) = ((๐ ยท ๐)(+gโ๐
)(๐ ยท
((invgโ๐
)โ๐)))) |
15 | 7, 12, 8, 1, 2, 6 | ringmneg2 13289 |
. . . 4
โข (๐ โ (๐ ยท
((invgโ๐
)โ๐)) = ((invgโ๐
)โ(๐ ยท ๐))) |
16 | 15 | oveq2d 5904 |
. . 3
โข (๐ โ ((๐ ยท ๐)(+gโ๐
)(๐ ยท
((invgโ๐
)โ๐))) = ((๐ ยท ๐)(+gโ๐
)((invgโ๐
)โ(๐ ยท ๐)))) |
17 | 14, 16 | eqtrd 2220 |
. 2
โข (๐ โ (๐ ยท (๐(+gโ๐
)((invgโ๐
)โ๐))) = ((๐ ยท ๐)(+gโ๐
)((invgโ๐
)โ(๐ ยท ๐)))) |
18 | | ringsubdi.m |
. . . . 5
โข โ =
(-gโ๐
) |
19 | 7, 11, 8, 18 | grpsubval 12940 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐(+gโ๐
)((invgโ๐
)โ๐))) |
20 | 3, 6, 19 | syl2anc 411 |
. . 3
โข (๐ โ (๐ โ ๐) = (๐(+gโ๐
)((invgโ๐
)โ๐))) |
21 | 20 | oveq2d 5904 |
. 2
โข (๐ โ (๐ ยท (๐ โ ๐)) = (๐ ยท (๐(+gโ๐
)((invgโ๐
)โ๐)))) |
22 | 7, 12 | ringcl 13250 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
23 | 1, 2, 3, 22 | syl3anc 1248 |
. . 3
โข (๐ โ (๐ ยท ๐) โ ๐ต) |
24 | 7, 12 | ringcl 13250 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
25 | 1, 2, 6, 24 | syl3anc 1248 |
. . 3
โข (๐ โ (๐ ยท ๐) โ ๐ต) |
26 | 7, 11, 8, 18 | grpsubval 12940 |
. . 3
โข (((๐ ยท ๐) โ ๐ต โง (๐ ยท ๐) โ ๐ต) โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐
)((invgโ๐
)โ(๐ ยท ๐)))) |
27 | 23, 25, 26 | syl2anc 411 |
. 2
โข (๐ โ ((๐ ยท ๐) โ (๐ ยท ๐)) = ((๐ ยท ๐)(+gโ๐
)((invgโ๐
)โ(๐ ยท ๐)))) |
28 | 17, 21, 27 | 3eqtr4d 2230 |
1
โข (๐ โ (๐ ยท (๐ โ ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) |