Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . . 5
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
2 | 1 | srgmgp 13156 |
. . . 4
โข (๐
โ SRing โ
(mulGrpโ๐
) โ
Mnd) |
3 | 2 | adantr 276 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (mulGrpโ๐
) โ Mnd) |
4 | | simpr1 1003 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
5 | | srgcl.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
6 | 1, 5 | mgpbasg 13141 |
. . . . 5
โข (๐
โ SRing โ ๐ต =
(Baseโ(mulGrpโ๐
))) |
7 | 6 | adantr 276 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ต = (Baseโ(mulGrpโ๐
))) |
8 | 4, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
9 | | simpr2 1004 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
10 | 9, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
11 | | simpr3 1005 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
12 | 11, 7 | eleqtrd 2256 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ (Baseโ(mulGrpโ๐
))) |
13 | | eqid 2177 |
. . . 4
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
14 | | eqid 2177 |
. . . 4
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
15 | 13, 14 | mndass 12830 |
. . 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
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
17 | | srgcl.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
18 | 1, 17 | mgpplusgg 13139 |
. . . . 5
โข (๐
โ SRing โ ยท =
(+gโ(mulGrpโ๐
))) |
19 | 18 | adantr 276 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ยท =
(+gโ(mulGrpโ๐
))) |
20 | 19 | oveqd 5894 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = ((๐ ยท ๐)(+gโ(mulGrpโ๐
))๐)) |
21 | 19 | oveqd 5894 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) = (๐(+gโ(mulGrpโ๐
))๐)) |
22 | 21 | oveq1d 5892 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐)(+gโ(mulGrpโ๐
))๐) = ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐)) |
23 | 20, 22 | eqtrd 2210 |
. 2
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = ((๐(+gโ(mulGrpโ๐
))๐)(+gโ(mulGrpโ๐
))๐)) |
24 | 19 | oveqd 5894 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ ยท ๐)) = (๐(+gโ(mulGrpโ๐
))(๐ ยท ๐))) |
25 | 19 | oveqd 5894 |
. . . 4
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) = (๐(+gโ(mulGrpโ๐
))๐)) |
26 | 25 | oveq2d 5893 |
. . 3
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(+gโ(mulGrpโ๐
))(๐ ยท ๐)) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
27 | 24, 26 | eqtrd 2210 |
. 2
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ ยท ๐)) = (๐(+gโ(mulGrpโ๐
))(๐(+gโ(mulGrpโ๐
))๐))) |
28 | 16, 23, 27 | 3eqtr4d 2220 |
1
โข ((๐
โ SRing โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |