Step | Hyp | Ref
| Expression |
1 | | tgptmd 23453 |
. . . 4
β’ (πΊ β TopGrp β πΊ β TopMnd) |
2 | | tgpmulg.j |
. . . . 5
β’ π½ = (TopOpenβπΊ) |
3 | | tgpmulg.t |
. . . . 5
β’ Β· =
(.gβπΊ) |
4 | | tgpmulg.b |
. . . . 5
β’ π΅ = (BaseβπΊ) |
5 | 2, 3, 4 | tmdmulg 23466 |
. . . 4
β’ ((πΊ β TopMnd β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
6 | 1, 5 | sylan 581 |
. . 3
β’ ((πΊ β TopGrp β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
7 | 6 | adantlr 714 |
. 2
β’ (((πΊ β TopGrp β§ π β β€) β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
8 | | simpllr 775 |
. . . . . . . . 9
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β π β β€) |
9 | 8 | zcnd 12616 |
. . . . . . . 8
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β π β β) |
10 | 9 | negnegd 11511 |
. . . . . . 7
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β --π = π) |
11 | 10 | oveq1d 7376 |
. . . . . 6
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (--π Β· π₯) = (π Β· π₯)) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπΊ) = (invgβπΊ) |
13 | 4, 3, 12 | mulgnegnn 18894 |
. . . . . . 7
β’ ((-π β β β§ π₯ β π΅) β (--π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
14 | 13 | adantll 713 |
. . . . . 6
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (--π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
15 | 11, 14 | eqtr3d 2775 |
. . . . 5
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
16 | 15 | mpteq2dva 5209 |
. . . 4
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ ((invgβπΊ)β(-π Β· π₯)))) |
17 | 2, 4 | tgptopon 23456 |
. . . . . 6
β’ (πΊ β TopGrp β π½ β (TopOnβπ΅)) |
18 | 17 | ad2antrr 725 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β π½ β (TopOnβπ΅)) |
19 | 1 | adantr 482 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β β€) β πΊ β TopMnd) |
20 | | nnnn0 12428 |
. . . . . 6
β’ (-π β β β -π β
β0) |
21 | 2, 3, 4 | tmdmulg 23466 |
. . . . . 6
β’ ((πΊ β TopMnd β§ -π β β0)
β (π₯ β π΅ β¦ (-π Β· π₯)) β (π½ Cn π½)) |
22 | 19, 20, 21 | syl2an 597 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (-π Β· π₯)) β (π½ Cn π½)) |
23 | 2, 12 | tgpinv 23459 |
. . . . . 6
β’ (πΊ β TopGrp β
(invgβπΊ)
β (π½ Cn π½)) |
24 | 23 | ad2antrr 725 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β
(invgβπΊ)
β (π½ Cn π½)) |
25 | 18, 22, 24 | cnmpt11f 23038 |
. . . 4
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ ((invgβπΊ)β(-π Β· π₯))) β (π½ Cn π½)) |
26 | 16, 25 | eqeltrd 2834 |
. . 3
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
27 | 26 | adantrl 715 |
. 2
β’ (((πΊ β TopGrp β§ π β β€) β§ (π β β β§ -π β β)) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
28 | | simpr 486 |
. . 3
β’ ((πΊ β TopGrp β§ π β β€) β π β
β€) |
29 | | elznn0nn 12521 |
. . 3
β’ (π β β€ β (π β β0 β¨
(π β β β§
-π β
β))) |
30 | 28, 29 | sylib 217 |
. 2
β’ ((πΊ β TopGrp β§ π β β€) β (π β β0 β¨
(π β β β§
-π β
β))) |
31 | 7, 27, 30 | mpjaodan 958 |
1
β’ ((πΊ β TopGrp β§ π β β€) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |