Step | Hyp | Ref
| Expression |
1 | | rngchomfvalALTV.h |
. . 3
β’ π» = (Hom βπΆ) |
2 | | rngcbasALTV.c |
. . . . 5
β’ πΆ = (RngCatALTVβπ) |
3 | | rngcbasALTV.u |
. . . . 5
β’ (π β π β π) |
4 | | rngcbasALTV.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
5 | 2, 4, 3 | rngcbasALTV 46371 |
. . . . 5
β’ (π β π΅ = (π β© Rng)) |
6 | | eqidd 2734 |
. . . . 5
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))) |
7 | | eqidd 2734 |
. . . . 5
β’ (π β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π))) = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))) |
8 | 2, 3, 5, 6, 7 | rngcvalALTV 46349 |
. . . 4
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©}) |
9 | 8 | fveq2d 6850 |
. . 3
β’ (π β (Hom βπΆ) = (Hom
β{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©})) |
10 | 1, 9 | eqtrid 2785 |
. 2
β’ (π β π» = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©})) |
11 | 4 | fvexi 6860 |
. . . 4
β’ π΅ β V |
12 | 11, 11 | mpoex 8016 |
. . 3
β’ (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦)) β V |
13 | | catstr 17853 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©} Struct β¨1, ;15β© |
14 | | homid 17301 |
. . . 4
β’ Hom =
Slot (Hom βndx) |
15 | | snsstp2 4781 |
. . . 4
β’
{β¨(Hom βndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©} β {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©} |
16 | 13, 14, 15 | strfv 17084 |
. . 3
β’ ((π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦)) β V β (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦)) = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©})) |
17 | 12, 16 | mp1i 13 |
. 2
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦)) = (Hom β{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π₯ β
π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©})) |
18 | 10, 17 | eqtr4d 2776 |
1
β’ (π β π» = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RngHomo π¦))) |