Step | Hyp | Ref
| Expression |
1 | | xrge0mulc1cn.k |
. . . . . 6
β’ π½ = ((ordTopβ β€ )
βΎt (0[,]+β)) |
2 | | letopon 22572 |
. . . . . . 7
β’
(ordTopβ β€ ) β
(TopOnββ*) |
3 | | iccssxr 13354 |
. . . . . . 7
β’
(0[,]+β) β β* |
4 | | resttopon 22528 |
. . . . . . 7
β’
(((ordTopβ β€ ) β (TopOnββ*) β§
(0[,]+β) β β*) β ((ordTopβ β€ )
βΎt (0[,]+β)) β
(TopOnβ(0[,]+β))) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . 6
β’
((ordTopβ β€ ) βΎt (0[,]+β)) β
(TopOnβ(0[,]+β)) |
6 | 1, 5 | eqeltri 2834 |
. . . . 5
β’ π½ β
(TopOnβ(0[,]+β)) |
7 | 6 | a1i 11 |
. . . 4
β’ (πΆ = 0 β π½ β
(TopOnβ(0[,]+β))) |
8 | | 0e0iccpnf 13383 |
. . . . 5
β’ 0 β
(0[,]+β) |
9 | 8 | a1i 11 |
. . . 4
β’ (πΆ = 0 β 0 β
(0[,]+β)) |
10 | | simpl 484 |
. . . . . . . . 9
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β πΆ = 0) |
11 | 10 | oveq2d 7378 |
. . . . . . . 8
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β (π₯ Β·e πΆ) = (π₯ Β·e 0)) |
12 | | simpr 486 |
. . . . . . . . . 10
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β π₯ β
(0[,]+β)) |
13 | 3, 12 | sselid 3947 |
. . . . . . . . 9
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β π₯ β
β*) |
14 | | xmul01 13193 |
. . . . . . . . 9
β’ (π₯ β β*
β (π₯
Β·e 0) = 0) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β (π₯ Β·e 0) =
0) |
16 | 11, 15 | eqtrd 2777 |
. . . . . . 7
β’ ((πΆ = 0 β§ π₯ β (0[,]+β)) β (π₯ Β·e πΆ) = 0) |
17 | 16 | mpteq2dva 5210 |
. . . . . 6
β’ (πΆ = 0 β (π₯ β (0[,]+β) β¦ (π₯ Β·e πΆ)) = (π₯ β (0[,]+β) β¦
0)) |
18 | | xrge0mulc1cn.f |
. . . . . 6
β’ πΉ = (π₯ β (0[,]+β) β¦ (π₯ Β·e πΆ)) |
19 | | fconstmpt 5699 |
. . . . . 6
β’
((0[,]+β) Γ {0}) = (π₯ β (0[,]+β) β¦
0) |
20 | 17, 18, 19 | 3eqtr4g 2802 |
. . . . 5
β’ (πΆ = 0 β πΉ = ((0[,]+β) Γ
{0})) |
21 | | c0ex 11156 |
. . . . . 6
β’ 0 β
V |
22 | 21 | fconst2 7159 |
. . . . 5
β’ (πΉ:(0[,]+β)βΆ{0}
β πΉ = ((0[,]+β)
Γ {0})) |
23 | 20, 22 | sylibr 233 |
. . . 4
β’ (πΆ = 0 β πΉ:(0[,]+β)βΆ{0}) |
24 | | cnconst 22651 |
. . . 4
β’ (((π½ β
(TopOnβ(0[,]+β)) β§ π½ β (TopOnβ(0[,]+β))) β§
(0 β (0[,]+β) β§ πΉ:(0[,]+β)βΆ{0})) β πΉ β (π½ Cn π½)) |
25 | 7, 7, 9, 23, 24 | syl22anc 838 |
. . 3
β’ (πΆ = 0 β πΉ β (π½ Cn π½)) |
26 | 25 | adantl 483 |
. 2
β’ ((π β§ πΆ = 0) β πΉ β (π½ Cn π½)) |
27 | | eqid 2737 |
. . . . . . . . 9
β’
(ordTopβ β€ ) = (ordTopβ β€ ) |
28 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ Β·e πΆ) = (π¦ Β·e πΆ)) |
29 | 28 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π₯ β β*
β¦ (π₯
Β·e πΆ)) =
(π¦ β
β* β¦ (π¦ Β·e πΆ)) |
30 | | id 22 |
. . . . . . . . 9
β’ (πΆ β β+
β πΆ β
β+) |
31 | 27, 29, 30 | xrmulc1cn 32551 |
. . . . . . . 8
β’ (πΆ β β+
β (π₯ β
β* β¦ (π₯ Β·e πΆ)) β ((ordTopβ β€ ) Cn
(ordTopβ β€ ))) |
32 | | letopuni 22574 |
. . . . . . . . 9
β’
β* = βͺ (ordTopβ β€
) |
33 | 32 | cnrest 22652 |
. . . . . . . 8
β’ (((π₯ β β*
β¦ (π₯
Β·e πΆ))
β ((ordTopβ β€ ) Cn (ordTopβ β€ )) β§ (0[,]+β)
β β*) β ((π₯ β β* β¦ (π₯ Β·e πΆ)) βΎ (0[,]+β))
β (((ordTopβ β€ ) βΎt (0[,]+β)) Cn
(ordTopβ β€ ))) |
34 | 31, 3, 33 | sylancl 587 |
. . . . . . 7
β’ (πΆ β β+
β ((π₯ β
β* β¦ (π₯ Β·e πΆ)) βΎ (0[,]+β)) β
(((ordTopβ β€ ) βΎt (0[,]+β)) Cn (ordTopβ
β€ ))) |
35 | | resmpt 5996 |
. . . . . . . . 9
β’
((0[,]+β) β β* β ((π₯ β β* β¦ (π₯ Β·e πΆ)) βΎ (0[,]+β)) =
(π₯ β (0[,]+β)
β¦ (π₯
Β·e πΆ))) |
36 | 3, 35 | ax-mp 5 |
. . . . . . . 8
β’ ((π₯ β β*
β¦ (π₯
Β·e πΆ))
βΎ (0[,]+β)) = (π₯ β (0[,]+β) β¦ (π₯ Β·e πΆ)) |
37 | 36, 18 | eqtr4i 2768 |
. . . . . . 7
β’ ((π₯ β β*
β¦ (π₯
Β·e πΆ))
βΎ (0[,]+β)) = πΉ |
38 | 1 | eqcomi 2746 |
. . . . . . . 8
β’
((ordTopβ β€ ) βΎt (0[,]+β)) = π½ |
39 | 38 | oveq1i 7372 |
. . . . . . 7
β’
(((ordTopβ β€ ) βΎt (0[,]+β)) Cn
(ordTopβ β€ )) = (π½
Cn (ordTopβ β€ )) |
40 | 34, 37, 39 | 3eltr3g 2854 |
. . . . . 6
β’ (πΆ β β+
β πΉ β (π½ Cn (ordTopβ β€
))) |
41 | 2 | a1i 11 |
. . . . . . 7
β’ (πΆ β β+
β (ordTopβ β€ ) β
(TopOnββ*)) |
42 | | simpr 486 |
. . . . . . . . . 10
β’ ((πΆ β β+
β§ π₯ β
(0[,]+β)) β π₯
β (0[,]+β)) |
43 | | ioorp 13349 |
. . . . . . . . . . . 12
β’
(0(,)+β) = β+ |
44 | | ioossicc 13357 |
. . . . . . . . . . . 12
β’
(0(,)+β) β (0[,]+β) |
45 | 43, 44 | eqsstrri 3984 |
. . . . . . . . . . 11
β’
β+ β (0[,]+β) |
46 | | simpl 484 |
. . . . . . . . . . 11
β’ ((πΆ β β+
β§ π₯ β
(0[,]+β)) β πΆ
β β+) |
47 | 45, 46 | sselid 3947 |
. . . . . . . . . 10
β’ ((πΆ β β+
β§ π₯ β
(0[,]+β)) β πΆ
β (0[,]+β)) |
48 | | ge0xmulcl 13387 |
. . . . . . . . . 10
β’ ((π₯ β (0[,]+β) β§
πΆ β (0[,]+β))
β (π₯
Β·e πΆ)
β (0[,]+β)) |
49 | 42, 47, 48 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΆ β β+
β§ π₯ β
(0[,]+β)) β (π₯
Β·e πΆ)
β (0[,]+β)) |
50 | 49, 18 | fmptd 7067 |
. . . . . . . 8
β’ (πΆ β β+
β πΉ:(0[,]+β)βΆ(0[,]+β)) |
51 | 50 | frnd 6681 |
. . . . . . 7
β’ (πΆ β β+
β ran πΉ β
(0[,]+β)) |
52 | 3 | a1i 11 |
. . . . . . 7
β’ (πΆ β β+
β (0[,]+β) β β*) |
53 | | cnrest2 22653 |
. . . . . . 7
β’
(((ordTopβ β€ ) β (TopOnββ*) β§
ran πΉ β
(0[,]+β) β§ (0[,]+β) β β*) β (πΉ β (π½ Cn (ordTopβ β€ )) β πΉ β (π½ Cn ((ordTopβ β€ )
βΎt (0[,]+β))))) |
54 | 41, 51, 52, 53 | syl3anc 1372 |
. . . . . 6
β’ (πΆ β β+
β (πΉ β (π½ Cn (ordTopβ β€ ))
β πΉ β (π½ Cn ((ordTopβ β€ )
βΎt (0[,]+β))))) |
55 | 40, 54 | mpbid 231 |
. . . . 5
β’ (πΆ β β+
β πΉ β (π½ Cn ((ordTopβ β€ )
βΎt (0[,]+β)))) |
56 | 1 | oveq2i 7373 |
. . . . 5
β’ (π½ Cn π½) = (π½ Cn ((ordTopβ β€ )
βΎt (0[,]+β))) |
57 | 55, 56 | eleqtrrdi 2849 |
. . . 4
β’ (πΆ β β+
β πΉ β (π½ Cn π½)) |
58 | 57, 43 | eleq2s 2856 |
. . 3
β’ (πΆ β (0(,)+β) β
πΉ β (π½ Cn π½)) |
59 | 58 | adantl 483 |
. 2
β’ ((π β§ πΆ β (0(,)+β)) β πΉ β (π½ Cn π½)) |
60 | | xrge0mulc1cn.c |
. . 3
β’ (π β πΆ β (0[,)+β)) |
61 | | 0xr 11209 |
. . . 4
β’ 0 β
β* |
62 | | pnfxr 11216 |
. . . 4
β’ +β
β β* |
63 | | 0ltpnf 13050 |
. . . 4
β’ 0 <
+β |
64 | | elicoelioo 31723 |
. . . 4
β’ ((0
β β* β§ +β β β* β§ 0
< +β) β (πΆ
β (0[,)+β) β (πΆ = 0 β¨ πΆ β (0(,)+β)))) |
65 | 61, 62, 63, 64 | mp3an 1462 |
. . 3
β’ (πΆ β (0[,)+β) β
(πΆ = 0 β¨ πΆ β
(0(,)+β))) |
66 | 60, 65 | sylib 217 |
. 2
β’ (π β (πΆ = 0 β¨ πΆ β (0(,)+β))) |
67 | 26, 59, 66 | mpjaodan 958 |
1
β’ (π β πΉ β (π½ Cn π½)) |