Step | Hyp | Ref
| Expression |
1 | | elex 2750 |
. 2
โข (๐
โ CRing โ ๐
โ V) |
2 | | elex 2750 |
. . 3
โข (๐
โ Ring โ ๐
โ V) |
3 | 2 | adantr 276 |
. 2
โข ((๐
โ Ring โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)) โ ๐
โ V) |
4 | | eqid 2177 |
. . . 4
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
5 | 4 | iscrng 13191 |
. . 3
โข (๐
โ CRing โ (๐
โ Ring โง
(mulGrpโ๐
) โ
CMnd)) |
6 | 4 | ringmgp 13190 |
. . . . 5
โข (๐
โ Ring โ
(mulGrpโ๐
) โ
Mnd) |
7 | | eqid 2177 |
. . . . . . . 8
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
8 | | eqid 2177 |
. . . . . . . 8
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
9 | 7, 8 | iscmn 13101 |
. . . . . . 7
โข
((mulGrpโ๐
)
โ CMnd โ ((mulGrpโ๐
) โ Mnd โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))โ๐ฆ โ (Baseโ(mulGrpโ๐
))(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ))) |
10 | | ringcl.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐
) |
11 | 4, 10 | mgpbasg 13141 |
. . . . . . . . 9
โข (๐
โ V โ ๐ต =
(Baseโ(mulGrpโ๐
))) |
12 | | ringcl.t |
. . . . . . . . . . . . 13
โข ยท =
(.rโ๐
) |
13 | 4, 12 | mgpplusgg 13139 |
. . . . . . . . . . . 12
โข (๐
โ V โ ยท =
(+gโ(mulGrpโ๐
))) |
14 | 13 | oveqd 5894 |
. . . . . . . . . . 11
โข (๐
โ V โ (๐ฅ ยท ๐ฆ) = (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ)) |
15 | 13 | oveqd 5894 |
. . . . . . . . . . 11
โข (๐
โ V โ (๐ฆ ยท ๐ฅ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ)) |
16 | 14, 15 | eqeq12d 2192 |
. . . . . . . . . 10
โข (๐
โ V โ ((๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ) โ (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ))) |
17 | 11, 16 | raleqbidv 2685 |
. . . . . . . . 9
โข (๐
โ V โ (โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ) โ โ๐ฆ โ (Baseโ(mulGrpโ๐
))(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ))) |
18 | 11, 17 | raleqbidv 2685 |
. . . . . . . 8
โข (๐
โ V โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ) โ โ๐ฅ โ (Baseโ(mulGrpโ๐
))โ๐ฆ โ (Baseโ(mulGrpโ๐
))(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ))) |
19 | 18 | anbi2d 464 |
. . . . . . 7
โข (๐
โ V โ
(((mulGrpโ๐
) โ
Mnd โง โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)) โ ((mulGrpโ๐
) โ Mnd โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))โ๐ฆ โ (Baseโ(mulGrpโ๐
))(๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ)))) |
20 | 9, 19 | bitr4id 199 |
. . . . . 6
โข (๐
โ V โ
((mulGrpโ๐
) โ
CMnd โ ((mulGrpโ๐
) โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)))) |
21 | 20 | baibd 923 |
. . . . 5
โข ((๐
โ V โง
(mulGrpโ๐
) โ
Mnd) โ ((mulGrpโ๐
) โ CMnd โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ))) |
22 | 6, 21 | sylan2 286 |
. . . 4
โข ((๐
โ V โง ๐
โ Ring) โ
((mulGrpโ๐
) โ
CMnd โ โ๐ฅ
โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ))) |
23 | 22 | pm5.32da 452 |
. . 3
โข (๐
โ V โ ((๐
โ Ring โง
(mulGrpโ๐
) โ
CMnd) โ (๐
โ Ring
โง โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)))) |
24 | 5, 23 | bitrid 192 |
. 2
โข (๐
โ V โ (๐
โ CRing โ (๐
โ Ring โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)))) |
25 | 1, 3, 24 | pm5.21nii 704 |
1
โข (๐
โ CRing โ (๐
โ Ring โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ))) |