Step | Hyp | Ref
| Expression |
1 | | fco 6742 |
. . . . . . 7
β’ ((π:ran π»βΆran πΎ β§ π:ran πΊβΆran π») β (π β π):ran πΊβΆran πΎ) |
2 | 1 | ancoms 460 |
. . . . . 6
β’ ((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β (π β π):ran πΊβΆran πΎ) |
3 | 2 | ad2ant2r 746 |
. . . . 5
β’ (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β (π β π):ran πΊβΆran πΎ) |
4 | 3 | a1i 11 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β (π β π):ran πΊβΆran πΎ)) |
5 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π:ran πΊβΆran π» β§ π₯ β ran πΊ) β (πβπ₯) β ran π») |
6 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π:ran πΊβΆran π» β§ π¦ β ran πΊ) β (πβπ¦) β ran π») |
7 | 5, 6 | anim12dan 620 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:ran πΊβΆran π» β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((πβπ₯) β ran π» β§ (πβπ¦) β ran π»)) |
8 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π’ = (πβπ₯) β (πβπ’) = (πβ(πβπ₯))) |
9 | 8 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ = (πβπ₯) β ((πβπ’)πΎ(πβπ£)) = ((πβ(πβπ₯))πΎ(πβπ£))) |
10 | | fvoveq1 7432 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ = (πβπ₯) β (πβ(π’π»π£)) = (πβ((πβπ₯)π»π£))) |
11 | 9, 10 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π’ = (πβπ₯) β (((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)) β ((πβ(πβπ₯))πΎ(πβπ£)) = (πβ((πβπ₯)π»π£)))) |
12 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π£ = (πβπ¦) β (πβπ£) = (πβ(πβπ¦))) |
13 | 12 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π£ = (πβπ¦) β ((πβ(πβπ₯))πΎ(πβπ£)) = ((πβ(πβπ₯))πΎ(πβ(πβπ¦)))) |
14 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π£ = (πβπ¦) β ((πβπ₯)π»π£) = ((πβπ₯)π»(πβπ¦))) |
15 | 14 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π£ = (πβπ¦) β (πβ((πβπ₯)π»π£)) = (πβ((πβπ₯)π»(πβπ¦)))) |
16 | 13, 15 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π£ = (πβπ¦) β (((πβ(πβπ₯))πΎ(πβπ£)) = (πβ((πβπ₯)π»π£)) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦))))) |
17 | 11, 16 | rspc2va 3624 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πβπ₯) β ran π» β§ (πβπ¦) β ran π») β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦)))) |
18 | 7, 17 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π:ran πΊβΆran π» β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦)))) |
19 | 18 | an32s 651 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ran πΊβΆran π» β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦)))) |
20 | 19 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦)))) |
21 | 20 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ((πβπ₯)π»(πβπ¦)))) |
22 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β (πβ((πβπ₯)π»(πβπ¦))) = (πβ(πβ(π₯πΊπ¦)))) |
23 | 21, 22 | sylan9eq 2793 |
. . . . . . . . . . . . . . . 16
β’
((((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β§ ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ(πβ(π₯πΊπ¦)))) |
24 | 23 | anasss 468 |
. . . . . . . . . . . . . . 15
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ ((π₯ β ran πΊ β§ π¦ β ran πΊ) β§ ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) β ((πβ(πβπ₯))πΎ(πβ(πβπ¦))) = (πβ(πβ(π₯πΊπ¦)))) |
25 | | fvco3 6991 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:ran πΊβΆran π» β§ π₯ β ran πΊ) β ((π β π)βπ₯) = (πβ(πβπ₯))) |
26 | 25 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((π β π)βπ₯) = (πβ(πβπ₯))) |
27 | | fvco3 6991 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:ran πΊβΆran π» β§ π¦ β ran πΊ) β ((π β π)βπ¦) = (πβ(πβπ¦))) |
28 | 27 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((π β π)βπ¦) = (πβ(πβπ¦))) |
29 | 26, 28 | oveq12d 7427 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β (((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((πβ(πβπ₯))πΎ(πβ(πβπ¦)))) |
30 | 29 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β (((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((πβ(πβπ₯))πΎ(πβ(πβπ¦)))) |
31 | 30 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ ((π₯ β ran πΊ β§ π¦ β ran πΊ) β§ ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) β (((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((πβ(πβπ₯))πΎ(πβ(πβπ¦)))) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ ran πΊ = ran πΊ |
33 | 32 | grpocl 29753 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β GrpOp β§ π₯ β ran πΊ β§ π¦ β ran πΊ) β (π₯πΊπ¦) β ran πΊ) |
34 | 33 | 3expb 1121 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β GrpOp β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β (π₯πΊπ¦) β ran πΊ) |
35 | | fvco3 6991 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:ran πΊβΆran π» β§ (π₯πΊπ¦) β ran πΊ) β ((π β π)β(π₯πΊπ¦)) = (πβ(πβ(π₯πΊπ¦)))) |
36 | 35 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ (π₯πΊπ¦) β ran πΊ) β ((π β π)β(π₯πΊπ¦)) = (πβ(πβ(π₯πΊπ¦)))) |
37 | 34, 36 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ (πΊ β GrpOp β§ (π₯ β ran πΊ β§ π¦ β ran πΊ))) β ((π β π)β(π₯πΊπ¦)) = (πβ(πβ(π₯πΊπ¦)))) |
38 | 37 | anassrs 469 |
. . . . . . . . . . . . . . . 16
β’ ((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β ((π β π)β(π₯πΊπ¦)) = (πβ(πβ(π₯πΊπ¦)))) |
39 | 38 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ ((π₯ β ran πΊ β§ π¦ β ran πΊ) β§ ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) β ((π β π)β(π₯πΊπ¦)) = (πβ(πβ(π₯πΊπ¦)))) |
40 | 24, 31, 39 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ ((π₯ β ran πΊ β§ π¦ β ran πΊ) β§ ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) β (((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))) |
41 | 40 | expr 458 |
. . . . . . . . . . . . 13
β’
(((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ (π₯ β ran πΊ β§ π¦ β ran πΊ)) β (((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β (((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
42 | 41 | ralimdvva 3205 |
. . . . . . . . . . . 12
β’ ((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ πΊ β GrpOp) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
43 | 42 | an32s 651 |
. . . . . . . . . . 11
β’ ((((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β§ πΊ β GrpOp) β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
44 | 43 | ex 414 |
. . . . . . . . . 10
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β (πΊ β GrpOp β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
45 | 44 | com23 86 |
. . . . . . . . 9
β’ (((π:ran πΊβΆran π» β§ π:ran π»βΆran πΎ) β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))) β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β (πΊ β GrpOp β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
46 | 45 | anasss 468 |
. . . . . . . 8
β’ ((π:ran πΊβΆran π» β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β (πΊ β GrpOp β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
47 | 46 | imp 408 |
. . . . . . 7
β’ (((π:ran πΊβΆran π» β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β (πΊ β GrpOp β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
48 | 47 | an32s 651 |
. . . . . 6
β’ (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β (πΊ β GrpOp β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
49 | 48 | com12 32 |
. . . . 5
β’ (πΊ β GrpOp β (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
50 | 49 | 3ad2ant1 1134 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦)))) |
51 | 4, 50 | jcad 514 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β (((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))) β ((π β π):ran πΊβΆran πΎ β§ βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
52 | | eqid 2733 |
. . . . . 6
β’ ran π» = ran π» |
53 | 32, 52 | elghomOLD 36755 |
. . . . 5
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (π β (πΊ GrpOpHom π») β (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
54 | 53 | 3adant3 1133 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β (π β (πΊ GrpOpHom π») β (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
55 | | eqid 2733 |
. . . . . 6
β’ ran πΎ = ran πΎ |
56 | 52, 55 | elghomOLD 36755 |
. . . . 5
β’ ((π» β GrpOp β§ πΎ β GrpOp) β (π β (π» GrpOpHom πΎ) β (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))))) |
57 | 56 | 3adant1 1131 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β (π β (π» GrpOpHom πΎ) β (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£))))) |
58 | 54, 57 | anbi12d 632 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β ((π β (πΊ GrpOpHom π») β§ π β (π» GrpOpHom πΎ)) β ((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β§ (π:ran π»βΆran πΎ β§ βπ’ β ran π»βπ£ β ran π»((πβπ’)πΎ(πβπ£)) = (πβ(π’π»π£)))))) |
59 | 32, 55 | elghomOLD 36755 |
. . . 4
β’ ((πΊ β GrpOp β§ πΎ β GrpOp) β ((π β π) β (πΊ GrpOpHom πΎ) β ((π β π):ran πΊβΆran πΎ β§ βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
60 | 59 | 3adant2 1132 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β ((π β π) β (πΊ GrpOpHom πΎ) β ((π β π):ran πΊβΆran πΎ β§ βπ₯ β ran πΊβπ¦ β ran πΊ(((π β π)βπ₯)πΎ((π β π)βπ¦)) = ((π β π)β(π₯πΊπ¦))))) |
61 | 51, 58, 60 | 3imtr4d 294 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β ((π β (πΊ GrpOpHom π») β§ π β (π» GrpOpHom πΎ)) β (π β π) β (πΊ GrpOpHom πΎ))) |
62 | 61 | imp 408 |
1
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β§ (π β (πΊ GrpOpHom π») β§ π β (π» GrpOpHom πΎ))) β (π β π) β (πΊ GrpOpHom πΎ)) |