Step | Hyp | Ref
| Expression |
1 | | ringcbasALTV.c |
. . . 4
β’ πΆ = (RingCatALTVβπ) |
2 | | ringcbasALTV.u |
. . . 4
β’ (π β π β π) |
3 | | ringcbasALTV.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
4 | 1, 3, 2 | ringcbasALTV 46418 |
. . . 4
β’ (π β π΅ = (π β© Ring)) |
5 | | eqid 2737 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | 1, 3, 2, 5 | ringchomfvalALTV 46419 |
. . . 4
β’ (π β (Hom βπΆ) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ RingHom π¦))) |
7 | | eqidd 2738 |
. . . 4
β’ (π β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π))) = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))) |
8 | 1, 2, 4, 6, 7 | ringcvalALTV 46379 |
. . 3
β’ (π β πΆ = {β¨(Baseβndx), π΅β©, β¨(Hom βndx),
(Hom βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©}) |
9 | 8 | fveq2d 6851 |
. 2
β’ (π β (compβπΆ) =
(compβ{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©})) |
10 | | ringccoALTV.o |
. 2
β’ Β· =
(compβπΆ) |
11 | 3 | fvexi 6861 |
. . . . 5
β’ π΅ β V |
12 | | sqxpexg 7694 |
. . . . 5
β’ (π΅ β V β (π΅ Γ π΅) β V) |
13 | 11, 12 | ax-mp 5 |
. . . 4
β’ (π΅ Γ π΅) β V |
14 | 13, 11 | mpoex 8017 |
. . 3
β’ (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π))) β V |
15 | | catstr 17852 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (Hom
βπΆ)β©,
β¨(compβndx), (π£
β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©} Struct β¨1, ;15β© |
16 | | ccoid 17302 |
. . . 4
β’ comp =
Slot (compβndx) |
17 | | snsstp3 4783 |
. . . 4
β’
{β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©} β {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (Hom βπΆ)β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©} |
18 | 15, 16, 17 | strfv 17083 |
. . 3
β’ ((π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π))) β V β (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π))) = (compβ{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (Hom βπΆ)β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©})) |
19 | 14, 18 | ax-mp 5 |
. 2
β’ (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π))) = (compβ{β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (Hom βπΆ)β©, β¨(compβndx), (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))β©}) |
20 | 9, 10, 19 | 3eqtr4g 2802 |
1
β’ (π β Β· = (π£ β (π΅ Γ π΅), π§ β π΅ β¦ (π β ((2nd βπ£) RingHom π§), π β ((1st βπ£) RingHom (2nd
βπ£)) β¦ (π β π)))) |