Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’ (π΄ Γc
πΆ) = (π΄ Γc πΆ) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ΄) =
(Baseβπ΄) |
3 | | eqid 2733 |
. . 3
β’
(BaseβπΆ) =
(BaseβπΆ) |
4 | | eqid 2733 |
. . 3
β’ (Hom
βπ΄) = (Hom
βπ΄) |
5 | | eqid 2733 |
. . 3
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | | eqid 2733 |
. . 3
β’
(compβπ΄) =
(compβπ΄) |
7 | | eqid 2733 |
. . 3
β’
(compβπΆ) =
(compβπΆ) |
8 | | xpcpropd.a |
. . 3
β’ (π β π΄ β π) |
9 | | xpcpropd.c |
. . 3
β’ (π β πΆ β π) |
10 | | eqidd 2734 |
. . 3
β’ (π β ((Baseβπ΄) Γ (BaseβπΆ)) = ((Baseβπ΄) Γ (BaseβπΆ))) |
11 | 1, 2, 3 | xpcbas 18071 |
. . . . 5
β’
((Baseβπ΄)
Γ (BaseβπΆ)) =
(Baseβ(π΄
Γc πΆ)) |
12 | | eqid 2733 |
. . . . 5
β’ (Hom
β(π΄
Γc πΆ)) = (Hom β(π΄ Γc πΆ)) |
13 | 1, 11, 4, 5, 12 | xpchomfval 18072 |
. . . 4
β’ (Hom
β(π΄
Γc πΆ)) = (π’ β ((Baseβπ΄) Γ (BaseβπΆ)), π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (((1st βπ’)(Hom βπ΄)(1st βπ£)) Γ ((2nd βπ’)(Hom βπΆ)(2nd βπ£)))) |
14 | 13 | a1i 11 |
. . 3
β’ (π β (Hom β(π΄ Γc
πΆ)) = (π’ β ((Baseβπ΄) Γ (BaseβπΆ)), π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (((1st βπ’)(Hom βπ΄)(1st βπ£)) Γ ((2nd βπ’)(Hom βπΆ)(2nd βπ£))))) |
15 | | eqidd 2734 |
. . 3
β’ (π β (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))), π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©)) = (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))), π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((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, 10,
14, 15 | xpcval 18070 |
. 2
β’ (π β (π΄ Γc πΆ) = {β¨(Baseβndx),
((Baseβπ΄) Γ
(BaseβπΆ))β©,
β¨(Hom βndx), (Hom β(π΄ Γc πΆ))β©,
β¨(compβndx), (π₯
β (((Baseβπ΄)
Γ (BaseβπΆ))
Γ ((Baseβπ΄)
Γ (BaseβπΆ))),
π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©))β©}) |
17 | | eqid 2733 |
. . 3
β’ (π΅ Γc
π·) = (π΅ Γc π·) |
18 | | eqid 2733 |
. . 3
β’
(Baseβπ΅) =
(Baseβπ΅) |
19 | | eqid 2733 |
. . 3
β’
(Baseβπ·) =
(Baseβπ·) |
20 | | eqid 2733 |
. . 3
β’ (Hom
βπ΅) = (Hom
βπ΅) |
21 | | eqid 2733 |
. . 3
β’ (Hom
βπ·) = (Hom
βπ·) |
22 | | eqid 2733 |
. . 3
β’
(compβπ΅) =
(compβπ΅) |
23 | | eqid 2733 |
. . 3
β’
(compβπ·) =
(compβπ·) |
24 | | xpcpropd.b |
. . 3
β’ (π β π΅ β π) |
25 | | xpcpropd.d |
. . 3
β’ (π β π· β π) |
26 | | xpcpropd.1 |
. . . . 5
β’ (π β (Homf
βπ΄) =
(Homf βπ΅)) |
27 | 26 | homfeqbas 17581 |
. . . 4
β’ (π β (Baseβπ΄) = (Baseβπ΅)) |
28 | | xpcpropd.3 |
. . . . 5
β’ (π β (Homf
βπΆ) =
(Homf βπ·)) |
29 | 28 | homfeqbas 17581 |
. . . 4
β’ (π β (BaseβπΆ) = (Baseβπ·)) |
30 | 27, 29 | xpeq12d 5665 |
. . 3
β’ (π β ((Baseβπ΄) Γ (BaseβπΆ)) = ((Baseβπ΅) Γ (Baseβπ·))) |
31 | 26 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (Homf
βπ΄) =
(Homf βπ΅)) |
32 | | xp1st 7954 |
. . . . . . . 8
β’ (π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β (1st
βπ’) β
(Baseβπ΄)) |
33 | 32 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (1st βπ’) β (Baseβπ΄)) |
34 | | xp1st 7954 |
. . . . . . . 8
β’ (π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β (1st
βπ£) β
(Baseβπ΄)) |
35 | 34 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (1st βπ£) β (Baseβπ΄)) |
36 | 2, 4, 20, 31, 33, 35 | homfeqval 17582 |
. . . . . 6
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β ((1st βπ’)(Hom βπ΄)(1st βπ£)) = ((1st βπ’)(Hom βπ΅)(1st βπ£))) |
37 | 28 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (Homf
βπΆ) =
(Homf βπ·)) |
38 | | xp2nd 7955 |
. . . . . . . 8
β’ (π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β (2nd
βπ’) β
(BaseβπΆ)) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (2nd βπ’) β (BaseβπΆ)) |
40 | | xp2nd 7955 |
. . . . . . . 8
β’ (π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β (2nd
βπ£) β
(BaseβπΆ)) |
41 | 40 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (2nd βπ£) β (BaseβπΆ)) |
42 | 3, 5, 21, 37, 39, 41 | homfeqval 17582 |
. . . . . 6
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β ((2nd βπ’)(Hom βπΆ)(2nd βπ£)) = ((2nd βπ’)(Hom βπ·)(2nd βπ£))) |
43 | 36, 42 | xpeq12d 5665 |
. . . . 5
β’ ((π β§ π’ β ((Baseβπ΄) Γ (BaseβπΆ)) β§ π£ β ((Baseβπ΄) Γ (BaseβπΆ))) β (((1st βπ’)(Hom βπ΄)(1st βπ£)) Γ ((2nd βπ’)(Hom βπΆ)(2nd βπ£))) = (((1st βπ’)(Hom βπ΅)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£)))) |
44 | 43 | mpoeq3dva 7435 |
. . . 4
β’ (π β (π’ β ((Baseβπ΄) Γ (BaseβπΆ)), π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (((1st βπ’)(Hom βπ΄)(1st βπ£)) Γ ((2nd βπ’)(Hom βπΆ)(2nd βπ£)))) = (π’ β ((Baseβπ΄) Γ (BaseβπΆ)), π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (((1st βπ’)(Hom βπ΅)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))) |
45 | 13, 44 | eqtrid 2785 |
. . 3
β’ (π β (Hom β(π΄ Γc
πΆ)) = (π’ β ((Baseβπ΄) Γ (BaseβπΆ)), π£ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (((1st βπ’)(Hom βπ΅)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ·)(2nd βπ£))))) |
46 | 26 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (Homf
βπ΄) =
(Homf βπ΅)) |
47 | | xpcpropd.2 |
. . . . . . . . . 10
β’ (π β
(compfβπ΄) = (compfβπ΅)) |
48 | 47 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β
(compfβπ΄) = (compfβπ΅)) |
49 | | simp-4r 783 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) |
50 | | xp1st 7954 |
. . . . . . . . . . 11
β’ (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))) β (1st
βπ₯) β
((Baseβπ΄) Γ
(BaseβπΆ))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ))) |
52 | | xp1st 7954 |
. . . . . . . . . 10
β’
((1st βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ)) β (1st
β(1st βπ₯)) β (Baseβπ΄)) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st
β(1st βπ₯)) β (Baseβπ΄)) |
54 | | xp2nd 7955 |
. . . . . . . . . . 11
β’ (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))) β (2nd
βπ₯) β
((Baseβπ΄) Γ
(BaseβπΆ))) |
55 | 49, 54 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ))) |
56 | | xp1st 7954 |
. . . . . . . . . 10
β’
((2nd βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ)) β (1st
β(2nd βπ₯)) β (Baseβπ΄)) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st
β(2nd βπ₯)) β (Baseβπ΄)) |
58 | | simpllr 775 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) |
59 | | xp1st 7954 |
. . . . . . . . . 10
β’ (π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β (1st
βπ¦) β
(Baseβπ΄)) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st βπ¦) β (Baseβπ΄)) |
61 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π β ((Hom β(π΄ Γc πΆ))βπ₯)) |
62 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
63 | 49, 62 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
64 | 63 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((Hom β(π΄ Γc πΆ))βπ₯) = ((Hom β(π΄ Γc πΆ))ββ¨(1st
βπ₯), (2nd
βπ₯)β©)) |
65 | | df-ov 7361 |
. . . . . . . . . . . . 13
β’
((1st βπ₯)(Hom β(π΄ Γc πΆ))(2nd βπ₯)) = ((Hom β(π΄ Γc
πΆ))ββ¨(1st βπ₯), (2nd βπ₯)β©) |
66 | 64, 65 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((Hom β(π΄ Γc πΆ))βπ₯) = ((1st βπ₯)(Hom β(π΄ Γc πΆ))(2nd βπ₯))) |
67 | 1, 11, 4, 5, 12, 51, 55 | xpchom 18073 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((1st βπ₯)(Hom β(π΄ Γc πΆ))(2nd βπ₯)) = (((1st
β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯))) Γ
((2nd β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯))))) |
68 | 66, 67 | eqtrd 2773 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((Hom β(π΄ Γc πΆ))βπ₯) = (((1st β(1st
βπ₯))(Hom βπ΄)(1st
β(2nd βπ₯))) Γ ((2nd
β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯))))) |
69 | 61, 68 | eleqtrd 2836 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π β (((1st
β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯))) Γ
((2nd β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯))))) |
70 | | xp1st 7954 |
. . . . . . . . . 10
β’ (π β (((1st
β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯))) Γ
((2nd β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯)))) β
(1st βπ)
β ((1st β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st βπ) β ((1st
β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯)))) |
72 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) |
73 | 1, 11, 4, 5, 12, 55, 58 | xpchom 18073 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦) = (((1st β(2nd
βπ₯))(Hom βπ΄)(1st βπ¦)) Γ ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦)))) |
74 | 72, 73 | eleqtrd 2836 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β π β (((1st
β(2nd βπ₯))(Hom βπ΄)(1st βπ¦)) Γ ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦)))) |
75 | | xp1st 7954 |
. . . . . . . . . 10
β’ (π β (((1st
β(2nd βπ₯))(Hom βπ΄)(1st βπ¦)) Γ ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦))) β (1st βπ) β ((1st
β(2nd βπ₯))(Hom βπ΄)(1st βπ¦))) |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (1st βπ) β ((1st
β(2nd βπ₯))(Hom βπ΄)(1st βπ¦))) |
77 | 2, 4, 6, 22, 46, 48, 53, 57, 60, 71, 76 | comfeqval 17593 |
. . . . . . . 8
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)) = ((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ))) |
78 | 28 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (Homf
βπΆ) =
(Homf βπ·)) |
79 | | xpcpropd.4 |
. . . . . . . . . 10
β’ (π β
(compfβπΆ) = (compfβπ·)) |
80 | 79 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β
(compfβπΆ) = (compfβπ·)) |
81 | | xp2nd 7955 |
. . . . . . . . . 10
β’
((1st βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ)) β (2nd
β(1st βπ₯)) β (BaseβπΆ)) |
82 | 51, 81 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd
β(1st βπ₯)) β (BaseβπΆ)) |
83 | | xp2nd 7955 |
. . . . . . . . . 10
β’
((2nd βπ₯) β ((Baseβπ΄) Γ (BaseβπΆ)) β (2nd
β(2nd βπ₯)) β (BaseβπΆ)) |
84 | 55, 83 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd
β(2nd βπ₯)) β (BaseβπΆ)) |
85 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β (2nd
βπ¦) β
(BaseβπΆ)) |
86 | 58, 85 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd βπ¦) β (BaseβπΆ)) |
87 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π β (((1st
β(1st βπ₯))(Hom βπ΄)(1st β(2nd
βπ₯))) Γ
((2nd β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯)))) β
(2nd βπ)
β ((2nd β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯)))) |
88 | 69, 87 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd βπ) β ((2nd
β(1st βπ₯))(Hom βπΆ)(2nd β(2nd
βπ₯)))) |
89 | | xp2nd 7955 |
. . . . . . . . . 10
β’ (π β (((1st
β(2nd βπ₯))(Hom βπ΄)(1st βπ¦)) Γ ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦))) β (2nd βπ) β ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦))) |
90 | 74, 89 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β (2nd βπ) β ((2nd
β(2nd βπ₯))(Hom βπΆ)(2nd βπ¦))) |
91 | 3, 5, 7, 23, 78, 80, 82, 84, 86, 88, 90 | comfeqval 17593 |
. . . . . . . 8
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ)) = ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))) |
92 | 77, 91 | opeq12d 4839 |
. . . . . . 7
β’
(((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦)) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β© = β¨((1st
βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©) |
93 | 92 | 3impa 1111 |
. . . . . 6
β’ ((((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β§ π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦) β§ π β ((Hom β(π΄ Γc πΆ))βπ₯)) β β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β© = β¨((1st
βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©) |
94 | 93 | mpoeq3dva 7435 |
. . . . 5
β’ (((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ)))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©) = (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©)) |
95 | 94 | 3impa 1111 |
. . . 4
β’ ((π β§ π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))) β§ π¦ β ((Baseβπ΄) Γ (BaseβπΆ))) β (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©) = (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©)) |
96 | 95 | mpoeq3dva 7435 |
. . 3
β’ (π β (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))), π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©)) = (π₯ β (((Baseβπ΄) Γ (BaseβπΆ)) Γ ((Baseβπ΄) Γ (BaseβπΆ))), π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΅)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ·)(2nd βπ¦))(2nd βπ))β©))) |
97 | 17, 18, 19, 20, 21, 22, 23, 24, 25, 30, 45, 96 | xpcval 18070 |
. 2
β’ (π β (π΅ Γc π·) = {β¨(Baseβndx),
((Baseβπ΄) Γ
(BaseβπΆ))β©,
β¨(Hom βndx), (Hom β(π΄ Γc πΆ))β©,
β¨(compβndx), (π₯
β (((Baseβπ΄)
Γ (BaseβπΆ))
Γ ((Baseβπ΄)
Γ (BaseβπΆ))),
π¦ β ((Baseβπ΄) Γ (BaseβπΆ)) β¦ (π β ((2nd βπ₯)(Hom β(π΄ Γc πΆ))π¦), π β ((Hom β(π΄ Γc πΆ))βπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ΄)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπΆ)(2nd βπ¦))(2nd βπ))β©))β©}) |
98 | 16, 97 | eqtr4d 2776 |
1
β’ (π β (π΄ Γc πΆ) = (π΅ Γc π·)) |