Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . 3
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
2 | | eqid 2177 |
. . 3
โข
(0gโ(mulGrpโ๐
)) =
(0gโ(mulGrpโ๐
)) |
3 | | eqid 2177 |
. . 3
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
4 | | srgidm.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
5 | | srgidm.t |
. . . . . 6
โข ยท =
(.rโ๐
) |
6 | 4, 5 | srgideu 13155 |
. . . . 5
โข (๐
โ SRing โ
โ!๐ฆ โ ๐ต โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ)) |
7 | | reurex 2691 |
. . . . 5
โข
(โ!๐ฆ โ
๐ต โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ) โ โ๐ฆ โ ๐ต โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ)) |
8 | 6, 7 | syl 14 |
. . . 4
โข (๐
โ SRing โ
โ๐ฆ โ ๐ต โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ)) |
9 | | eqid 2177 |
. . . . . 6
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
10 | 9, 4 | mgpbasg 13136 |
. . . . 5
โข (๐
โ SRing โ ๐ต =
(Baseโ(mulGrpโ๐
))) |
11 | 9, 5 | mgpplusgg 13134 |
. . . . . . . . 9
โข (๐
โ SRing โ ยท =
(+gโ(mulGrpโ๐
))) |
12 | 11 | oveqd 5892 |
. . . . . . . 8
โข (๐
โ SRing โ (๐ฆ ยท ๐ฅ) = (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ)) |
13 | 12 | eqeq1d 2186 |
. . . . . . 7
โข (๐
โ SRing โ ((๐ฆ ยท ๐ฅ) = ๐ฅ โ (๐ฆ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ)) |
14 | 11 | oveqd 5892 |
. . . . . . . 8
โข (๐
โ SRing โ (๐ฅ ยท ๐ฆ) = (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ)) |
15 | 14 | eqeq1d 2186 |
. . . . . . 7
โข (๐
โ SRing โ ((๐ฅ ยท ๐ฆ) = ๐ฅ โ (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = ๐ฅ)) |
16 | 13, 15 | anbi12d 473 |
. . . . . 6
โข (๐
โ SRing โ (((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ) โ ((๐ฆ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = ๐ฅ))) |
17 | 10, 16 | raleqbidv 2685 |
. . . . 5
โข (๐
โ SRing โ
(โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ) โ โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ฆ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = ๐ฅ))) |
18 | 10, 17 | rexeqbidv 2686 |
. . . 4
โข (๐
โ SRing โ
(โ๐ฆ โ ๐ต โ๐ฅ โ ๐ต ((๐ฆ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ฆ) = ๐ฅ) โ โ๐ฆ โ (Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ฆ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = ๐ฅ))) |
19 | 8, 18 | mpbid 147 |
. . 3
โข (๐
โ SRing โ
โ๐ฆ โ
(Baseโ(mulGrpโ๐
))โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ฆ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ฆ) = ๐ฅ)) |
20 | 1, 2, 3, 19 | ismgmid 12796 |
. 2
โข (๐
โ SRing โ ((๐ผ โ
(Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ผ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ผ) = ๐ฅ)) โ
(0gโ(mulGrpโ๐
)) = ๐ผ)) |
21 | 10 | eleq2d 2247 |
. . 3
โข (๐
โ SRing โ (๐ผ โ ๐ต โ ๐ผ โ (Baseโ(mulGrpโ๐
)))) |
22 | 11 | oveqd 5892 |
. . . . . 6
โข (๐
โ SRing โ (๐ผ ยท ๐ฅ) = (๐ผ(+gโ(mulGrpโ๐
))๐ฅ)) |
23 | 22 | eqeq1d 2186 |
. . . . 5
โข (๐
โ SRing โ ((๐ผ ยท ๐ฅ) = ๐ฅ โ (๐ผ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ)) |
24 | 11 | oveqd 5892 |
. . . . . 6
โข (๐
โ SRing โ (๐ฅ ยท ๐ผ) = (๐ฅ(+gโ(mulGrpโ๐
))๐ผ)) |
25 | 24 | eqeq1d 2186 |
. . . . 5
โข (๐
โ SRing โ ((๐ฅ ยท ๐ผ) = ๐ฅ โ (๐ฅ(+gโ(mulGrpโ๐
))๐ผ) = ๐ฅ)) |
26 | 23, 25 | anbi12d 473 |
. . . 4
โข (๐
โ SRing โ (((๐ผ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ผ) = ๐ฅ) โ ((๐ผ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ผ) = ๐ฅ))) |
27 | 10, 26 | raleqbidv 2685 |
. . 3
โข (๐
โ SRing โ
(โ๐ฅ โ ๐ต ((๐ผ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ผ) = ๐ฅ) โ โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐ผ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ผ) = ๐ฅ))) |
28 | 21, 27 | anbi12d 473 |
. 2
โข (๐
โ SRing โ ((๐ผ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ผ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ผ) = ๐ฅ)) โ (๐ผ โ (Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))((๐ผ(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐ผ) = ๐ฅ)))) |
29 | | srgidm.u |
. . . 4
โข 1 =
(1rโ๐
) |
30 | 9, 29 | ringidvalg 13144 |
. . 3
โข (๐
โ SRing โ 1 =
(0gโ(mulGrpโ๐
))) |
31 | 30 | eqeq1d 2186 |
. 2
โข (๐
โ SRing โ ( 1 = ๐ผ โ
(0gโ(mulGrpโ๐
)) = ๐ผ)) |
32 | 20, 28, 31 | 3bitr4d 220 |
1
โข (๐
โ SRing โ ((๐ผ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ผ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐ผ) = ๐ฅ)) โ 1 = ๐ผ)) |