Step | Hyp | Ref
| Expression |
1 | | dvrval.d |
. 2
β’ / =
(/rβπ
) |
2 | | fveq2 6839 |
. . . . . 6
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
3 | | dvrval.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
4 | 2, 3 | eqtr4di 2795 |
. . . . 5
β’ (π = π
β (Baseβπ) = π΅) |
5 | | fveq2 6839 |
. . . . . 6
β’ (π = π
β (Unitβπ) = (Unitβπ
)) |
6 | | dvrval.u |
. . . . . 6
β’ π = (Unitβπ
) |
7 | 5, 6 | eqtr4di 2795 |
. . . . 5
β’ (π = π
β (Unitβπ) = π) |
8 | | fveq2 6839 |
. . . . . . 7
β’ (π = π
β (.rβπ) = (.rβπ
)) |
9 | | dvrval.t |
. . . . . . 7
β’ Β· =
(.rβπ
) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . 6
β’ (π = π
β (.rβπ) = Β· ) |
11 | | eqidd 2738 |
. . . . . 6
β’ (π = π
β π₯ = π₯) |
12 | | fveq2 6839 |
. . . . . . . 8
β’ (π = π
β (invrβπ) = (invrβπ
)) |
13 | | dvrval.i |
. . . . . . . 8
β’ πΌ = (invrβπ
) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . 7
β’ (π = π
β (invrβπ) = πΌ) |
15 | 14 | fveq1d 6841 |
. . . . . 6
β’ (π = π
β ((invrβπ)βπ¦) = (πΌβπ¦)) |
16 | 10, 11, 15 | oveq123d 7372 |
. . . . 5
β’ (π = π
β (π₯(.rβπ)((invrβπ)βπ¦)) = (π₯ Β· (πΌβπ¦))) |
17 | 4, 7, 16 | mpoeq123dv 7426 |
. . . 4
β’ (π = π
β (π₯ β (Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦))) = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦)))) |
18 | | df-dvr 20065 |
. . . 4
β’
/r = (π
β V β¦ (π₯ β
(Baseβπ), π¦ β (Unitβπ) β¦ (π₯(.rβπ)((invrβπ)βπ¦)))) |
19 | 3 | fvexi 6853 |
. . . . 5
β’ π΅ β V |
20 | 6 | fvexi 6853 |
. . . . 5
β’ π β V |
21 | 19, 20 | mpoex 8004 |
. . . 4
β’ (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) β V |
22 | 17, 18, 21 | fvmpt 6945 |
. . 3
β’ (π
β V β
(/rβπ
) =
(π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦)))) |
23 | | fvprc 6831 |
. . . 4
β’ (Β¬
π
β V β
(/rβπ
) =
β
) |
24 | | fvprc 6831 |
. . . . . . 7
β’ (Β¬
π
β V β
(Baseβπ
) =
β
) |
25 | 3, 24 | eqtrid 2789 |
. . . . . 6
β’ (Β¬
π
β V β π΅ = β
) |
26 | 25 | orcd 871 |
. . . . 5
β’ (Β¬
π
β V β (π΅ = β
β¨ π = β
)) |
27 | | 0mpo0 7434 |
. . . . 5
β’ ((π΅ = β
β¨ π = β
) β (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) = β
) |
28 | 26, 27 | syl 17 |
. . . 4
β’ (Β¬
π
β V β (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) = β
) |
29 | 23, 28 | eqtr4d 2780 |
. . 3
β’ (Β¬
π
β V β
(/rβπ
) =
(π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦)))) |
30 | 22, 29 | pm2.61i 182 |
. 2
β’
(/rβπ
) = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) |
31 | 1, 30 | eqtri 2765 |
1
β’ / = (π₯ β π΅, π¦ β π β¦ (π₯ Β· (πΌβπ¦))) |