Step | Hyp | Ref
| Expression |
1 | | fnmgp 13130 |
. . . 4
โข mulGrp Fn
V |
2 | | elex 2748 |
. . . 4
โข (๐
โ ๐ โ ๐
โ V) |
3 | | funfvex 5532 |
. . . . 5
โข ((Fun
mulGrp โง ๐
โ dom
mulGrp) โ (mulGrpโ๐
) โ V) |
4 | 3 | funfni 5316 |
. . . 4
โข ((mulGrp
Fn V โง ๐
โ V)
โ (mulGrpโ๐
)
โ V) |
5 | 1, 2, 4 | sylancr 414 |
. . 3
โข (๐
โ ๐ โ (mulGrpโ๐
) โ V) |
6 | | eqid 2177 |
. . . 4
โข
(Baseโ(mulGrpโ๐
)) = (Baseโ(mulGrpโ๐
)) |
7 | | eqid 2177 |
. . . 4
โข
(+gโ(mulGrpโ๐
)) =
(+gโ(mulGrpโ๐
)) |
8 | | eqid 2177 |
. . . 4
โข
(0gโ(mulGrpโ๐
)) =
(0gโ(mulGrpโ๐
)) |
9 | 6, 7, 8 | grpidvalg 12791 |
. . 3
โข
((mulGrpโ๐
)
โ V โ (0gโ(mulGrpโ๐
)) = (โฉ๐(๐ โ (Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ)))) |
10 | 5, 9 | syl 14 |
. 2
โข (๐
โ ๐ โ
(0gโ(mulGrpโ๐
)) = (โฉ๐(๐ โ (Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ)))) |
11 | | eqid 2177 |
. . 3
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
12 | | dfur2.u |
. . 3
โข 1 =
(1rโ๐
) |
13 | 11, 12 | ringidvalg 13142 |
. 2
โข (๐
โ ๐ โ 1 =
(0gโ(mulGrpโ๐
))) |
14 | | dfur2.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
15 | 11, 14 | mgpbasg 13134 |
. . . . 5
โข (๐
โ ๐ โ ๐ต = (Baseโ(mulGrpโ๐
))) |
16 | 15 | eleq2d 2247 |
. . . 4
โข (๐
โ ๐ โ (๐ โ ๐ต โ ๐ โ (Baseโ(mulGrpโ๐
)))) |
17 | | dfur2.t |
. . . . . . . . 9
โข ยท =
(.rโ๐
) |
18 | 11, 17 | mgpplusgg 13132 |
. . . . . . . 8
โข (๐
โ ๐ โ ยท =
(+gโ(mulGrpโ๐
))) |
19 | 18 | oveqd 5891 |
. . . . . . 7
โข (๐
โ ๐ โ (๐ ยท ๐ฅ) = (๐(+gโ(mulGrpโ๐
))๐ฅ)) |
20 | 19 | eqeq1d 2186 |
. . . . . 6
โข (๐
โ ๐ โ ((๐ ยท ๐ฅ) = ๐ฅ โ (๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ)) |
21 | 18 | oveqd 5891 |
. . . . . . 7
โข (๐
โ ๐ โ (๐ฅ ยท ๐) = (๐ฅ(+gโ(mulGrpโ๐
))๐)) |
22 | 21 | eqeq1d 2186 |
. . . . . 6
โข (๐
โ ๐ โ ((๐ฅ ยท ๐) = ๐ฅ โ (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ)) |
23 | 20, 22 | anbi12d 473 |
. . . . 5
โข (๐
โ ๐ โ (((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ) โ ((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ))) |
24 | 15, 23 | raleqbidv 2684 |
. . . 4
โข (๐
โ ๐ โ (โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ) โ โ๐ฅ โ (Baseโ(mulGrpโ๐
))((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ))) |
25 | 16, 24 | anbi12d 473 |
. . 3
โข (๐
โ ๐ โ ((๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)) โ (๐ โ (Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ)))) |
26 | 25 | iotabidv 5199 |
. 2
โข (๐
โ ๐ โ (โฉ๐(๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ))) = (โฉ๐(๐ โ (Baseโ(mulGrpโ๐
)) โง โ๐ฅ โ
(Baseโ(mulGrpโ๐
))((๐(+gโ(mulGrpโ๐
))๐ฅ) = ๐ฅ โง (๐ฅ(+gโ(mulGrpโ๐
))๐) = ๐ฅ)))) |
27 | 10, 13, 26 | 3eqtr4d 2220 |
1
โข (๐
โ ๐ โ 1 = (โฉ๐(๐ โ ๐ต โง โ๐ฅ โ ๐ต ((๐ ยท ๐ฅ) = ๐ฅ โง (๐ฅ ยท ๐) = ๐ฅ)))) |