Step | Hyp | Ref
| Expression |
1 | | invrfvald.u |
. . . 4
โข (๐ โ ๐ = (Unitโ๐
)) |
2 | 1 | oveq2d 5890 |
. . 3
โข (๐ โ ((mulGrpโ๐
) โพs ๐) = ((mulGrpโ๐
) โพs
(Unitโ๐
))) |
3 | 2 | fveq2d 5519 |
. 2
โข (๐ โ
(invgโ((mulGrpโ๐
) โพs ๐)) =
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
4 | | invrfvald.g |
. . 3
โข (๐ โ ๐บ = ((mulGrpโ๐
) โพs ๐)) |
5 | 4 | fveq2d 5519 |
. 2
โข (๐ โ
(invgโ๐บ) =
(invgโ((mulGrpโ๐
) โพs ๐))) |
6 | | invrfvald.i |
. . 3
โข (๐ โ ๐ผ = (invrโ๐
)) |
7 | | df-invr 13288 |
. . . 4
โข
invr = (๐
โ V โฆ (invgโ((mulGrpโ๐) โพs (Unitโ๐)))) |
8 | | fveq2 5515 |
. . . . . 6
โข (๐ = ๐
โ (mulGrpโ๐) = (mulGrpโ๐
)) |
9 | | fveq2 5515 |
. . . . . 6
โข (๐ = ๐
โ (Unitโ๐) = (Unitโ๐
)) |
10 | 8, 9 | oveq12d 5892 |
. . . . 5
โข (๐ = ๐
โ ((mulGrpโ๐) โพs (Unitโ๐)) = ((mulGrpโ๐
) โพs
(Unitโ๐
))) |
11 | 10 | fveq2d 5519 |
. . . 4
โข (๐ = ๐
โ
(invgโ((mulGrpโ๐) โพs (Unitโ๐))) =
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
12 | | invrfvald.r |
. . . . 5
โข (๐ โ ๐
โ Ring) |
13 | 12 | elexd 2750 |
. . . 4
โข (๐ โ ๐
โ V) |
14 | | eqid 2177 |
. . . . . . . 8
โข
(Unitโ๐
) =
(Unitโ๐
) |
15 | | eqid 2177 |
. . . . . . . 8
โข
((mulGrpโ๐
)
โพs (Unitโ๐
)) = ((mulGrpโ๐
) โพs (Unitโ๐
)) |
16 | 14, 15 | unitgrp 13283 |
. . . . . . 7
โข (๐
โ Ring โ
((mulGrpโ๐
)
โพs (Unitโ๐
)) โ Grp) |
17 | 12, 16 | syl 14 |
. . . . . 6
โข (๐ โ ((mulGrpโ๐
) โพs
(Unitโ๐
)) โ
Grp) |
18 | | eqid 2177 |
. . . . . . 7
โข
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) =
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) |
19 | | eqid 2177 |
. . . . . . 7
โข
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) =
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) |
20 | 18, 19 | grpinvfng 12916 |
. . . . . 6
โข
(((mulGrpโ๐
)
โพs (Unitโ๐
)) โ Grp โ
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) Fn
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
21 | 17, 20 | syl 14 |
. . . . 5
โข (๐ โ
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) Fn
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
22 | | basfn 12519 |
. . . . . 6
โข Base Fn
V |
23 | 17 | elexd 2750 |
. . . . . 6
โข (๐ โ ((mulGrpโ๐
) โพs
(Unitโ๐
)) โ
V) |
24 | | funfvex 5532 |
. . . . . . 7
โข ((Fun
Base โง ((mulGrpโ๐
) โพs (Unitโ๐
)) โ dom Base) โ
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) |
25 | 24 | funfni 5316 |
. . . . . 6
โข ((Base Fn
V โง ((mulGrpโ๐
)
โพs (Unitโ๐
)) โ V) โ
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) |
26 | 22, 23, 25 | sylancr 414 |
. . . . 5
โข (๐ โ
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) |
27 | | fnex 5738 |
. . . . 5
โข
(((invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) Fn
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) โง
(Baseโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) โ
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) |
28 | 21, 26, 27 | syl2anc 411 |
. . . 4
โข (๐ โ
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
))) โ V) |
29 | 7, 11, 13, 28 | fvmptd3 5609 |
. . 3
โข (๐ โ
(invrโ๐
) =
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
30 | 6, 29 | eqtrd 2210 |
. 2
โข (๐ โ ๐ผ =
(invgโ((mulGrpโ๐
) โพs (Unitโ๐
)))) |
31 | 3, 5, 30 | 3eqtr4rd 2221 |
1
โข (๐ โ ๐ผ = (invgโ๐บ)) |