Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
2 | 1 | cnprcl 22612 |
. . . . 5
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β π΄ β βͺ π½) |
3 | 2 | a1i 11 |
. . . 4
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β π΄ β βͺ π½)) |
4 | | ghmcnp.j |
. . . . . . . . . 10
β’ π½ = (TopOpenβπΊ) |
5 | | ghmcnp.x |
. . . . . . . . . 10
β’ π = (BaseβπΊ) |
6 | 4, 5 | tmdtopon 23448 |
. . . . . . . . 9
β’ (πΊ β TopMnd β π½ β (TopOnβπ)) |
7 | 6 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β π½ β (TopOnβπ)) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π½ β (TopOnβπ)) |
9 | | simpl2 1193 |
. . . . . . . 8
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π» β TopMnd) |
10 | | ghmcnp.k |
. . . . . . . . 9
β’ πΎ = (TopOpenβπ») |
11 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ») =
(Baseβπ») |
12 | 10, 11 | tmdtopon 23448 |
. . . . . . . 8
β’ (π» β TopMnd β πΎ β
(TopOnβ(Baseβπ»))) |
13 | 9, 12 | syl 17 |
. . . . . . 7
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΎ β (TopOnβ(Baseβπ»))) |
14 | | simpr 486 |
. . . . . . 7
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ β ((π½ CnP πΎ)βπ΄)) |
15 | | cnpf2 22617 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβ(Baseβπ»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆ(Baseβπ»)) |
16 | 8, 13, 14, 15 | syl3anc 1372 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆ(Baseβπ»)) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β πΉ:πβΆ(Baseβπ»)) |
18 | 14 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β πΉ β ((π½ CnP πΎ)βπ΄)) |
19 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) = (π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) |
20 | 19 | mptpreima 6191 |
. . . . . . . . . . . . . 14
β’ (β‘(π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β π¦) = {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} |
21 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π» β TopMnd) |
22 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β πΉ:πβΆ(Baseβπ»)) |
23 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β πΉ β (πΊ GrpHom π»)) |
24 | | ghmgrp1 19015 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ β (πΊ GrpHom π») β πΊ β Grp) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β πΊ β Grp) |
26 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π₯ β π) |
27 | 2 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β βͺ π½) |
28 | | toponuni 22279 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
29 | 8, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π = βͺ π½) |
30 | 27, 29 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β π) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π΄ β π) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(-gβπΊ) = (-gβπΊ) |
33 | 5, 32 | grpsubcl 18832 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β Grp β§ π₯ β π β§ π΄ β π) β (π₯(-gβπΊ)π΄) β π) |
34 | 25, 26, 31, 33 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (π₯(-gβπΊ)π΄) β π) |
35 | 22, 34 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβ(π₯(-gβπΊ)π΄)) β (Baseβπ»)) |
36 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπ») = (+gβπ») |
37 | 19, 11, 36, 10 | tmdlactcn 23469 |
. . . . . . . . . . . . . . . 16
β’ ((π» β TopMnd β§ (πΉβ(π₯(-gβπΊ)π΄)) β (Baseβπ»)) β (π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β (πΎ Cn πΎ)) |
38 | 21, 35, 37 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β (πΎ Cn πΎ)) |
39 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π¦ β πΎ) |
40 | | cnima 22632 |
. . . . . . . . . . . . . . 15
β’ (((π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β (πΎ Cn πΎ) β§ π¦ β πΎ) β (β‘(π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β π¦) β πΎ) |
41 | 38, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (β‘(π€ β (Baseβπ») β¦ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€)) β π¦) β πΎ) |
42 | 20, 41 | eqeltrrid 2839 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} β πΎ) |
43 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πΉβπ΄) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) = ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ΄))) |
44 | 43 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ΄) β (((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ΄)) β π¦)) |
45 | 22, 31 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβπ΄) β (Baseβπ»)) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(-gβπ») = (-gβπ») |
47 | 5, 32, 46 | ghmsub 19021 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (πΊ GrpHom π») β§ π₯ β π β§ π΄ β π) β (πΉβ(π₯(-gβπΊ)π΄)) = ((πΉβπ₯)(-gβπ»)(πΉβπ΄))) |
48 | 23, 26, 31, 47 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβ(π₯(-gβπΊ)π΄)) = ((πΉβπ₯)(-gβπ»)(πΉβπ΄))) |
49 | 48 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ΄)) = (((πΉβπ₯)(-gβπ»)(πΉβπ΄))(+gβπ»)(πΉβπ΄))) |
50 | | ghmgrp2 19016 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β (πΊ GrpHom π») β π» β Grp) |
51 | 23, 50 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π» β Grp) |
52 | 22, 26 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβπ₯) β (Baseβπ»)) |
53 | 11, 36, 46 | grpnpcan 18844 |
. . . . . . . . . . . . . . . . 17
β’ ((π» β Grp β§ (πΉβπ₯) β (Baseβπ») β§ (πΉβπ΄) β (Baseβπ»)) β (((πΉβπ₯)(-gβπ»)(πΉβπ΄))(+gβπ»)(πΉβπ΄)) = (πΉβπ₯)) |
54 | 51, 52, 45, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (((πΉβπ₯)(-gβπ»)(πΉβπ΄))(+gβπ»)(πΉβπ΄)) = (πΉβπ₯)) |
55 | 49, 54 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ΄)) = (πΉβπ₯)) |
56 | | simprrr 781 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβπ₯) β π¦) |
57 | 55, 56 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ΄)) β π¦) |
58 | 44, 45, 57 | elrabd 3648 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (πΉβπ΄) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦}) |
59 | | cnpimaex 22623 |
. . . . . . . . . . . . 13
β’ ((πΉ β ((π½ CnP πΎ)βπ΄) β§ {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} β πΎ β§ (πΉβπ΄) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦}) β βπ§ β π½ (π΄ β π§ β§ (πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦})) |
60 | 18, 42, 58, 59 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β βπ§ β π½ (π΄ β π§ β§ (πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦})) |
61 | | ssrab 4031 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} β ((πΉ β π§) β (Baseβπ») β§ βπ€ β (πΉ β π§)((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦)) |
62 | 61 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} β βπ€ β (πΉ β π§)((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦) |
63 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β πΉ:πβΆ(Baseβπ»)) |
64 | 63 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β πΉ Fn π) |
65 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β π½ β (TopOnβπ)) |
66 | | toponss 22292 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β (TopOnβπ) β§ π§ β π½) β π§ β π) |
67 | 65, 66 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β π§ β π) |
68 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = (πΉβπ£) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) = ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£))) |
69 | 68 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = (πΉβπ£) β (((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦)) |
70 | 69 | ralima 7189 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ Fn π β§ π§ β π) β (βπ€ β (πΉ β π§)((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦ β βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦)) |
71 | 64, 67, 70 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β (βπ€ β (πΉ β π§)((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦ β βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦)) |
72 | 62, 71 | imbitrid 243 |
. . . . . . . . . . . . . 14
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β ((πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦} β βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦)) |
73 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) = (π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) |
74 | 73 | mptpreima 6191 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β π§) = {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} |
75 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΊ β TopMnd) |
76 | 75 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β πΊ β TopMnd) |
77 | 25 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β πΊ β Grp) |
78 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β π΄ β π) |
79 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β π₯ β π) |
80 | 5, 32 | grpsubcl 18832 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ β Grp β§ π΄ β π β§ π₯ β π) β (π΄(-gβπΊ)π₯) β π) |
81 | 77, 78, 79, 80 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β (π΄(-gβπΊ)π₯) β π) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’
(+gβπΊ) = (+gβπΊ) |
83 | 73, 5, 82, 4 | tmdlactcn 23469 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β TopMnd β§ (π΄(-gβπΊ)π₯) β π) β (π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β (π½ Cn π½)) |
84 | 76, 81, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β (π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β (π½ Cn π½)) |
85 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β π§ β π½) |
86 | | cnima 22632 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β (π½ Cn π½) β§ π§ β π½) β (β‘(π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β π§) β π½) |
87 | 84, 85, 86 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β (β‘(π€ β π β¦ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) β π§) β π½) |
88 | 74, 87 | eqeltrrid 2839 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β π½) |
89 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π₯ β ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) = ((π΄(-gβπΊ)π₯)(+gβπΊ)π₯)) |
90 | 89 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π₯ β (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β ((π΄(-gβπΊ)π₯)(+gβπΊ)π₯) β π§)) |
91 | 5, 82, 32 | grpnpcan 18844 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β Grp β§ π΄ β π β§ π₯ β π) β ((π΄(-gβπΊ)π₯)(+gβπΊ)π₯) = π΄) |
92 | 77, 78, 79, 91 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β ((π΄(-gβπΊ)π₯)(+gβπΊ)π₯) = π΄) |
93 | | simprrl 780 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β π΄ β π§) |
94 | 92, 93 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β ((π΄(-gβπΊ)π₯)(+gβπΊ)π₯) β π§) |
95 | 90, 79, 94 | elrabd 3648 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β π₯ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) |
96 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦) |
97 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π£ = ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β (πΉβπ£) = (πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) |
98 | 97 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π£ = ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) = ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)))) |
99 | 98 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π£ = ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β (((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) β π¦)) |
100 | 99 | rspccv 3577 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ£ β
π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦ β (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) β π¦)) |
101 | 96, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) β π¦)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((πΊ β
TopMnd β§ π» β
TopMnd β§ πΉ β
(πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β§ π€ β π) β (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) β π¦)) |
103 | 23 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β πΉ β (πΊ GrpHom π»)) |
104 | 34 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (π₯(-gβπΊ)π΄) β π) |
105 | 103, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β πΊ β Grp) |
106 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β π΄ β π) |
107 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β π₯ β π) |
108 | 105, 106,
107, 80 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (π΄(-gβπΊ)π₯) β π) |
109 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β π€ β π) |
110 | 5, 82 | grpcl 18761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΊ β Grp β§ (π΄(-gβπΊ)π₯) β π β§ π€ β π) β ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π) |
111 | 105, 108,
109, 110 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π) |
112 | 5, 82, 36 | ghmlin 19018 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ β (πΊ GrpHom π») β§ (π₯(-gβπΊ)π΄) β π β§ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π) β (πΉβ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) = ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)))) |
113 | 103, 104,
111, 112 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (πΉβ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) = ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€)))) |
114 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(invgβπΊ) = (invgβπΊ) |
115 | 5, 32, 114 | grpinvsub 18834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΊ β Grp β§ π₯ β π β§ π΄ β π) β ((invgβπΊ)β(π₯(-gβπΊ)π΄)) = (π΄(-gβπΊ)π₯)) |
116 | 105, 107,
106, 115 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((invgβπΊ)β(π₯(-gβπΊ)π΄)) = (π΄(-gβπΊ)π₯)) |
117 | 116 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)((invgβπΊ)β(π₯(-gβπΊ)π΄))) = ((π₯(-gβπΊ)π΄)(+gβπΊ)(π΄(-gβπΊ)π₯))) |
118 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(0gβπΊ) = (0gβπΊ) |
119 | 5, 82, 118, 114 | grprinv 18806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΊ β Grp β§ (π₯(-gβπΊ)π΄) β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)((invgβπΊ)β(π₯(-gβπΊ)π΄))) = (0gβπΊ)) |
120 | 105, 104,
119 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)((invgβπΊ)β(π₯(-gβπΊ)π΄))) = (0gβπΊ)) |
121 | 117, 120 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)(π΄(-gβπΊ)π₯)) = (0gβπΊ)) |
122 | 121 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (((π₯(-gβπΊ)π΄)(+gβπΊ)(π΄(-gβπΊ)π₯))(+gβπΊ)π€) = ((0gβπΊ)(+gβπΊ)π€)) |
123 | 5, 82 | grpass 18762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΊ β Grp β§ ((π₯(-gβπΊ)π΄) β π β§ (π΄(-gβπΊ)π₯) β π β§ π€ β π)) β (((π₯(-gβπΊ)π΄)(+gβπΊ)(π΄(-gβπΊ)π₯))(+gβπΊ)π€) = ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) |
124 | 105, 104,
108, 109, 123 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (((π₯(-gβπΊ)π΄)(+gβπΊ)(π΄(-gβπΊ)π₯))(+gβπΊ)π€) = ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) |
125 | 5, 82, 118 | grplid 18785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΊ β Grp β§ π€ β π) β ((0gβπΊ)(+gβπΊ)π€) = π€) |
126 | 105, 109,
125 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((0gβπΊ)(+gβπΊ)π€) = π€) |
127 | 122, 124,
126 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€)) = π€) |
128 | 127 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β (πΉβ((π₯(-gβπΊ)π΄)(+gβπΊ)((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) = (πΉβπ€)) |
129 | 113, 128 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π€ β π) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) = (πΉβπ€)) |
130 | 129 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((πΊ β
TopMnd β§ π» β
TopMnd β§ πΉ β
(πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β§ π€ β π) β ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) = (πΉβπ€)) |
131 | 130 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((πΊ β
TopMnd β§ π» β
TopMnd β§ πΉ β
(πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β§ π€ β π) β (((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβ((π΄(-gβπΊ)π₯)(+gβπΊ)π€))) β π¦ β (πΉβπ€) β π¦)) |
132 | 102, 131 | sylibd 238 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((πΊ β
TopMnd β§ π» β
TopMnd β§ πΉ β
(πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β§ π€ β π) β (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β (πΉβπ€) β π¦)) |
133 | 132 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β βπ€ β π (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β (πΉβπ€) β π¦)) |
134 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π£ = π€ β (πΉβπ£) = (πΉβπ€)) |
135 | 134 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ = π€ β ((πΉβπ£) β π¦ β (πΉβπ€) β π¦)) |
136 | 135 | ralrab2 3657 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ£ β
{π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} (πΉβπ£) β π¦ β βπ€ β π (((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§ β (πΉβπ€) β π¦)) |
137 | 133, 136 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β βπ£ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} (πΉβπ£) β π¦) |
138 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β πΉ:πβΆ(Baseβπ»)) |
139 | 138 | ffund 6673 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β Fun πΉ) |
140 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . . . 19
β’ {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β π |
141 | 138 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β dom πΉ = π) |
142 | 140, 141 | sseqtrrid 3998 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β dom πΉ) |
143 | | funimass4 6908 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
πΉ β§ {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β dom πΉ) β ((πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦ β βπ£ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} (πΉβπ£) β π¦)) |
144 | 139, 142,
143 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β ((πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦ β βπ£ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} (πΉβπ£) β π¦)) |
145 | 137, 144 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β (πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦) |
146 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β (π₯ β π’ β π₯ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§})) |
147 | | imaeq2 6010 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ = {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β (πΉ β π’) = (πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§})) |
148 | 147 | sseq1d 3976 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β ((πΉ β π’) β π¦ β (πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦)) |
149 | 146, 148 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β ((π₯ β π’ β§ (πΉ β π’) β π¦) β (π₯ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β§ (πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦))) |
150 | 149 | rspcev 3580 |
. . . . . . . . . . . . . . . 16
β’ (({π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β π½ β§ (π₯ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§} β§ (πΉ β {π€ β π β£ ((π΄(-gβπΊ)π₯)(+gβπΊ)π€) β π§}) β π¦)) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦)) |
151 | 88, 95, 145, 150 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ (π§ β π½ β§ (π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦))) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦)) |
152 | 151 | expr 458 |
. . . . . . . . . . . . . 14
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β ((π΄ β π§ β§ βπ£ β π§ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)(πΉβπ£)) β π¦) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))) |
153 | 72, 152 | sylan2d 606 |
. . . . . . . . . . . . 13
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β§ π§ β π½) β ((π΄ β π§ β§ (πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦}) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))) |
154 | 153 | rexlimdva 3149 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β (βπ§ β π½ (π΄ β π§ β§ (πΉ β π§) β {π€ β (Baseβπ») β£ ((πΉβ(π₯(-gβπΊ)π΄))(+gβπ»)π€) β π¦}) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))) |
155 | 60, 154 | mpd 15 |
. . . . . . . . . . 11
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β π β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦))) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦)) |
156 | 155 | anassrs 469 |
. . . . . . . . . 10
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β§ (π¦ β πΎ β§ (πΉβπ₯) β π¦)) β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦)) |
157 | 156 | expr 458 |
. . . . . . . . 9
β’
(((((πΊ β TopMnd
β§ π» β TopMnd β§
πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β§ π¦ β πΎ) β ((πΉβπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))) |
158 | 157 | ralrimiva 3140 |
. . . . . . . 8
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β βπ¦ β πΎ ((πΉβπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))) |
159 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β π½ β (TopOnβπ)) |
160 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β πΎ β (TopOnβ(Baseβπ»))) |
161 | | simpr 486 |
. . . . . . . . 9
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β π₯ β π) |
162 | | iscnp 22604 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβ(Baseβπ»)) β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β (πΉ:πβΆ(Baseβπ») β§ βπ¦ β πΎ ((πΉβπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))))) |
163 | 159, 160,
161, 162 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β (πΉ β ((π½ CnP πΎ)βπ₯) β (πΉ:πβΆ(Baseβπ») β§ βπ¦ β πΎ ((πΉβπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ (πΉ β π’) β π¦))))) |
164 | 17, 158, 163 | mpbir2and 712 |
. . . . . . 7
β’ ((((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β π) β πΉ β ((π½ CnP πΎ)βπ₯)) |
165 | 164 | ralrimiva 3140 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) |
166 | | cncnp 22647 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβ(Baseβπ»))) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆ(Baseβπ») β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
167 | 8, 13, 166 | syl2anc 585 |
. . . . . 6
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆ(Baseβπ») β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
168 | 16, 165, 167 | mpbir2and 712 |
. . . . 5
β’ (((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ β (π½ Cn πΎ)) |
169 | 168 | ex 414 |
. . . 4
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β πΉ β (π½ Cn πΎ))) |
170 | 3, 169 | jcad 514 |
. . 3
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β βͺ π½ β§ πΉ β (π½ Cn πΎ)))) |
171 | 1 | cncnpi 22645 |
. . . 4
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β βͺ π½) β πΉ β ((π½ CnP πΎ)βπ΄)) |
172 | 171 | ancoms 460 |
. . 3
β’ ((π΄ β βͺ π½
β§ πΉ β (π½ Cn πΎ)) β πΉ β ((π½ CnP πΎ)βπ΄)) |
173 | 170, 172 | impbid1 224 |
. 2
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β βͺ π½ β§ πΉ β (π½ Cn πΎ)))) |
174 | 7, 28 | syl 17 |
. . . 4
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β π = βͺ π½) |
175 | 174 | eleq2d 2820 |
. . 3
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (π΄ β π β π΄ β βͺ π½)) |
176 | 175 | anbi1d 631 |
. 2
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β ((π΄ β π β§ πΉ β (π½ Cn πΎ)) β (π΄ β βͺ π½ β§ πΉ β (π½ Cn πΎ)))) |
177 | 173, 176 | bitr4d 282 |
1
β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β π β§ πΉ β (π½ Cn πΎ)))) |