Step | Hyp | Ref
| Expression |
1 | | eqidd 2738 |
. . . 4
β’ (π = π
β β€ = β€) |
2 | | fveq2 6839 |
. . . . . . 7
β’ (π = π
β (β€RHomβπ) = (β€RHomβπ
)) |
3 | | qqhval.3 |
. . . . . . 7
β’ πΏ = (β€RHomβπ
) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . 6
β’ (π = π
β (β€RHomβπ) = πΏ) |
5 | 4 | cnveqd 5829 |
. . . . 5
β’ (π = π
β β‘(β€RHomβπ) = β‘πΏ) |
6 | | fveq2 6839 |
. . . . 5
β’ (π = π
β (Unitβπ) = (Unitβπ
)) |
7 | 5, 6 | imaeq12d 6012 |
. . . 4
β’ (π = π
β (β‘(β€RHomβπ) β (Unitβπ)) = (β‘πΏ β (Unitβπ
))) |
8 | | fveq2 6839 |
. . . . . . 7
β’ (π = π
β (/rβπ) = (/rβπ
)) |
9 | | qqhval.1 |
. . . . . . 7
β’ / =
(/rβπ
) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . 6
β’ (π = π
β (/rβπ) = / ) |
11 | 4 | fveq1d 6841 |
. . . . . 6
β’ (π = π
β ((β€RHomβπ)βπ₯) = (πΏβπ₯)) |
12 | 4 | fveq1d 6841 |
. . . . . 6
β’ (π = π
β ((β€RHomβπ)βπ¦) = (πΏβπ¦)) |
13 | 10, 11, 12 | oveq123d 7372 |
. . . . 5
β’ (π = π
β (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦)) = ((πΏβπ₯) / (πΏβπ¦))) |
14 | 13 | opeq2d 4835 |
. . . 4
β’ (π = π
β β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β© = β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) |
15 | 1, 7, 14 | mpoeq123dv 7426 |
. . 3
β’ (π = π
β (π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©) = (π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
16 | 15 | rneqd 5891 |
. 2
β’ (π = π
β ran (π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©) = ran (π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |
17 | | df-qqh 32366 |
. 2
β’
βHom = (π
β V β¦ ran (π₯
β β€, π¦ β
(β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©)) |
18 | | zex 12466 |
. . . 4
β’ β€
β V |
19 | 3 | fvexi 6853 |
. . . . . 6
β’ πΏ β V |
20 | 19 | cnvex 7854 |
. . . . 5
β’ β‘πΏ β V |
21 | | imaexg 7844 |
. . . . 5
β’ (β‘πΏ β V β (β‘πΏ β (Unitβπ
)) β V) |
22 | 20, 21 | ax-mp 5 |
. . . 4
β’ (β‘πΏ β (Unitβπ
)) β V |
23 | 18, 22 | mpoex 8004 |
. . 3
β’ (π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β V |
24 | 23 | rnex 7841 |
. 2
β’ ran
(π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©) β V |
25 | 16, 17, 24 | fvmpt 6945 |
1
β’ (π
β V β
(βHomβπ
) = ran
(π₯ β β€, π¦ β (β‘πΏ β (Unitβπ
)) β¦ β¨(π₯ / π¦), ((πΏβπ₯) / (πΏβπ¦))β©)) |