Step | Hyp | Ref
| Expression |
1 | | xpchomfval.t |
. . . 4
β’ π = (πΆ Γc π·) |
2 | | eqid 2733 |
. . . 4
β’
(BaseβπΆ) =
(BaseβπΆ) |
3 | | eqid 2733 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
4 | | xpchomfval.h |
. . . 4
β’ π» = (Hom βπΆ) |
5 | | xpchomfval.j |
. . . 4
β’ π½ = (Hom βπ·) |
6 | | eqid 2733 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
7 | | eqid 2733 |
. . . 4
β’
(compβπ·) =
(compβπ·) |
8 | | simpl 484 |
. . . 4
β’ ((πΆ β V β§ π· β V) β πΆ β V) |
9 | | simpr 486 |
. . . 4
β’ ((πΆ β V β§ π· β V) β π· β V) |
10 | | xpchomfval.y |
. . . . . 6
β’ π΅ = (Baseβπ) |
11 | 1, 2, 3 | xpcbas 18071 |
. . . . . 6
β’
((BaseβπΆ)
Γ (Baseβπ·)) =
(Baseβπ) |
12 | 10, 11 | eqtr4i 2764 |
. . . . 5
β’ π΅ = ((BaseβπΆ) Γ (Baseβπ·)) |
13 | 12 | a1i 11 |
. . . 4
β’ ((πΆ β V β§ π· β V) β π΅ = ((BaseβπΆ) Γ (Baseβπ·))) |
14 | | eqidd 2734 |
. . . 4
β’ ((πΆ β V β§ π· β V) β (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))) |
15 | | eqidd 2734 |
. . . 4
β’ ((πΆ β V β§ π· β V) β (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)(π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))π¦), π β ((π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©)) = (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)(π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))π¦), π β ((π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 13,
14, 15 | xpcval 18070 |
. . 3
β’ ((πΆ β V β§ π· β V) β π = {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π’ β
π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))β©, β¨(compβndx), (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)(π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))π¦), π β ((π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))β©}) |
17 | | catstr 17850 |
. . 3
β’
{β¨(Baseβndx), π΅β©, β¨(Hom βndx), (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))β©, β¨(compβndx), (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)(π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))π¦), π β ((π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))β©} Struct β¨1, ;15β© |
18 | | homid 17298 |
. . 3
β’ Hom =
Slot (Hom βndx) |
19 | | snsstp2 4778 |
. . 3
β’
{β¨(Hom βndx), (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))β©} β {β¨(Baseβndx),
π΅β©, β¨(Hom
βndx), (π’ β
π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))β©, β¨(compβndx), (π₯ β (π΅ Γ π΅), π¦ β π΅ β¦ (π β ((2nd βπ₯)(π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))π¦), π β ((π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπΆ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))β©} |
20 | 10 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
21 | 20, 20 | mpoex 8013 |
. . . 4
β’ (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) β V |
22 | 21 | a1i 11 |
. . 3
β’ ((πΆ β V β§ π· β V) β (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) β V) |
23 | | xpchomfval.k |
. . 3
β’ πΎ = (Hom βπ) |
24 | 16, 17, 18, 19, 22, 23 | strfv3 17082 |
. 2
β’ ((πΆ β V β§ π· β V) β πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))) |
25 | | fnxpc 18069 |
. . . . . . . 8
β’
Γc Fn (V Γ V) |
26 | | fndm 6606 |
. . . . . . . 8
β’ (
Γc Fn (V Γ V) β dom
Γc = (V Γ V)) |
27 | 25, 26 | ax-mp 5 |
. . . . . . 7
β’ dom
Γc = (V Γ V) |
28 | 27 | ndmov 7539 |
. . . . . 6
β’ (Β¬
(πΆ β V β§ π· β V) β (πΆ Γc
π·) =
β
) |
29 | 1, 28 | eqtrid 2785 |
. . . . 5
β’ (Β¬
(πΆ β V β§ π· β V) β π = β
) |
30 | 29 | fveq2d 6847 |
. . . 4
β’ (Β¬
(πΆ β V β§ π· β V) β (Hom
βπ) = (Hom
ββ
)) |
31 | 18 | str0 17066 |
. . . 4
β’ β
=
(Hom ββ
) |
32 | 30, 23, 31 | 3eqtr4g 2798 |
. . 3
β’ (Β¬
(πΆ β V β§ π· β V) β πΎ = β
) |
33 | 29 | fveq2d 6847 |
. . . . . 6
β’ (Β¬
(πΆ β V β§ π· β V) β
(Baseβπ) =
(Baseββ
)) |
34 | | base0 17093 |
. . . . . 6
β’ β
=
(Baseββ
) |
35 | 33, 10, 34 | 3eqtr4g 2798 |
. . . . 5
β’ (Β¬
(πΆ β V β§ π· β V) β π΅ = β
) |
36 | 35 | olcd 873 |
. . . 4
β’ (Β¬
(πΆ β V β§ π· β V) β (π΅ = β
β¨ π΅ = β
)) |
37 | | 0mpo0 7441 |
. . . 4
β’ ((π΅ = β
β¨ π΅ = β
) β (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) = β
) |
38 | 36, 37 | syl 17 |
. . 3
β’ (Β¬
(πΆ β V β§ π· β V) β (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) = β
) |
39 | 32, 38 | eqtr4d 2776 |
. 2
β’ (Β¬
(πΆ β V β§ π· β V) β πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£))))) |
40 | 24, 39 | pm2.61i 182 |
1
β’ πΎ = (π’ β π΅, π£ β π΅ β¦ (((1st βπ’)π»(1st βπ£)) Γ ((2nd βπ’)π½(2nd βπ£)))) |