Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . 5
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
2 | 1 | ringmgp 13183 |
. . . 4
โข (๐
โ Ring โ
(mulGrpโ๐
) โ
Mnd) |
3 | 2 | adantr 276 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (mulGrpโ๐
) โ Mnd) |
4 | | simpr1 1003 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
5 | | ringcl.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
6 | 1, 5 | mgpbasg 13134 |
. . . . 5
โข (๐
โ Ring โ ๐ต =
(Baseโ(mulGrpโ๐
))) |
7 | 6 | adantr 276 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ต = (Baseโ(mulGrpโ๐
))) |
8 | 4, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
9 | | simpr2 1004 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
10 | 9, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
11 | | simpr3 1005 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
12 | 11, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
13 | | eqid 2177 |
. . . 4
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
14 | | eqid 2177 |
. . . 4
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
15 | 13, 14 | mndass 12824 |
. . 3
โข
(((mulGrpโ๐
)
โ Mnd โง (๐ โ
(Baseโ(mulGrpโ๐
)) โง ๐ โ (Baseโ(mulGrpโ๐
)) โง ๐ โ (Baseโ(mulGrpโ๐
)))) โ ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
16 | 3, 8, 10, 12, 15 | syl13anc 1240 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
17 | | ringcl.t |
. . . . 5
โข ยท =
(.rโ๐
) |
18 | 1, 17 | mgpplusgg 13132 |
. . . 4
โข (๐
โ Ring โ ยท =
(+gโ(mulGrpโ๐
))) |
19 | 18 | adantr 276 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ยท =
(+gโ(mulGrpโ๐
))) |
20 | 19 | oveqd 5891 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) = (๐(+gโ(mulGrpโ๐
))๐)) |
21 | | eqidd 2178 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ = ๐) |
22 | 19, 20, 21 | oveq123d 5895 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐)) |
23 | | eqidd 2178 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ = ๐) |
24 | 19 | oveqd 5891 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) = (๐(+gโ(mulGrpโ๐
))๐)) |
25 | 19, 23, 24 | oveq123d 5895 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ ยท ๐)) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
26 | 16, 22, 25 | 3eqtr4d 2220 |
1
โข ((๐
โ Ring โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |