Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
โข
(opprโ๐
) = (opprโ๐
) |
2 | 1 | opprring 20068 |
. . . . 5
โข (๐
โ Ring โ
(opprโ๐
) โ Ring) |
3 | 2 | adantr 482 |
. . . 4
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ
(opprโ๐
) โ Ring) |
4 | | simpr1 1195 |
. . . 4
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ โค) |
5 | | simpr3 1197 |
. . . 4
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
6 | | simpr2 1196 |
. . . 4
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
7 | | mulgass3.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
8 | 1, 7 | opprbas 20064 |
. . . . 5
โข ๐ต =
(Baseโ(opprโ๐
)) |
9 | | eqid 2733 |
. . . . 5
โข
(.gโ(opprโ๐
)) =
(.gโ(opprโ๐
)) |
10 | | eqid 2733 |
. . . . 5
โข
(.rโ(opprโ๐
)) =
(.rโ(opprโ๐
)) |
11 | 8, 9, 10 | mulgass2 20033 |
. . . 4
โข
(((opprโ๐
) โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(.gโ(opprโ๐
))๐)(.rโ(opprโ๐
))๐) = (๐(.gโ(opprโ๐
))(๐(.rโ(opprโ๐
))๐))) |
12 | 3, 4, 5, 6, 11 | syl13anc 1373 |
. . 3
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(.gโ(opprโ๐
))๐)(.rโ(opprโ๐
))๐) = (๐(.gโ(opprโ๐
))(๐(.rโ(opprโ๐
))๐))) |
13 | | mulgass3.t |
. . . 4
โข ร =
(.rโ๐
) |
14 | 7, 13, 1, 10 | opprmul 20060 |
. . 3
โข ((๐(.gโ(opprโ๐
))๐)(.rโ(opprโ๐
))๐) = (๐ ร (๐(.gโ(opprโ๐
))๐)) |
15 | 7, 13, 1, 10 | opprmul 20060 |
. . . 4
โข (๐(.rโ(opprโ๐
))๐) = (๐ ร ๐) |
16 | 15 | oveq2i 7372 |
. . 3
โข (๐(.gโ(opprโ๐
))(๐(.rโ(opprโ๐
))๐)) = (๐(.gโ(opprโ๐
))(๐ ร ๐)) |
17 | 12, 14, 16 | 3eqtr3g 2796 |
. 2
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ร (๐(.gโ(opprโ๐
))๐)) = (๐(.gโ(opprโ๐
))(๐ ร ๐))) |
18 | | mulgass3.m |
. . . . 5
โข ยท =
(.gโ๐
) |
19 | 7 | a1i 11 |
. . . . 5
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ต = (Baseโ๐
)) |
20 | 8 | a1i 11 |
. . . . 5
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ต =
(Baseโ(opprโ๐
))) |
21 | | ssv 3972 |
. . . . . 6
โข ๐ต โ V |
22 | 21 | a1i 11 |
. . . . 5
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ต โ V) |
23 | | ovexd 7396 |
. . . . 5
โข (((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ V โง ๐ฆ โ V)) โ (๐ฅ(+gโ๐
)๐ฆ) โ V) |
24 | | eqid 2733 |
. . . . . . . 8
โข
(+gโ๐
) = (+gโ๐
) |
25 | 1, 24 | oppradd 20066 |
. . . . . . 7
โข
(+gโ๐
) =
(+gโ(opprโ๐
)) |
26 | 25 | oveqi 7374 |
. . . . . 6
โข (๐ฅ(+gโ๐
)๐ฆ) = (๐ฅ(+gโ(opprโ๐
))๐ฆ) |
27 | 26 | a1i 11 |
. . . . 5
โข (((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ V โง ๐ฆ โ V)) โ (๐ฅ(+gโ๐
)๐ฆ) = (๐ฅ(+gโ(opprโ๐
))๐ฆ)) |
28 | 18, 9, 19, 20, 22, 23, 27 | mulgpropd 18926 |
. . . 4
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ยท =
(.gโ(opprโ๐
))) |
29 | 28 | oveqd 7378 |
. . 3
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) = (๐(.gโ(opprโ๐
))๐)) |
30 | 29 | oveq2d 7377 |
. 2
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ร (๐ ยท ๐)) = (๐ ร (๐(.gโ(opprโ๐
))๐))) |
31 | 28 | oveqd 7378 |
. 2
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ ร ๐)) = (๐(.gโ(opprโ๐
))(๐ ร ๐))) |
32 | 17, 30, 31 | 3eqtr4d 2783 |
1
โข ((๐
โ Ring โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ร (๐ ยท ๐)) = (๐ ยท (๐ ร ๐))) |