Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . 4
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
2 | 1 | ringmgp 13185 |
. . 3
โข (๐
โ Ring โ
(mulGrpโ๐
) โ
Mnd) |
3 | | eqid 2177 |
. . . 4
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
4 | | eqid 2177 |
. . . 4
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
5 | 3, 4 | mndideu 12827 |
. . 3
โข
((mulGrpโ๐
)
โ Mnd โ โ!๐ข
โ (Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ)) |
6 | 2, 5 | syl 14 |
. 2
โข (๐
โ Ring โ
โ!๐ข โ
(Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ)) |
7 | | ringcl.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
8 | 1, 7 | mgpbasg 13136 |
. . . . 5
โข (๐
โ Ring โ ๐ต =
(Baseโ(mulGrpโ๐
))) |
9 | | ringcl.t |
. . . . . . . . 9
โข ยท =
(.rโ๐
) |
10 | 1, 9 | mgpplusgg 13134 |
. . . . . . . 8
โข (๐
โ Ring โ ยท =
(+gโ(mulGrpโ๐
))) |
11 | 10 | oveqd 5892 |
. . . . . . 7
โข (๐
โ Ring โ (๐ข ยท ๐ฅ) = (๐ข(+gโ(mulGrpโ๐
))๐ฅ)) |
12 | 11 | eqeq1d 2186 |
. . . . . 6
โข (๐
โ Ring โ ((๐ข ยท ๐ฅ) = ๐ฅ โ (๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ)) |
13 | 10 | oveqd 5892 |
. . . . . . 7
โข (๐
โ Ring โ (๐ฅ ยท ๐ข) = (๐ฅ(+gโ(mulGrpโ๐
))๐ข)) |
14 | 13 | eqeq1d 2186 |
. . . . . 6
โข (๐
โ Ring โ ((๐ฅ ยท ๐ข) = ๐ฅ โ (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ)) |
15 | 12, 14 | anbi12d 473 |
. . . . 5
โข (๐
โ Ring โ (((๐ข ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ข) = ๐ฅ) โ ((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
16 | 8, 15 | raleqbidv 2685 |
. . . 4
โข (๐
โ Ring โ
(โ๐ฅ โ ๐ต ((๐ข ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ข) = ๐ฅ) โ โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
17 | 16 | reubidv 2661 |
. . 3
โข (๐
โ Ring โ
(โ!๐ข โ ๐ต โ๐ฅ โ ๐ต ((๐ข ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ข) = ๐ฅ) โ โ!๐ข โ ๐ต โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
18 | | reueq1 2675 |
. . . 4
โข (๐ต =
(Baseโ(mulGrpโ๐
)) โ (โ!๐ข โ ๐ต โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ) โ โ!๐ข โ (Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
19 | 8, 18 | syl 14 |
. . 3
โข (๐
โ Ring โ
(โ!๐ข โ ๐ต โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ) โ โ!๐ข โ (Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
20 | 17, 19 | bitrd 188 |
. 2
โข (๐
โ Ring โ
(โ!๐ข โ ๐ต โ๐ฅ โ ๐ต ((๐ข ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ข) = ๐ฅ) โ โ!๐ข โ (Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ข(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ข) = ๐ฅ))) |
21 | 6, 20 | mpbird 167 |
1
โข (๐
โ Ring โ
โ!๐ข โ ๐ต โ๐ฅ โ ๐ต ((๐ข ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ข) = ๐ฅ)) |