Step | Hyp | Ref
| Expression |
1 | | tgptmd 23934 |
. . . 4
β’ (πΊ β TopGrp β πΊ β TopMnd) |
2 | | tgpmulg.j |
. . . . 5
β’ π½ = (TopOpenβπΊ) |
3 | | tgpmulg.t |
. . . . 5
β’ Β· =
(.gβπΊ) |
4 | | tgpmulg.b |
. . . . 5
β’ π΅ = (BaseβπΊ) |
5 | 2, 3, 4 | tmdmulg 23947 |
. . . 4
β’ ((πΊ β TopMnd β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
6 | 1, 5 | sylan 579 |
. . 3
β’ ((πΊ β TopGrp β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
7 | 6 | adantlr 712 |
. 2
β’ (((πΊ β TopGrp β§ π β β€) β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
8 | | simpllr 773 |
. . . . . . . . 9
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β π β β€) |
9 | 8 | zcnd 12668 |
. . . . . . . 8
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β π β β) |
10 | 9 | negnegd 11563 |
. . . . . . 7
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β --π = π) |
11 | 10 | oveq1d 7419 |
. . . . . 6
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (--π Β· π₯) = (π Β· π₯)) |
12 | | eqid 2726 |
. . . . . . . 8
β’
(invgβπΊ) = (invgβπΊ) |
13 | 4, 3, 12 | mulgnegnn 19009 |
. . . . . . 7
β’ ((-π β β β§ π₯ β π΅) β (--π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
14 | 13 | adantll 711 |
. . . . . 6
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (--π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
15 | 11, 14 | eqtr3d 2768 |
. . . . 5
β’ ((((πΊ β TopGrp β§ π β β€) β§ -π β β) β§ π₯ β π΅) β (π Β· π₯) = ((invgβπΊ)β(-π Β· π₯))) |
16 | 15 | mpteq2dva 5241 |
. . . 4
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ ((invgβπΊ)β(-π Β· π₯)))) |
17 | 2, 4 | tgptopon 23937 |
. . . . . 6
β’ (πΊ β TopGrp β π½ β (TopOnβπ΅)) |
18 | 17 | ad2antrr 723 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β π½ β (TopOnβπ΅)) |
19 | 1 | adantr 480 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π β β€) β πΊ β TopMnd) |
20 | | nnnn0 12480 |
. . . . . 6
β’ (-π β β β -π β
β0) |
21 | 2, 3, 4 | tmdmulg 23947 |
. . . . . 6
β’ ((πΊ β TopMnd β§ -π β β0)
β (π₯ β π΅ β¦ (-π Β· π₯)) β (π½ Cn π½)) |
22 | 19, 20, 21 | syl2an 595 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (-π Β· π₯)) β (π½ Cn π½)) |
23 | 2, 12 | tgpinv 23940 |
. . . . . 6
β’ (πΊ β TopGrp β
(invgβπΊ)
β (π½ Cn π½)) |
24 | 23 | ad2antrr 723 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β
(invgβπΊ)
β (π½ Cn π½)) |
25 | 18, 22, 24 | cnmpt11f 23519 |
. . . 4
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ ((invgβπΊ)β(-π Β· π₯))) β (π½ Cn π½)) |
26 | 16, 25 | eqeltrd 2827 |
. . 3
β’ (((πΊ β TopGrp β§ π β β€) β§ -π β β) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
27 | 26 | adantrl 713 |
. 2
β’ (((πΊ β TopGrp β§ π β β€) β§ (π β β β§ -π β β)) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
28 | | simpr 484 |
. . 3
β’ ((πΊ β TopGrp β§ π β β€) β π β
β€) |
29 | | elznn0nn 12573 |
. . 3
β’ (π β β€ β (π β β0 β¨
(π β β β§
-π β
β))) |
30 | 28, 29 | sylib 217 |
. 2
β’ ((πΊ β TopGrp β§ π β β€) β (π β β0 β¨
(π β β β§
-π β
β))) |
31 | 7, 27, 30 | mpjaodan 955 |
1
β’ ((πΊ β TopGrp β§ π β β€) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |