Step | Hyp | Ref
| Expression |
1 | | subgntr.h |
. . . . . . 7
β’ π½ = (TopOpenβπΊ) |
2 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΊ) =
(BaseβπΊ) |
3 | 1, 2 | tgptopon 23456 |
. . . . . 6
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π½ β (TopOnβ(BaseβπΊ))) |
5 | | topontop 22285 |
. . . . 5
β’ (π½ β
(TopOnβ(BaseβπΊ)) β π½ β Top) |
6 | 4, 5 | syl 17 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π½ β Top) |
7 | 2 | subgss 18937 |
. . . . . 6
β’ (π β (SubGrpβπΊ) β π β (BaseβπΊ)) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π β (BaseβπΊ)) |
9 | | toponuni 22286 |
. . . . . 6
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (BaseβπΊ) = βͺ π½) |
10 | 4, 9 | syl 17 |
. . . . 5
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (BaseβπΊ) = βͺ
π½) |
11 | 8, 10 | sseqtrd 3988 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π β βͺ π½) |
12 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
13 | 12 | clsss3 22433 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β βͺ π½) |
14 | 6, 11, 13 | syl2anc 585 |
. . 3
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β βͺ π½) |
15 | 14, 10 | sseqtrrd 3989 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β (BaseβπΊ)) |
16 | 12 | sscls 22430 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½)
β π β
((clsβπ½)βπ)) |
17 | 6, 11, 16 | syl2anc 585 |
. . 3
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π β ((clsβπ½)βπ)) |
18 | | eqid 2733 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
19 | 18 | subg0cl 18944 |
. . . . 5
β’ (π β (SubGrpβπΊ) β
(0gβπΊ)
β π) |
20 | 19 | adantl 483 |
. . . 4
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β
(0gβπΊ)
β π) |
21 | 20 | ne0d 4299 |
. . 3
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π β β
) |
22 | | ssn0 4364 |
. . 3
β’ ((π β ((clsβπ½)βπ) β§ π β β
) β ((clsβπ½)βπ) β β
) |
23 | 17, 21, 22 | syl2anc 585 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β β
) |
24 | | df-ov 7364 |
. . . 4
β’ (π₯(-gβπΊ)π¦) = ((-gβπΊ)ββ¨π₯, π¦β©) |
25 | | opelxpi 5674 |
. . . . . . 7
β’ ((π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ)) β β¨π₯, π¦β© β (((clsβπ½)βπ) Γ ((clsβπ½)βπ))) |
26 | | txcls 22978 |
. . . . . . . . . 10
β’ (((π½ β
(TopOnβ(BaseβπΊ)) β§ π½ β (TopOnβ(BaseβπΊ))) β§ (π β (BaseβπΊ) β§ π β (BaseβπΊ))) β ((clsβ(π½ Γt π½))β(π Γ π)) = (((clsβπ½)βπ) Γ ((clsβπ½)βπ))) |
27 | 4, 4, 8, 8, 26 | syl22anc 838 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβ(π½ Γt π½))β(π Γ π)) = (((clsβπ½)βπ) Γ ((clsβπ½)βπ))) |
28 | | txtopon 22965 |
. . . . . . . . . . . . 13
β’ ((π½ β
(TopOnβ(BaseβπΊ)) β§ π½ β (TopOnβ(BaseβπΊ))) β (π½ Γt π½) β (TopOnβ((BaseβπΊ) Γ (BaseβπΊ)))) |
29 | 4, 4, 28 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π½ Γt π½) β (TopOnβ((BaseβπΊ) Γ (BaseβπΊ)))) |
30 | | topontop 22285 |
. . . . . . . . . . . 12
β’ ((π½ Γt π½) β
(TopOnβ((BaseβπΊ) Γ (BaseβπΊ))) β (π½ Γt π½) β Top) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π½ Γt π½) β Top) |
32 | | cnvimass 6037 |
. . . . . . . . . . . . 13
β’ (β‘(-gβπΊ) β π) β dom (-gβπΊ) |
33 | | tgpgrp 23452 |
. . . . . . . . . . . . . . 15
β’ (πΊ β TopGrp β πΊ β Grp) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β πΊ β Grp) |
35 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(-gβπΊ) = (-gβπΊ) |
36 | 2, 35 | grpsubf 18834 |
. . . . . . . . . . . . . 14
β’ (πΊ β Grp β
(-gβπΊ):((BaseβπΊ) Γ (BaseβπΊ))βΆ(BaseβπΊ)) |
37 | 34, 36 | syl 17 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β
(-gβπΊ):((BaseβπΊ) Γ (BaseβπΊ))βΆ(BaseβπΊ)) |
38 | 32, 37 | fssdm 6692 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (β‘(-gβπΊ) β π) β ((BaseβπΊ) Γ (BaseβπΊ))) |
39 | | toponuni 22286 |
. . . . . . . . . . . . 13
β’ ((π½ Γt π½) β
(TopOnβ((BaseβπΊ) Γ (BaseβπΊ))) β ((BaseβπΊ) Γ (BaseβπΊ)) = βͺ (π½ Γt π½)) |
40 | 29, 39 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((BaseβπΊ) Γ (BaseβπΊ)) = βͺ (π½
Γt π½)) |
41 | 38, 40 | sseqtrd 3988 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (β‘(-gβπΊ) β π) β βͺ
(π½ Γt
π½)) |
42 | 35 | subgsubcl 18947 |
. . . . . . . . . . . . . . . 16
β’ ((π β (SubGrpβπΊ) β§ π₯ β π β§ π¦ β π) β (π₯(-gβπΊ)π¦) β π) |
43 | 42 | 3expb 1121 |
. . . . . . . . . . . . . . 15
β’ ((π β (SubGrpβπΊ) β§ (π₯ β π β§ π¦ β π)) β (π₯(-gβπΊ)π¦) β π) |
44 | 43 | ralrimivva 3194 |
. . . . . . . . . . . . . 14
β’ (π β (SubGrpβπΊ) β βπ₯ β π βπ¦ β π (π₯(-gβπΊ)π¦) β π) |
45 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = β¨π₯, π¦β© β ((-gβπΊ)βπ§) = ((-gβπΊ)ββ¨π₯, π¦β©)) |
46 | 45, 24 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ (π§ = β¨π₯, π¦β© β ((-gβπΊ)βπ§) = (π₯(-gβπΊ)π¦)) |
47 | 46 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π§ = β¨π₯, π¦β© β (((-gβπΊ)βπ§) β π β (π₯(-gβπΊ)π¦) β π)) |
48 | 47 | ralxp 5801 |
. . . . . . . . . . . . . 14
β’
(βπ§ β
(π Γ π)((-gβπΊ)βπ§) β π β βπ₯ β π βπ¦ β π (π₯(-gβπΊ)π¦) β π) |
49 | 44, 48 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β βπ§ β (π Γ π)((-gβπΊ)βπ§) β π) |
50 | 49 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β βπ§ β (π Γ π)((-gβπΊ)βπ§) β π) |
51 | 37 | ffund 6676 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β Fun
(-gβπΊ)) |
52 | | xpss12 5652 |
. . . . . . . . . . . . . . 15
β’ ((π β (BaseβπΊ) β§ π β (BaseβπΊ)) β (π Γ π) β ((BaseβπΊ) Γ (BaseβπΊ))) |
53 | 8, 8, 52 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π Γ π) β ((BaseβπΊ) Γ (BaseβπΊ))) |
54 | 37 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β dom
(-gβπΊ) =
((BaseβπΊ) Γ
(BaseβπΊ))) |
55 | 53, 54 | sseqtrrd 3989 |
. . . . . . . . . . . . 13
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π Γ π) β dom (-gβπΊ)) |
56 | | funimass5 7009 |
. . . . . . . . . . . . 13
β’ ((Fun
(-gβπΊ)
β§ (π Γ π) β dom
(-gβπΊ))
β ((π Γ π) β (β‘(-gβπΊ) β π) β βπ§ β (π Γ π)((-gβπΊ)βπ§) β π)) |
57 | 51, 55, 56 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((π Γ π) β (β‘(-gβπΊ) β π) β βπ§ β (π Γ π)((-gβπΊ)βπ§) β π)) |
58 | 50, 57 | mpbird 257 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (π Γ π) β (β‘(-gβπΊ) β π)) |
59 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ (π½
Γt π½) =
βͺ (π½ Γt π½) |
60 | 59 | clsss 22428 |
. . . . . . . . . . 11
β’ (((π½ Γt π½) β Top β§ (β‘(-gβπΊ) β π) β βͺ
(π½ Γt
π½) β§ (π Γ π) β (β‘(-gβπΊ) β π)) β ((clsβ(π½ Γt π½))β(π Γ π)) β ((clsβ(π½ Γt π½))β(β‘(-gβπΊ) β π))) |
61 | 31, 41, 58, 60 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβ(π½ Γt π½))β(π Γ π)) β ((clsβ(π½ Γt π½))β(β‘(-gβπΊ) β π))) |
62 | 1, 35 | tgpsubcn 23464 |
. . . . . . . . . . . 12
β’ (πΊ β TopGrp β
(-gβπΊ)
β ((π½
Γt π½) Cn
π½)) |
63 | 62 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β
(-gβπΊ)
β ((π½
Γt π½) Cn
π½)) |
64 | 12 | cncls2i 22644 |
. . . . . . . . . . 11
β’
(((-gβπΊ) β ((π½ Γt π½) Cn π½) β§ π β βͺ π½) β ((clsβ(π½ Γt π½))β(β‘(-gβπΊ) β π)) β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
65 | 63, 11, 64 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβ(π½ Γt π½))β(β‘(-gβπΊ) β π)) β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
66 | 61, 65 | sstrd 3958 |
. . . . . . . . 9
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβ(π½ Γt π½))β(π Γ π)) β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
67 | 27, 66 | eqsstrrd 3987 |
. . . . . . . 8
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (((clsβπ½)βπ) Γ ((clsβπ½)βπ)) β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
68 | 67 | sselda 3948 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ β¨π₯, π¦β© β (((clsβπ½)βπ) Γ ((clsβπ½)βπ))) β β¨π₯, π¦β© β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
69 | 25, 68 | sylan2 594 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β β¨π₯, π¦β© β (β‘(-gβπΊ) β ((clsβπ½)βπ))) |
70 | 33 | ad2antrr 725 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β πΊ β Grp) |
71 | | ffn 6672 |
. . . . . . 7
β’
((-gβπΊ):((BaseβπΊ) Γ (BaseβπΊ))βΆ(BaseβπΊ) β (-gβπΊ) Fn ((BaseβπΊ) Γ (BaseβπΊ))) |
72 | | elpreima 7012 |
. . . . . . 7
β’
((-gβπΊ) Fn ((BaseβπΊ) Γ (BaseβπΊ)) β (β¨π₯, π¦β© β (β‘(-gβπΊ) β ((clsβπ½)βπ)) β (β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β ((clsβπ½)βπ)))) |
73 | 70, 36, 71, 72 | 4syl 19 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β (β¨π₯, π¦β© β (β‘(-gβπΊ) β ((clsβπ½)βπ)) β (β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β ((clsβπ½)βπ)))) |
74 | 69, 73 | mpbid 231 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β (β¨π₯, π¦β© β ((BaseβπΊ) Γ (BaseβπΊ)) β§ ((-gβπΊ)ββ¨π₯, π¦β©) β ((clsβπ½)βπ))) |
75 | 74 | simprd 497 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β ((-gβπΊ)ββ¨π₯, π¦β©) β ((clsβπ½)βπ)) |
76 | 24, 75 | eqeltrid 2838 |
. . 3
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β§ (π₯ β ((clsβπ½)βπ) β§ π¦ β ((clsβπ½)βπ))) β (π₯(-gβπΊ)π¦) β ((clsβπ½)βπ)) |
77 | 76 | ralrimivva 3194 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β βπ₯ β ((clsβπ½)βπ)βπ¦ β ((clsβπ½)βπ)(π₯(-gβπΊ)π¦) β ((clsβπ½)βπ)) |
78 | 2, 35 | issubg4 18955 |
. . 3
β’ (πΊ β Grp β
(((clsβπ½)βπ) β (SubGrpβπΊ) β (((clsβπ½)βπ) β (BaseβπΊ) β§ ((clsβπ½)βπ) β β
β§ βπ₯ β ((clsβπ½)βπ)βπ¦ β ((clsβπ½)βπ)(π₯(-gβπΊ)π¦) β ((clsβπ½)βπ)))) |
79 | 34, 78 | syl 17 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β (((clsβπ½)βπ) β (SubGrpβπΊ) β (((clsβπ½)βπ) β (BaseβπΊ) β§ ((clsβπ½)βπ) β β
β§ βπ₯ β ((clsβπ½)βπ)βπ¦ β ((clsβπ½)βπ)(π₯(-gβπΊ)π¦) β ((clsβπ½)βπ)))) |
80 | 15, 23, 77, 79 | mpbir3and 1343 |
1
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β (SubGrpβπΊ)) |