Step | Hyp | Ref
| Expression |
1 | | df-dvr 13299 |
. . 3
β’
/r = (π
β V β¦ (π₯ β
(Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) |
2 | | fveq2 5515 |
. . . 4
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
3 | | fveq2 5515 |
. . . 4
β’ (π = π
β (Unitβπ) = (Unitβπ
)) |
4 | | fveq2 5515 |
. . . . 5
β’ (π = π
β (.rβπ) = (.rβπ
)) |
5 | | eqidd 2178 |
. . . . 5
β’ (π = π
β π₯ = π₯) |
6 | | fveq2 5515 |
. . . . . 6
β’ (π = π
β (invrβπ) = (invrβπ
)) |
7 | 6 | fveq1d 5517 |
. . . . 5
β’ (π = π
β ((invrβπ)βπ¦) = ((invrβπ
)βπ¦)) |
8 | 4, 5, 7 | oveq123d 5895 |
. . . 4
β’ (π = π
β (π₯(.rβπ)((invrβπ)βπ¦)) = (π₯(.rβπ
)((invrβπ
)βπ¦))) |
9 | 2, 3, 8 | mpoeq123dv 5936 |
. . 3
β’ (π = π
β (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦))) = (π₯ β (Baseβπ
), π¦ β (Unitβπ
) β¦ (π₯(.rβπ
)((invrβπ
)βπ¦)))) |
10 | | dvrfvald.r |
. . . 4
β’ (π β π
β SRing) |
11 | 10 | elexd 2750 |
. . 3
β’ (π β π
β V) |
12 | | basfn 12519 |
. . . . 5
β’ Base Fn
V |
13 | | funfvex 5532 |
. . . . . 6
β’ ((Fun
Base β§ π
β dom
Base) β (Baseβπ
)
β V) |
14 | 13 | funfni 5316 |
. . . . 5
β’ ((Base Fn
V β§ π
β V) β
(Baseβπ
) β
V) |
15 | 12, 11, 14 | sylancr 414 |
. . . 4
β’ (π β (Baseβπ
) β V) |
16 | | eqidd 2178 |
. . . . . 6
β’ (π β (Baseβπ
) = (Baseβπ
)) |
17 | | eqidd 2178 |
. . . . . 6
β’ (π β (Unitβπ
) = (Unitβπ
)) |
18 | 16, 17, 10 | unitssd 13276 |
. . . . 5
β’ (π β (Unitβπ
) β (Baseβπ
)) |
19 | 15, 18 | ssexd 4143 |
. . . 4
β’ (π β (Unitβπ
) β V) |
20 | | mpoexga 6212 |
. . . 4
β’
(((Baseβπ
)
β V β§ (Unitβπ
) β V) β (π₯ β (Baseβπ
), π¦ β (Unitβπ
) β¦ (π₯(.rβπ
)((invrβπ
)βπ¦))) β V) |
21 | 15, 19, 20 | syl2anc 411 |
. . 3
β’ (π β (π₯ β (Baseβπ
), π¦ β (Unitβπ
) β¦ (π₯(.rβπ
)((invrβπ
)βπ¦))) β V) |
22 | 1, 9, 11, 21 | fvmptd3 5609 |
. 2
β’ (π β (/rβπ
) = (π₯ β (Baseβπ
), π¦ β (Unitβπ
) β¦ (π₯(.rβπ
)((invrβπ
)βπ¦)))) |
23 | | dvrfvald.d |
. 2
β’ (π β / =
(/rβπ
)) |
24 | | dvrfvald.b |
. . 3
β’ (π β π΅ = (Baseβπ
)) |
25 | | dvrfvald.u |
. . 3
β’ (π β π = (Unitβπ
)) |
26 | | dvrfvald.t |
. . . 4
β’ (π β Β· =
(.rβπ
)) |
27 | | eqidd 2178 |
. . . 4
β’ (π β π₯ = π₯) |
28 | | dvrfvald.i |
. . . . 5
β’ (π β πΌ = (invrβπ
)) |
29 | 28 | fveq1d 5517 |
. . . 4
β’ (π β (πΌβπ¦) = ((invrβπ
)βπ¦)) |
30 | 26, 27, 29 | oveq123d 5895 |
. . 3
β’ (π β (π₯ Β· (πΌβπ¦)) = (π₯(.rβπ
)((invrβπ
)βπ¦))) |
31 | 24, 25, 30 | mpoeq123dv 5936 |
. 2
β’ (π β (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) = (π₯ β (Baseβπ
), π¦ β (Unitβπ
) β¦ (π₯(.rβπ
)((invrβπ
)βπ¦)))) |
32 | 22, 23, 31 | 3eqtr4d 2220 |
1
β’ (π β / = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦)))) |