Step | Hyp | Ref
| Expression |
1 | | oveq1 7368 |
. . . . 5
β’ (π = 0 β (π Β· π₯) = (0 Β· π₯)) |
2 | | tgpmulg.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | | eqid 2733 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
4 | | tgpmulg.t |
. . . . . 6
β’ Β· =
(.gβπΊ) |
5 | 2, 3, 4 | mulg0 18887 |
. . . . 5
β’ (π₯ β π΅ β (0 Β· π₯) = (0gβπΊ)) |
6 | 1, 5 | sylan9eq 2793 |
. . . 4
β’ ((π = 0 β§ π₯ β π΅) β (π Β· π₯) = (0gβπΊ)) |
7 | 6 | mpteq2dva 5209 |
. . 3
β’ (π = 0 β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (0gβπΊ))) |
8 | 7 | eleq1d 2819 |
. 2
β’ (π = 0 β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (0gβπΊ)) β (π½ Cn π½))) |
9 | | oveq1 7368 |
. . . 4
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
10 | 9 | mpteq2dv 5211 |
. . 3
β’ (π = π β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (π Β· π₯))) |
11 | 10 | eleq1d 2819 |
. 2
β’ (π = π β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½))) |
12 | | oveq1 7368 |
. . . 4
β’ (π = (π + 1) β (π Β· π₯) = ((π + 1) Β· π₯)) |
13 | 12 | mpteq2dv 5211 |
. . 3
β’ (π = (π + 1) β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ ((π + 1) Β· π₯))) |
14 | 13 | eleq1d 2819 |
. 2
β’ (π = (π + 1) β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) β (π½ Cn π½))) |
15 | | oveq1 7368 |
. . . 4
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
16 | 15 | mpteq2dv 5211 |
. . 3
β’ (π = π β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (π Β· π₯))) |
17 | 16 | eleq1d 2819 |
. 2
β’ (π = π β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½))) |
18 | | tgpmulg.j |
. . . 4
β’ π½ = (TopOpenβπΊ) |
19 | 18, 2 | tmdtopon 23455 |
. . 3
β’ (πΊ β TopMnd β π½ β (TopOnβπ΅)) |
20 | | tmdmnd 23449 |
. . . 4
β’ (πΊ β TopMnd β πΊ β Mnd) |
21 | 2, 3 | mndidcl 18579 |
. . . 4
β’ (πΊ β Mnd β
(0gβπΊ)
β π΅) |
22 | 20, 21 | syl 17 |
. . 3
β’ (πΊ β TopMnd β
(0gβπΊ)
β π΅) |
23 | 19, 19, 22 | cnmptc 23036 |
. 2
β’ (πΊ β TopMnd β (π₯ β π΅ β¦ (0gβπΊ)) β (π½ Cn π½)) |
24 | | oveq2 7369 |
. . . . 5
β’ (π₯ = π¦ β ((π + 1) Β· π₯) = ((π + 1) Β· π¦)) |
25 | 24 | cbvmptv 5222 |
. . . 4
β’ (π₯ β π΅ β¦ ((π + 1) Β· π₯)) = (π¦ β π΅ β¦ ((π + 1) Β· π¦)) |
26 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
27 | 2, 4, 26 | mulgnn0p1 18895 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π β β0
β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
28 | 20, 27 | syl3an1 1164 |
. . . . . 6
β’ ((πΊ β TopMnd β§ π β β0
β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
29 | 28 | ad4ant124 1174 |
. . . . 5
β’ ((((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
30 | 29 | mpteq2dva 5209 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ ((π + 1) Β· π¦)) = (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦))) |
31 | 25, 30 | eqtrid 2785 |
. . 3
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) = (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦))) |
32 | | simpll 766 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β πΊ β TopMnd) |
33 | 32, 19 | syl 17 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β π½ β (TopOnβπ΅)) |
34 | | oveq2 7369 |
. . . . . 6
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
35 | 34 | cbvmptv 5222 |
. . . . 5
β’ (π₯ β π΅ β¦ (π Β· π₯)) = (π¦ β π΅ β¦ (π Β· π¦)) |
36 | | simpr 486 |
. . . . 5
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
37 | 35, 36 | eqeltrrid 2839 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ (π Β· π¦)) β (π½ Cn π½)) |
38 | 33 | cnmptid 23035 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ π¦) β (π½ Cn π½)) |
39 | 18, 26, 32, 33, 37, 38 | cnmpt1plusg 23461 |
. . 3
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦)) β (π½ Cn π½)) |
40 | 31, 39 | eqeltrd 2834 |
. 2
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) β (π½ Cn π½)) |
41 | 8, 11, 14, 17, 23, 40 | nn0indd 12608 |
1
β’ ((πΊ β TopMnd β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |