Step | Hyp | Ref
| Expression |
1 | | oveq1 7415 |
. . . . 5
β’ (π = 0 β (π Β· π₯) = (0 Β· π₯)) |
2 | | tgpmulg.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | | eqid 2732 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
4 | | tgpmulg.t |
. . . . . 6
β’ Β· =
(.gβπΊ) |
5 | 2, 3, 4 | mulg0 18956 |
. . . . 5
β’ (π₯ β π΅ β (0 Β· π₯) = (0gβπΊ)) |
6 | 1, 5 | sylan9eq 2792 |
. . . 4
β’ ((π = 0 β§ π₯ β π΅) β (π Β· π₯) = (0gβπΊ)) |
7 | 6 | mpteq2dva 5248 |
. . 3
β’ (π = 0 β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (0gβπΊ))) |
8 | 7 | eleq1d 2818 |
. 2
β’ (π = 0 β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (0gβπΊ)) β (π½ Cn π½))) |
9 | | oveq1 7415 |
. . . 4
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
10 | 9 | mpteq2dv 5250 |
. . 3
β’ (π = π β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (π Β· π₯))) |
11 | 10 | eleq1d 2818 |
. 2
β’ (π = π β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½))) |
12 | | oveq1 7415 |
. . . 4
β’ (π = (π + 1) β (π Β· π₯) = ((π + 1) Β· π₯)) |
13 | 12 | mpteq2dv 5250 |
. . 3
β’ (π = (π + 1) β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ ((π + 1) Β· π₯))) |
14 | 13 | eleq1d 2818 |
. 2
β’ (π = (π + 1) β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) β (π½ Cn π½))) |
15 | | oveq1 7415 |
. . . 4
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
16 | 15 | mpteq2dv 5250 |
. . 3
β’ (π = π β (π₯ β π΅ β¦ (π Β· π₯)) = (π₯ β π΅ β¦ (π Β· π₯))) |
17 | 16 | eleq1d 2818 |
. 2
β’ (π = π β ((π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½))) |
18 | | tgpmulg.j |
. . . 4
β’ π½ = (TopOpenβπΊ) |
19 | 18, 2 | tmdtopon 23584 |
. . 3
β’ (πΊ β TopMnd β π½ β (TopOnβπ΅)) |
20 | | tmdmnd 23578 |
. . . 4
β’ (πΊ β TopMnd β πΊ β Mnd) |
21 | 2, 3 | mndidcl 18639 |
. . . 4
β’ (πΊ β Mnd β
(0gβπΊ)
β π΅) |
22 | 20, 21 | syl 17 |
. . 3
β’ (πΊ β TopMnd β
(0gβπΊ)
β π΅) |
23 | 19, 19, 22 | cnmptc 23165 |
. 2
β’ (πΊ β TopMnd β (π₯ β π΅ β¦ (0gβπΊ)) β (π½ Cn π½)) |
24 | | oveq2 7416 |
. . . . 5
β’ (π₯ = π¦ β ((π + 1) Β· π₯) = ((π + 1) Β· π¦)) |
25 | 24 | cbvmptv 5261 |
. . . 4
β’ (π₯ β π΅ β¦ ((π + 1) Β· π₯)) = (π¦ β π΅ β¦ ((π + 1) Β· π¦)) |
26 | | eqid 2732 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
27 | 2, 4, 26 | mulgnn0p1 18964 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π β β0
β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
28 | 20, 27 | syl3an1 1163 |
. . . . . 6
β’ ((πΊ β TopMnd β§ π β β0
β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
29 | 28 | ad4ant124 1173 |
. . . . 5
β’ ((((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β§ π¦ β π΅) β ((π + 1) Β· π¦) = ((π Β· π¦)(+gβπΊ)π¦)) |
30 | 29 | mpteq2dva 5248 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ ((π + 1) Β· π¦)) = (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦))) |
31 | 25, 30 | eqtrid 2784 |
. . 3
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) = (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦))) |
32 | | simpll 765 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β πΊ β TopMnd) |
33 | 32, 19 | syl 17 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β π½ β (TopOnβπ΅)) |
34 | | oveq2 7416 |
. . . . . 6
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
35 | 34 | cbvmptv 5261 |
. . . . 5
β’ (π₯ β π΅ β¦ (π Β· π₯)) = (π¦ β π΅ β¦ (π Β· π¦)) |
36 | | simpr 485 |
. . . . 5
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |
37 | 35, 36 | eqeltrrid 2838 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ (π Β· π¦)) β (π½ Cn π½)) |
38 | 33 | cnmptid 23164 |
. . . 4
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ π¦) β (π½ Cn π½)) |
39 | 18, 26, 32, 33, 37, 38 | cnmpt1plusg 23590 |
. . 3
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π¦ β π΅ β¦ ((π Β· π¦)(+gβπΊ)π¦)) β (π½ Cn π½)) |
40 | 31, 39 | eqeltrd 2833 |
. 2
β’ (((πΊ β TopMnd β§ π β β0)
β§ (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) β (π₯ β π΅ β¦ ((π + 1) Β· π₯)) β (π½ Cn π½)) |
41 | 8, 11, 14, 17, 23, 40 | nn0indd 12658 |
1
β’ ((πΊ β TopMnd β§ π β β0)
β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) |