Step | Hyp | Ref
| Expression |
1 | | 3simpa 1149 |
. 2
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)))) |
2 | | simp3 1139 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) |
3 | 2 | eqcomd 2739 |
. 2
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) |
4 | | initoeu2lem.x |
. . 3
β’ π = (BaseβπΆ) |
5 | | eqid 2733 |
. . 3
β’
(InvβπΆ) =
(InvβπΆ) |
6 | | initoeu1.c |
. . . . 5
β’ (π β πΆ β Cat) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β πΆ β Cat) |
8 | 7 | adantr 482 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΆ β Cat) |
9 | | simpr1 1195 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β π΄ β π) |
10 | 9 | adantr 482 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β π΄ β π) |
11 | | simpr2 1196 |
. . . 4
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β π΅ β π) |
12 | 11 | adantr 482 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β π΅ β π) |
13 | | simplr3 1218 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β π· β π) |
14 | | initoeu2lem.i |
. . . . . . . 8
β’ πΌ = (IsoβπΆ) |
15 | 14 | oveqi 7422 |
. . . . . . 7
β’ (π΅πΌπ΄) = (π΅(IsoβπΆ)π΄) |
16 | 15 | eleq2i 2826 |
. . . . . 6
β’ (πΎ β (π΅πΌπ΄) β πΎ β (π΅(IsoβπΆ)π΄)) |
17 | 16 | biimpi 215 |
. . . . 5
β’ (πΎ β (π΅πΌπ΄) β πΎ β (π΅(IsoβπΆ)π΄)) |
18 | 17 | 3ad2ant1 1134 |
. . . 4
β’ ((πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β πΎ β (π΅(IsoβπΆ)π΄)) |
19 | 18 | adantl 483 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΎ β (π΅(IsoβπΆ)π΄)) |
20 | | initoeu2lem.h |
. . . . . . . 8
β’ π» = (Hom βπΆ) |
21 | 20 | oveqi 7422 |
. . . . . . 7
β’ (π΅π»π·) = (π΅(Hom βπΆ)π·) |
22 | 21 | eleq2i 2826 |
. . . . . 6
β’ (πΊ β (π΅π»π·) β πΊ β (π΅(Hom βπΆ)π·)) |
23 | 22 | biimpi 215 |
. . . . 5
β’ (πΊ β (π΅π»π·) β πΊ β (π΅(Hom βπΆ)π·)) |
24 | 23 | 3ad2ant3 1136 |
. . . 4
β’ ((πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β πΊ β (π΅(Hom βπΆ)π·)) |
25 | 24 | adantl 483 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΊ β (π΅(Hom βπΆ)π·)) |
26 | | eqid 2733 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
27 | | initoeu2lem.o |
. . . 4
β’ β¬ =
(compβπΆ) |
28 | 4, 26, 14, 7, 11, 9 | isohom 17723 |
. . . . . . . 8
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β (π΅πΌπ΄) β (π΅(Hom βπΆ)π΄)) |
29 | 28 | sseld 3982 |
. . . . . . 7
β’ ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β (πΎ β (π΅πΌπ΄) β πΎ β (π΅(Hom βπΆ)π΄))) |
30 | 29 | com12 32 |
. . . . . 6
β’ (πΎ β (π΅πΌπ΄) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β πΎ β (π΅(Hom βπΆ)π΄))) |
31 | 30 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β ((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β πΎ β (π΅(Hom βπΆ)π΄))) |
32 | 31 | impcom 409 |
. . . 4
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΎ β (π΅(Hom βπΆ)π΄)) |
33 | 20 | oveqi 7422 |
. . . . . . . 8
β’ (π΄π»π·) = (π΄(Hom βπΆ)π·) |
34 | 33 | eleq2i 2826 |
. . . . . . 7
β’ (πΉ β (π΄π»π·) β πΉ β (π΄(Hom βπΆ)π·)) |
35 | 34 | biimpi 215 |
. . . . . 6
β’ (πΉ β (π΄π»π·) β πΉ β (π΄(Hom βπΆ)π·)) |
36 | 35 | 3ad2ant2 1135 |
. . . . 5
β’ ((πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β πΉ β (π΄(Hom βπΆ)π·)) |
37 | 36 | adantl 483 |
. . . 4
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β πΉ β (π΄(Hom βπΆ)π·)) |
38 | 4, 26, 27, 8, 12, 10, 13, 32, 37 | catcocl 17629 |
. . 3
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β (πΉ(β¨π΅, π΄β© β¬ π·)πΎ) β (π΅(Hom βπΆ)π·)) |
39 | | eqid 2733 |
. . 3
β’ ((π΅(InvβπΆ)π΄)βπΎ) = ((π΅(InvβπΆ)π΄)βπΎ) |
40 | 27 | oveqi 7422 |
. . 3
β’
(β¨π΄, π΅β© β¬ π·) = (β¨π΄, π΅β©(compβπΆ)π·) |
41 | 4, 5, 8, 10, 12, 13, 19, 25, 38, 39, 40 | rcaninv 17741 |
. 2
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·))) β ((πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ))) |
42 | 1, 3, 41 | sylc 65 |
1
β’ (((π β§ (π΄ β π β§ π΅ β π β§ π· β π)) β§ (πΎ β (π΅πΌπ΄) β§ πΉ β (π΄π»π·) β§ πΊ β (π΅π»π·)) β§ ((πΉ(β¨π΅, π΄β© β¬ π·)πΎ)(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ)) = (πΊ(β¨π΄, π΅β© β¬ π·)((π΅(InvβπΆ)π΄)βπΎ))) β πΊ = (πΉ(β¨π΅, π΄β© β¬ π·)πΎ)) |