Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
β’ (π β π β β) |
2 | | poimir.i |
. . 3
β’ πΌ = ((0[,]1) βm
(1...π)) |
3 | | poimir.r |
. . 3
β’ π
=
(βtβ((1...π) Γ {(topGenβran
(,))})) |
4 | | elmapfn 8858 |
. . . . . . . 8
β’ (π₯ β ((0[,]1)
βm (1...π))
β π₯ Fn (1...π)) |
5 | 4, 2 | eleq2s 2851 |
. . . . . . 7
β’ (π₯ β πΌ β π₯ Fn (1...π)) |
6 | 5 | adantl 482 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β π₯ Fn (1...π)) |
7 | | broucube.1 |
. . . . . . . . 9
β’ (π β πΉ β ((π
βΎt πΌ) Cn (π
βΎt πΌ))) |
8 | | ovex 7441 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
9 | | retopon 24279 |
. . . . . . . . . . . . 13
β’
(topGenβran (,)) β (TopOnββ) |
10 | 3 | pttoponconst 23100 |
. . . . . . . . . . . . 13
β’
(((1...π) β V
β§ (topGenβran (,)) β (TopOnββ)) β π
β (TopOnβ(β
βm (1...π)))) |
11 | 8, 9, 10 | mp2an 690 |
. . . . . . . . . . . 12
β’ π
β (TopOnβ(β
βm (1...π))) |
12 | | reex 11200 |
. . . . . . . . . . . . . 14
β’ β
β V |
13 | | unitssre 13475 |
. . . . . . . . . . . . . 14
β’ (0[,]1)
β β |
14 | | mapss 8882 |
. . . . . . . . . . . . . 14
β’ ((β
β V β§ (0[,]1) β β) β ((0[,]1) βm
(1...π)) β (β
βm (1...π))) |
15 | 12, 13, 14 | mp2an 690 |
. . . . . . . . . . . . 13
β’ ((0[,]1)
βm (1...π))
β (β βm (1...π)) |
16 | 2, 15 | eqsstri 4016 |
. . . . . . . . . . . 12
β’ πΌ β (β
βm (1...π)) |
17 | | resttopon 22664 |
. . . . . . . . . . . 12
β’ ((π
β (TopOnβ(β
βm (1...π))) β§ πΌ β (β βm
(1...π))) β (π
βΎt πΌ) β (TopOnβπΌ)) |
18 | 11, 16, 17 | mp2an 690 |
. . . . . . . . . . 11
β’ (π
βΎt πΌ) β (TopOnβπΌ) |
19 | 18 | toponunii 22417 |
. . . . . . . . . 10
β’ πΌ = βͺ
(π
βΎt
πΌ) |
20 | 19, 19 | cnf 22749 |
. . . . . . . . 9
β’ (πΉ β ((π
βΎt πΌ) Cn (π
βΎt πΌ)) β πΉ:πΌβΆπΌ) |
21 | 7, 20 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:πΌβΆπΌ) |
22 | 21 | ffvelcdmda 7086 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) β πΌ) |
23 | | elmapfn 8858 |
. . . . . . . 8
β’ ((πΉβπ₯) β ((0[,]1) βm
(1...π)) β (πΉβπ₯) Fn (1...π)) |
24 | 23, 2 | eleq2s 2851 |
. . . . . . 7
β’ ((πΉβπ₯) β πΌ β (πΉβπ₯) Fn (1...π)) |
25 | 22, 24 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯) Fn (1...π)) |
26 | | ovexd 7443 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (1...π) β V) |
27 | | inidm 4218 |
. . . . . 6
β’
((1...π) β©
(1...π)) = (1...π) |
28 | | eqidd 2733 |
. . . . . 6
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β (π₯βπ) = (π₯βπ)) |
29 | | eqidd 2733 |
. . . . . 6
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β ((πΉβπ₯)βπ) = ((πΉβπ₯)βπ)) |
30 | 6, 25, 26, 26, 27, 28, 29 | offval 7678 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (π₯ βf β (πΉβπ₯)) = (π β (1...π) β¦ ((π₯βπ) β ((πΉβπ₯)βπ)))) |
31 | 30 | mpteq2dva 5248 |
. . . 4
β’ (π β (π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯))) = (π₯ β πΌ β¦ (π β (1...π) β¦ ((π₯βπ) β ((πΉβπ₯)βπ))))) |
32 | 18 | a1i 11 |
. . . . 5
β’ (π β (π
βΎt πΌ) β (TopOnβπΌ)) |
33 | | ovexd 7443 |
. . . . 5
β’ (π β (1...π) β V) |
34 | | retop 24277 |
. . . . . . 7
β’
(topGenβran (,)) β Top |
35 | 34 | fconst6 6781 |
. . . . . 6
β’
((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop |
36 | 35 | a1i 11 |
. . . . 5
β’ (π β ((1...π) Γ {(topGenβran
(,))}):(1...π)βΆTop) |
37 | 18 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π
βΎt πΌ) β (TopOnβπΌ)) |
38 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) =
(TopOpenββfld) |
39 | 38 | cnfldtop 24299 |
. . . . . . . . . . 11
β’
(TopOpenββfld) β Top |
40 | | cnrest2r 22790 |
. . . . . . . . . . 11
β’
((TopOpenββfld) β Top β ((π
βΎt πΌ) Cn
((TopOpenββfld) βΎt β)) β
((π
βΎt
πΌ) Cn
(TopOpenββfld))) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π
βΎt πΌ) Cn
((TopOpenββfld) βΎt β)) β
((π
βΎt
πΌ) Cn
(TopOpenββfld)) |
42 | | resmpt 6037 |
. . . . . . . . . . . . 13
β’ (πΌ β (β
βm (1...π))
β ((π₯ β (β
βm (1...π))
β¦ (π₯βπ)) βΎ πΌ) = (π₯ β πΌ β¦ (π₯βπ))) |
43 | 16, 42 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π₯ β (β
βm (1...π))
β¦ (π₯βπ)) βΎ πΌ) = (π₯ β πΌ β¦ (π₯βπ)) |
44 | 11 | toponunii 22417 |
. . . . . . . . . . . . . . 15
β’ (β
βm (1...π))
= βͺ π
|
45 | 44, 3 | ptpjcn 23114 |
. . . . . . . . . . . . . 14
β’
(((1...π) β V
β§ ((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop β§ π β (1...π)) β (π₯ β (β βm
(1...π)) β¦ (π₯βπ)) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
46 | 8, 35, 45 | mp3an12 1451 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β (π₯ β (β βm
(1...π)) β¦ (π₯βπ)) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
47 | 44 | cnrest 22788 |
. . . . . . . . . . . . 13
β’ (((π₯ β (β
βm (1...π))
β¦ (π₯βπ)) β (π
Cn (((1...π) Γ {(topGenβran
(,))})βπ)) β§
πΌ β (β
βm (1...π))) β ((π₯ β (β βm
(1...π)) β¦ (π₯βπ)) βΎ πΌ) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
48 | 46, 16, 47 | sylancl 586 |
. . . . . . . . . . . 12
β’ (π β (1...π) β ((π₯ β (β βm
(1...π)) β¦ (π₯βπ)) βΎ πΌ) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
49 | 43, 48 | eqeltrrid 2838 |
. . . . . . . . . . 11
β’ (π β (1...π) β (π₯ β πΌ β¦ (π₯βπ)) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
50 | | fvex 6904 |
. . . . . . . . . . . . . 14
β’
(topGenβran (,)) β V |
51 | 50 | fvconst2 7204 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β (((1...π) Γ {(topGenβran
(,))})βπ) =
(topGenβran (,))) |
52 | 38 | tgioo2 24318 |
. . . . . . . . . . . . 13
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
53 | 51, 52 | eqtrdi 2788 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (((1...π) Γ {(topGenβran
(,))})βπ) =
((TopOpenββfld) βΎt
β)) |
54 | 53 | oveq2d 7424 |
. . . . . . . . . . 11
β’ (π β (1...π) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ)) = ((π
βΎt πΌ) Cn
((TopOpenββfld) βΎt
β))) |
55 | 49, 54 | eleqtrd 2835 |
. . . . . . . . . 10
β’ (π β (1...π) β (π₯ β πΌ β¦ (π₯βπ)) β ((π
βΎt πΌ) Cn ((TopOpenββfld)
βΎt β))) |
56 | 41, 55 | sselid 3980 |
. . . . . . . . 9
β’ (π β (1...π) β (π₯ β πΌ β¦ (π₯βπ)) β ((π
βΎt πΌ) Cn
(TopOpenββfld))) |
57 | 56 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ (π₯βπ)) β ((π
βΎt πΌ) Cn
(TopOpenββfld))) |
58 | 21 | feqmptd 6960 |
. . . . . . . . . . 11
β’ (π β πΉ = (π₯ β πΌ β¦ (πΉβπ₯))) |
59 | 58, 7 | eqeltrrd 2834 |
. . . . . . . . . 10
β’ (π β (π₯ β πΌ β¦ (πΉβπ₯)) β ((π
βΎt πΌ) Cn (π
βΎt πΌ))) |
60 | 59 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ (πΉβπ₯)) β ((π
βΎt πΌ) Cn (π
βΎt πΌ))) |
61 | | fveq1 6890 |
. . . . . . . . . . 11
β’ (π₯ = π§ β (π₯βπ) = (π§βπ)) |
62 | 61 | cbvmptv 5261 |
. . . . . . . . . 10
β’ (π₯ β πΌ β¦ (π₯βπ)) = (π§ β πΌ β¦ (π§βπ)) |
63 | 62, 57 | eqeltrrid 2838 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (π§ β πΌ β¦ (π§βπ)) β ((π
βΎt πΌ) Cn
(TopOpenββfld))) |
64 | | fveq1 6890 |
. . . . . . . . 9
β’ (π§ = (πΉβπ₯) β (π§βπ) = ((πΉβπ₯)βπ)) |
65 | 37, 60, 37, 63, 64 | cnmpt11 23166 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((πΉβπ₯)βπ)) β ((π
βΎt πΌ) Cn
(TopOpenββfld))) |
66 | 38 | subcn 24381 |
. . . . . . . . 9
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
67 | 66 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β β β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
68 | 37, 57, 65, 67 | cnmpt12f 23169 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn
(TopOpenββfld))) |
69 | | elmapi 8842 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ((0[,]1)
βm (1...π))
β π₯:(1...π)βΆ(0[,]1)) |
70 | 69, 2 | eleq2s 2851 |
. . . . . . . . . . . . . 14
β’ (π₯ β πΌ β π₯:(1...π)βΆ(0[,]1)) |
71 | 70 | ffvelcdmda 7086 |
. . . . . . . . . . . . 13
β’ ((π₯ β πΌ β§ π β (1...π)) β (π₯βπ) β (0[,]1)) |
72 | 13, 71 | sselid 3980 |
. . . . . . . . . . . 12
β’ ((π₯ β πΌ β§ π β (1...π)) β (π₯βπ) β β) |
73 | 72 | adantll 712 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β (π₯βπ) β β) |
74 | | elmapi 8842 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ₯) β ((0[,]1) βm
(1...π)) β (πΉβπ₯):(1...π)βΆ(0[,]1)) |
75 | 74, 2 | eleq2s 2851 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) β πΌ β (πΉβπ₯):(1...π)βΆ(0[,]1)) |
76 | 22, 75 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΌ) β (πΉβπ₯):(1...π)βΆ(0[,]1)) |
77 | 76 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β ((πΉβπ₯)βπ) β (0[,]1)) |
78 | 13, 77 | sselid 3980 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β ((πΉβπ₯)βπ) β β) |
79 | 73, 78 | resubcld 11641 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΌ) β§ π β (1...π)) β ((π₯βπ) β ((πΉβπ₯)βπ)) β β) |
80 | 79 | an32s 650 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π₯ β πΌ) β ((π₯βπ) β ((πΉβπ₯)βπ)) β β) |
81 | 80 | fmpttd 7114 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))):πΌβΆβ) |
82 | | frn 6724 |
. . . . . . . 8
β’ ((π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))):πΌβΆβ β ran (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β β) |
83 | 38 | cnfldtopon 24298 |
. . . . . . . . 9
β’
(TopOpenββfld) β
(TopOnββ) |
84 | | ax-resscn 11166 |
. . . . . . . . 9
β’ β
β β |
85 | | cnrest2 22789 |
. . . . . . . . 9
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β β β§ β β
β) β ((π₯ β
πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn (TopOpenββfld))
β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn ((TopOpenββfld)
βΎt β)))) |
86 | 83, 84, 85 | mp3an13 1452 |
. . . . . . . 8
β’ (ran
(π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β β β ((π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn (TopOpenββfld))
β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn ((TopOpenββfld)
βΎt β)))) |
87 | 81, 82, 86 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn (TopOpenββfld))
β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn ((TopOpenββfld)
βΎt β)))) |
88 | 68, 87 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn ((TopOpenββfld)
βΎt β))) |
89 | 54 | adantl 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ)) = ((π
βΎt πΌ) Cn
((TopOpenββfld) βΎt
β))) |
90 | 88, 89 | eleqtrrd 2836 |
. . . . 5
β’ ((π β§ π β (1...π)) β (π₯ β πΌ β¦ ((π₯βπ) β ((πΉβπ₯)βπ))) β ((π
βΎt πΌ) Cn (((1...π) Γ {(topGenβran
(,))})βπ))) |
91 | 3, 32, 33, 36, 90 | ptcn 23130 |
. . . 4
β’ (π β (π₯ β πΌ β¦ (π β (1...π) β¦ ((π₯βπ) β ((πΉβπ₯)βπ)))) β ((π
βΎt πΌ) Cn π
)) |
92 | 31, 91 | eqeltrd 2833 |
. . 3
β’ (π β (π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯))) β ((π
βΎt πΌ) Cn π
)) |
93 | | simpr2 1195 |
. . . . . 6
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β π§ β πΌ) |
94 | | id 22 |
. . . . . . . . 9
β’ (π₯ = π§ β π₯ = π§) |
95 | | fveq2 6891 |
. . . . . . . . 9
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
96 | 94, 95 | oveq12d 7426 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ βf β (πΉβπ₯)) = (π§ βf β (πΉβπ§))) |
97 | | eqid 2732 |
. . . . . . . 8
β’ (π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯))) = (π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯))) |
98 | | ovex 7441 |
. . . . . . . 8
β’ (π§ βf β
(πΉβπ§)) β V |
99 | 96, 97, 98 | fvmpt 6998 |
. . . . . . 7
β’ (π§ β πΌ β ((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§) = (π§ βf β (πΉβπ§))) |
100 | 99 | fveq1d 6893 |
. . . . . 6
β’ (π§ β πΌ β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) = ((π§ βf β (πΉβπ§))βπ)) |
101 | 93, 100 | syl 17 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) = ((π§ βf β (πΉβπ§))βπ)) |
102 | | elmapfn 8858 |
. . . . . . . . . . . 12
β’ (π§ β ((0[,]1)
βm (1...π))
β π§ Fn (1...π)) |
103 | 102, 2 | eleq2s 2851 |
. . . . . . . . . . 11
β’ (π§ β πΌ β π§ Fn (1...π)) |
104 | 103 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ (π§βπ) = 0) β§ π§ β πΌ) β π§ Fn (1...π)) |
105 | 21 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β πΌ) β (πΉβπ§) β πΌ) |
106 | | elmapfn 8858 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) β ((0[,]1) βm
(1...π)) β (πΉβπ§) Fn (1...π)) |
107 | 106, 2 | eleq2s 2851 |
. . . . . . . . . . . 12
β’ ((πΉβπ§) β πΌ β (πΉβπ§) Fn (1...π)) |
108 | 105, 107 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π§ β πΌ) β (πΉβπ§) Fn (1...π)) |
109 | 108 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ (π§βπ) = 0) β§ π§ β πΌ) β (πΉβπ§) Fn (1...π)) |
110 | | ovexd 7443 |
. . . . . . . . . 10
β’ (((π β§ (π§βπ) = 0) β§ π§ β πΌ) β (1...π) β V) |
111 | | simpllr 774 |
. . . . . . . . . 10
β’ ((((π β§ (π§βπ) = 0) β§ π§ β πΌ) β§ π β (1...π)) β (π§βπ) = 0) |
112 | | eqidd 2733 |
. . . . . . . . . 10
β’ ((((π β§ (π§βπ) = 0) β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) = ((πΉβπ§)βπ)) |
113 | 104, 109,
110, 110, 27, 111, 112 | ofval 7680 |
. . . . . . . . 9
β’ ((((π β§ (π§βπ) = 0) β§ π§ β πΌ) β§ π β (1...π)) β ((π§ βf β (πΉβπ§))βπ) = (0 β ((πΉβπ§)βπ))) |
114 | | df-neg 11446 |
. . . . . . . . 9
β’ -((πΉβπ§)βπ) = (0 β ((πΉβπ§)βπ)) |
115 | 113, 114 | eqtr4di 2790 |
. . . . . . . 8
β’ ((((π β§ (π§βπ) = 0) β§ π§ β πΌ) β§ π β (1...π)) β ((π§ βf β (πΉβπ§))βπ) = -((πΉβπ§)βπ)) |
116 | 115 | exp41 435 |
. . . . . . 7
β’ (π β ((π§βπ) = 0 β (π§ β πΌ β (π β (1...π) β ((π§ βf β (πΉβπ§))βπ) = -((πΉβπ§)βπ))))) |
117 | 116 | com24 95 |
. . . . . 6
β’ (π β (π β (1...π) β (π§ β πΌ β ((π§βπ) = 0 β ((π§ βf β (πΉβπ§))βπ) = -((πΉβπ§)βπ))))) |
118 | 117 | 3imp2 1349 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((π§ βf β (πΉβπ§))βπ) = -((πΉβπ§)βπ)) |
119 | 101, 118 | eqtrd 2772 |
. . . 4
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) = -((πΉβπ§)βπ)) |
120 | | elmapi 8842 |
. . . . . . . . . . . 12
β’ ((πΉβπ§) β ((0[,]1) βm
(1...π)) β (πΉβπ§):(1...π)βΆ(0[,]1)) |
121 | 120, 2 | eleq2s 2851 |
. . . . . . . . . . 11
β’ ((πΉβπ§) β πΌ β (πΉβπ§):(1...π)βΆ(0[,]1)) |
122 | 105, 121 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π§ β πΌ) β (πΉβπ§):(1...π)βΆ(0[,]1)) |
123 | 122 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) β (0[,]1)) |
124 | | 0xr 11260 |
. . . . . . . . . 10
β’ 0 β
β* |
125 | | 1xr 11272 |
. . . . . . . . . 10
β’ 1 β
β* |
126 | | iccgelb 13379 |
. . . . . . . . . 10
β’ ((0
β β* β§ 1 β β* β§ ((πΉβπ§)βπ) β (0[,]1)) β 0 β€ ((πΉβπ§)βπ)) |
127 | 124, 125,
126 | mp3an12 1451 |
. . . . . . . . 9
β’ (((πΉβπ§)βπ) β (0[,]1) β 0 β€ ((πΉβπ§)βπ)) |
128 | 123, 127 | syl 17 |
. . . . . . . 8
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β 0 β€ ((πΉβπ§)βπ)) |
129 | 13, 123 | sselid 3980 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) β β) |
130 | 129 | le0neg2d 11785 |
. . . . . . . 8
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β (0 β€ ((πΉβπ§)βπ) β -((πΉβπ§)βπ) β€ 0)) |
131 | 128, 130 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β -((πΉβπ§)βπ) β€ 0) |
132 | 131 | an32s 650 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β -((πΉβπ§)βπ) β€ 0) |
133 | 132 | anasss 467 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ)) β -((πΉβπ§)βπ) β€ 0) |
134 | 133 | 3adantr3 1171 |
. . . 4
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β -((πΉβπ§)βπ) β€ 0) |
135 | 119, 134 | eqbrtrd 5170 |
. . 3
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) β€ 0) |
136 | | iccleub 13378 |
. . . . . . . . . 10
β’ ((0
β β* β§ 1 β β* β§ ((πΉβπ§)βπ) β (0[,]1)) β ((πΉβπ§)βπ) β€ 1) |
137 | 124, 125,
136 | mp3an12 1451 |
. . . . . . . . 9
β’ (((πΉβπ§)βπ) β (0[,]1) β ((πΉβπ§)βπ) β€ 1) |
138 | 123, 137 | syl 17 |
. . . . . . . 8
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) β€ 1) |
139 | | 1red 11214 |
. . . . . . . . 9
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β 1 β β) |
140 | 139, 129 | subge0d 11803 |
. . . . . . . 8
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β (0 β€ (1 β ((πΉβπ§)βπ)) β ((πΉβπ§)βπ) β€ 1)) |
141 | 138, 140 | mpbird 256 |
. . . . . . 7
β’ (((π β§ π§ β πΌ) β§ π β (1...π)) β 0 β€ (1 β ((πΉβπ§)βπ))) |
142 | 141 | an32s 650 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π§ β πΌ) β 0 β€ (1 β ((πΉβπ§)βπ))) |
143 | 142 | anasss 467 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ)) β 0 β€ (1 β ((πΉβπ§)βπ))) |
144 | 143 | 3adantr3 1171 |
. . . 4
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ (1 β ((πΉβπ§)βπ))) |
145 | | simpr2 1195 |
. . . . . 6
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β π§ β πΌ) |
146 | 145, 100 | syl 17 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) = ((π§ βf β (πΉβπ§))βπ)) |
147 | 103 | adantl 482 |
. . . . . . . . 9
β’ (((π β§ (π§βπ) = 1) β§ π§ β πΌ) β π§ Fn (1...π)) |
148 | 108 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ (π§βπ) = 1) β§ π§ β πΌ) β (πΉβπ§) Fn (1...π)) |
149 | | ovexd 7443 |
. . . . . . . . 9
β’ (((π β§ (π§βπ) = 1) β§ π§ β πΌ) β (1...π) β V) |
150 | | simpllr 774 |
. . . . . . . . 9
β’ ((((π β§ (π§βπ) = 1) β§ π§ β πΌ) β§ π β (1...π)) β (π§βπ) = 1) |
151 | | eqidd 2733 |
. . . . . . . . 9
β’ ((((π β§ (π§βπ) = 1) β§ π§ β πΌ) β§ π β (1...π)) β ((πΉβπ§)βπ) = ((πΉβπ§)βπ)) |
152 | 147, 148,
149, 149, 27, 150, 151 | ofval 7680 |
. . . . . . . 8
β’ ((((π β§ (π§βπ) = 1) β§ π§ β πΌ) β§ π β (1...π)) β ((π§ βf β (πΉβπ§))βπ) = (1 β ((πΉβπ§)βπ))) |
153 | 152 | exp41 435 |
. . . . . . 7
β’ (π β ((π§βπ) = 1 β (π§ β πΌ β (π β (1...π) β ((π§ βf β (πΉβπ§))βπ) = (1 β ((πΉβπ§)βπ)))))) |
154 | 153 | com24 95 |
. . . . . 6
β’ (π β (π β (1...π) β (π§ β πΌ β ((π§βπ) = 1 β ((π§ βf β (πΉβπ§))βπ) = (1 β ((πΉβπ§)βπ)))))) |
155 | 154 | 3imp2 1349 |
. . . . 5
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β ((π§ βf β (πΉβπ§))βπ) = (1 β ((πΉβπ§)βπ))) |
156 | 146, 155 | eqtrd 2772 |
. . . 4
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ) = (1 β ((πΉβπ§)βπ))) |
157 | 144, 156 | breqtrrd 5176 |
. . 3
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ§)βπ)) |
158 | 1, 2, 3, 92, 135, 157 | poimir 36516 |
. 2
β’ (π β βπ β πΌ ((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = ((1...π) Γ {0})) |
159 | | id 22 |
. . . . . . . 8
β’ (π₯ = π β π₯ = π) |
160 | | fveq2 6891 |
. . . . . . . 8
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
161 | 159, 160 | oveq12d 7426 |
. . . . . . 7
β’ (π₯ = π β (π₯ βf β (πΉβπ₯)) = (π βf β (πΉβπ))) |
162 | | ovex 7441 |
. . . . . . 7
β’ (π βf β
(πΉβπ)) β V |
163 | 161, 97, 162 | fvmpt 6998 |
. . . . . 6
β’ (π β πΌ β ((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = (π βf β (πΉβπ))) |
164 | 163 | adantl 482 |
. . . . 5
β’ ((π β§ π β πΌ) β ((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = (π βf β (πΉβπ))) |
165 | 164 | eqeq1d 2734 |
. . . 4
β’ ((π β§ π β πΌ) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = ((1...π) Γ {0}) β (π βf β (πΉβπ)) = ((1...π) Γ {0}))) |
166 | | elmapfn 8858 |
. . . . . . . . . . 11
β’ (π β ((0[,]1)
βm (1...π))
β π Fn (1...π)) |
167 | 166, 2 | eleq2s 2851 |
. . . . . . . . . 10
β’ (π β πΌ β π Fn (1...π)) |
168 | 167 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β π Fn (1...π)) |
169 | 21 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (πΉβπ) β πΌ) |
170 | | elmapfn 8858 |
. . . . . . . . . . 11
β’ ((πΉβπ) β ((0[,]1) βm
(1...π)) β (πΉβπ) Fn (1...π)) |
171 | 170, 2 | eleq2s 2851 |
. . . . . . . . . 10
β’ ((πΉβπ) β πΌ β (πΉβπ) Fn (1...π)) |
172 | 169, 171 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (πΉβπ) Fn (1...π)) |
173 | | ovexd 7443 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (1...π) β V) |
174 | | eqidd 2733 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (πβπ) = (πβπ)) |
175 | | eqidd 2733 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
176 | 168, 172,
173, 173, 27, 174, 175 | ofval 7680 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((π βf β (πΉβπ))βπ) = ((πβπ) β ((πΉβπ)βπ))) |
177 | | c0ex 11207 |
. . . . . . . . . 10
β’ 0 β
V |
178 | 177 | fvconst2 7204 |
. . . . . . . . 9
β’ (π β (1...π) β (((1...π) Γ {0})βπ) = 0) |
179 | 178 | adantl 482 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((1...π) Γ {0})βπ) = 0) |
180 | 176, 179 | eqeq12d 2748 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((π βf β (πΉβπ))βπ) = (((1...π) Γ {0})βπ) β ((πβπ) β ((πΉβπ)βπ)) = 0)) |
181 | 13, 84 | sstri 3991 |
. . . . . . . . . 10
β’ (0[,]1)
β β |
182 | | elmapi 8842 |
. . . . . . . . . . . 12
β’ (π β ((0[,]1)
βm (1...π))
β π:(1...π)βΆ(0[,]1)) |
183 | 182, 2 | eleq2s 2851 |
. . . . . . . . . . 11
β’ (π β πΌ β π:(1...π)βΆ(0[,]1)) |
184 | 183 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β πΌ β§ π β (1...π)) β (πβπ) β (0[,]1)) |
185 | 181, 184 | sselid 3980 |
. . . . . . . . 9
β’ ((π β πΌ β§ π β (1...π)) β (πβπ) β β) |
186 | 185 | adantll 712 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (πβπ) β β) |
187 | | elmapi 8842 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β ((0[,]1) βm
(1...π)) β (πΉβπ):(1...π)βΆ(0[,]1)) |
188 | 187, 2 | eleq2s 2851 |
. . . . . . . . . . 11
β’ ((πΉβπ) β πΌ β (πΉβπ):(1...π)βΆ(0[,]1)) |
189 | 169, 188 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (πΉβπ):(1...π)βΆ(0[,]1)) |
190 | 189 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((πΉβπ)βπ) β (0[,]1)) |
191 | 181, 190 | sselid 3980 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ π β (1...π)) β ((πΉβπ)βπ) β β) |
192 | 186, 191 | subeq0ad 11580 |
. . . . . . 7
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((πβπ) β ((πΉβπ)βπ)) = 0 β (πβπ) = ((πΉβπ)βπ))) |
193 | 180, 192 | bitrd 278 |
. . . . . 6
β’ (((π β§ π β πΌ) β§ π β (1...π)) β (((π βf β (πΉβπ))βπ) = (((1...π) Γ {0})βπ) β (πβπ) = ((πΉβπ)βπ))) |
194 | 193 | ralbidva 3175 |
. . . . 5
β’ ((π β§ π β πΌ) β (βπ β (1...π)((π βf β (πΉβπ))βπ) = (((1...π) Γ {0})βπ) β βπ β (1...π)(πβπ) = ((πΉβπ)βπ))) |
195 | 168, 172,
173, 173, 27 | offn 7682 |
. . . . . 6
β’ ((π β§ π β πΌ) β (π βf β (πΉβπ)) Fn (1...π)) |
196 | | fnconstg 6779 |
. . . . . . 7
β’ (0 β
V β ((1...π) Γ
{0}) Fn (1...π)) |
197 | 177, 196 | ax-mp 5 |
. . . . . 6
β’
((1...π) Γ
{0}) Fn (1...π) |
198 | | eqfnfv 7032 |
. . . . . 6
β’ (((π βf β
(πΉβπ)) Fn (1...π) β§ ((1...π) Γ {0}) Fn (1...π)) β ((π βf β (πΉβπ)) = ((1...π) Γ {0}) β βπ β (1...π)((π βf β (πΉβπ))βπ) = (((1...π) Γ {0})βπ))) |
199 | 195, 197,
198 | sylancl 586 |
. . . . 5
β’ ((π β§ π β πΌ) β ((π βf β (πΉβπ)) = ((1...π) Γ {0}) β βπ β (1...π)((π βf β (πΉβπ))βπ) = (((1...π) Γ {0})βπ))) |
200 | | eqfnfv 7032 |
. . . . . 6
β’ ((π Fn (1...π) β§ (πΉβπ) Fn (1...π)) β (π = (πΉβπ) β βπ β (1...π)(πβπ) = ((πΉβπ)βπ))) |
201 | 168, 172,
200 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β πΌ) β (π = (πΉβπ) β βπ β (1...π)(πβπ) = ((πΉβπ)βπ))) |
202 | 194, 199,
201 | 3bitr4d 310 |
. . . 4
β’ ((π β§ π β πΌ) β ((π βf β (πΉβπ)) = ((1...π) Γ {0}) β π = (πΉβπ))) |
203 | 165, 202 | bitrd 278 |
. . 3
β’ ((π β§ π β πΌ) β (((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = ((1...π) Γ {0}) β π = (πΉβπ))) |
204 | 203 | rexbidva 3176 |
. 2
β’ (π β (βπ β πΌ ((π₯ β πΌ β¦ (π₯ βf β (πΉβπ₯)))βπ) = ((1...π) Γ {0}) β βπ β πΌ π = (πΉβπ))) |
205 | 158, 204 | mpbid 231 |
1
β’ (π β βπ β πΌ π = (πΉβπ)) |