Step | Hyp | Ref
| Expression |
1 | | vdwlem8.a |
. . . . . . . . . 10
β’ (π β π΄ β β) |
2 | 1 | nncnd 12228 |
. . . . . . . . 9
β’ (π β π΄ β β) |
3 | | vdwlem8.d |
. . . . . . . . . 10
β’ (π β π· β β) |
4 | 3 | nncnd 12228 |
. . . . . . . . 9
β’ (π β π· β β) |
5 | 2, 4 | addcomd 11416 |
. . . . . . . 8
β’ (π β (π΄ + π·) = (π· + π΄)) |
6 | 5 | oveq2d 7425 |
. . . . . . 7
β’ (π β (π β (π΄ + π·)) = (π β (π· + π΄))) |
7 | | vdwlem8.w |
. . . . . . . . 9
β’ (π β π β β) |
8 | 7 | nncnd 12228 |
. . . . . . . 8
β’ (π β π β β) |
9 | 8, 4, 2 | subsub4d 11602 |
. . . . . . 7
β’ (π β ((π β π·) β π΄) = (π β (π· + π΄))) |
10 | 6, 9 | eqtr4d 2776 |
. . . . . 6
β’ (π β (π β (π΄ + π·)) = ((π β π·) β π΄)) |
11 | 10 | oveq2d 7425 |
. . . . 5
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) = ((π΄ + π΄) + ((π β π·) β π΄))) |
12 | 8, 4 | subcld 11571 |
. . . . . 6
β’ (π β (π β π·) β β) |
13 | 2, 2, 12 | ppncand 11611 |
. . . . 5
β’ (π β ((π΄ + π΄) + ((π β π·) β π΄)) = (π΄ + (π β π·))) |
14 | 11, 13 | eqtrd 2773 |
. . . 4
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) = (π΄ + (π β π·))) |
15 | 1, 1 | nnaddcld 12264 |
. . . . 5
β’ (π β (π΄ + π΄) β β) |
16 | | vdwlem8.s |
. . . . . . . 8
β’ (π β (π΄(APβπΎ)π·) β (β‘πΊ β {πΆ})) |
17 | | cnvimass 6081 |
. . . . . . . . 9
β’ (β‘πΊ β {πΆ}) β dom πΊ |
18 | | fvex 6905 |
. . . . . . . . . 10
β’ (πΉβ(π₯ + π)) β V |
19 | | vdwlem8.g |
. . . . . . . . . 10
β’ πΊ = (π₯ β (1...π) β¦ (πΉβ(π₯ + π))) |
20 | 18, 19 | dmmpti 6695 |
. . . . . . . . 9
β’ dom πΊ = (1...π) |
21 | 17, 20 | sseqtri 4019 |
. . . . . . . 8
β’ (β‘πΊ β {πΆ}) β (1...π) |
22 | 16, 21 | sstrdi 3995 |
. . . . . . 7
β’ (π β (π΄(APβπΎ)π·) β (1...π)) |
23 | | ssun2 4174 |
. . . . . . . . 9
β’ ((π΄ + π·)(APβ(πΎ β 1))π·) β ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·)) |
24 | | vdwlem8.k |
. . . . . . . . . . 11
β’ (π β πΎ β
(β€β₯β2)) |
25 | | uz2m1nn 12907 |
. . . . . . . . . . 11
β’ (πΎ β
(β€β₯β2) β (πΎ β 1) β β) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΎ β 1) β β) |
27 | 1, 3 | nnaddcld 12264 |
. . . . . . . . . 10
β’ (π β (π΄ + π·) β β) |
28 | | vdwapid1 16908 |
. . . . . . . . . 10
β’ (((πΎ β 1) β β β§
(π΄ + π·) β β β§ π· β β) β (π΄ + π·) β ((π΄ + π·)(APβ(πΎ β 1))π·)) |
29 | 26, 27, 3, 28 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄ + π·) β ((π΄ + π·)(APβ(πΎ β 1))π·)) |
30 | 23, 29 | sselid 3981 |
. . . . . . . 8
β’ (π β (π΄ + π·) β ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
31 | | eluz2nn 12868 |
. . . . . . . . . . . . . 14
β’ (πΎ β
(β€β₯β2) β πΎ β β) |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΎ β β) |
33 | 32 | nncnd 12228 |
. . . . . . . . . . . 12
β’ (π β πΎ β β) |
34 | | ax-1cn 11168 |
. . . . . . . . . . . 12
β’ 1 β
β |
35 | | npcan 11469 |
. . . . . . . . . . . 12
β’ ((πΎ β β β§ 1 β
β) β ((πΎ β
1) + 1) = πΎ) |
36 | 33, 34, 35 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β ((πΎ β 1) + 1) = πΎ) |
37 | 36 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π β (APβ((πΎ β 1) + 1)) =
(APβπΎ)) |
38 | 37 | oveqd 7426 |
. . . . . . . . 9
β’ (π β (π΄(APβ((πΎ β 1) + 1))π·) = (π΄(APβπΎ)π·)) |
39 | 26 | nnnn0d 12532 |
. . . . . . . . . 10
β’ (π β (πΎ β 1) β
β0) |
40 | | vdwapun 16907 |
. . . . . . . . . 10
β’ (((πΎ β 1) β
β0 β§ π΄
β β β§ π·
β β) β (π΄(APβ((πΎ β 1) + 1))π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
41 | 39, 1, 3, 40 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄(APβ((πΎ β 1) + 1))π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
42 | 38, 41 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (π΄(APβπΎ)π·) = ({π΄} βͺ ((π΄ + π·)(APβ(πΎ β 1))π·))) |
43 | 30, 42 | eleqtrrd 2837 |
. . . . . . 7
β’ (π β (π΄ + π·) β (π΄(APβπΎ)π·)) |
44 | 22, 43 | sseldd 3984 |
. . . . . 6
β’ (π β (π΄ + π·) β (1...π)) |
45 | | elfzuz3 13498 |
. . . . . 6
β’ ((π΄ + π·) β (1...π) β π β (β€β₯β(π΄ + π·))) |
46 | | uznn0sub 12861 |
. . . . . 6
β’ (π β
(β€β₯β(π΄ + π·)) β (π β (π΄ + π·)) β
β0) |
47 | 44, 45, 46 | 3syl 18 |
. . . . 5
β’ (π β (π β (π΄ + π·)) β
β0) |
48 | | nnnn0addcl 12502 |
. . . . 5
β’ (((π΄ + π΄) β β β§ (π β (π΄ + π·)) β β0) β
((π΄ + π΄) + (π β (π΄ + π·))) β β) |
49 | 15, 47, 48 | syl2anc 585 |
. . . 4
β’ (π β ((π΄ + π΄) + (π β (π΄ + π·))) β β) |
50 | 14, 49 | eqeltrrd 2835 |
. . 3
β’ (π β (π΄ + (π β π·)) β β) |
51 | | 1nn 12223 |
. . . . . . . 8
β’ 1 β
β |
52 | | f1osng 6875 |
. . . . . . . 8
β’ ((1
β β β§ π·
β β) β {β¨1, π·β©}:{1}β1-1-ontoβ{π·}) |
53 | 51, 3, 52 | sylancr 588 |
. . . . . . 7
β’ (π β {β¨1, π·β©}:{1}β1-1-ontoβ{π·}) |
54 | | f1of 6834 |
. . . . . . 7
β’
({β¨1, π·β©}:{1}β1-1-ontoβ{π·} β {β¨1, π·β©}:{1}βΆ{π·}) |
55 | 53, 54 | syl 17 |
. . . . . 6
β’ (π β {β¨1, π·β©}:{1}βΆ{π·}) |
56 | 3 | snssd 4813 |
. . . . . 6
β’ (π β {π·} β β) |
57 | 55, 56 | fssd 6736 |
. . . . 5
β’ (π β {β¨1, π·β©}:{1}βΆβ) |
58 | | 1z 12592 |
. . . . . . 7
β’ 1 β
β€ |
59 | | fzsn 13543 |
. . . . . . 7
β’ (1 β
β€ β (1...1) = {1}) |
60 | 58, 59 | ax-mp 5 |
. . . . . 6
β’ (1...1) =
{1} |
61 | 60 | feq2i 6710 |
. . . . 5
β’
({β¨1, π·β©}:(1...1)βΆβ β
{β¨1, π·β©}:{1}βΆβ) |
62 | 57, 61 | sylibr 233 |
. . . 4
β’ (π β {β¨1, π·β©}:(1...1)βΆβ) |
63 | | nnex 12218 |
. . . . 5
β’ β
β V |
64 | | ovex 7442 |
. . . . 5
β’ (1...1)
β V |
65 | 63, 64 | elmap 8865 |
. . . 4
β’
({β¨1, π·β©}
β (β βm (1...1)) β {β¨1, π·β©}:(1...1)βΆβ) |
66 | 62, 65 | sylibr 233 |
. . 3
β’ (π β {β¨1, π·β©} β (β
βm (1...1))) |
67 | 1, 7 | nnaddcld 12264 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ + π) β β) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + π) β β) |
69 | | elfznn0 13594 |
. . . . . . . . . . . . . 14
β’ (π β (0...(πΎ β 1)) β π β β0) |
70 | 3 | nnnn0d 12532 |
. . . . . . . . . . . . . 14
β’ (π β π· β
β0) |
71 | | nn0mulcl 12508 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π· β
β0) β (π Β· π·) β
β0) |
72 | 69, 70, 71 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π Β· π·) β
β0) |
73 | | nnnn0addcl 12502 |
. . . . . . . . . . . . 13
β’ (((π΄ + π) β β β§ (π Β· π·) β β0) β ((π΄ + π) + (π Β· π·)) β β) |
74 | 68, 72, 73 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β β) |
75 | | nnuz 12865 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
76 | 74, 75 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β
(β€β₯β1)) |
77 | 16 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄(APβπΎ)π·) β (β‘πΊ β {πΆ})) |
78 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ + (π Β· π·)) = (π΄ + (π Β· π·)) |
79 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π Β· π·) = (π Β· π·)) |
80 | 79 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
81 | 80 | rspceeqv 3634 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...(πΎ β 1)) β§ (π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
82 | 78, 81 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(πΎ β 1)) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) |
83 | 32 | nnnn0d 12532 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ β
β0) |
84 | | vdwapval 16906 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β β0
β§ π΄ β β
β§ π· β β)
β ((π΄ + (π Β· π·)) β (π΄(APβπΎ)π·) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·)))) |
85 | 83, 1, 3, 84 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π΄ + (π Β· π·)) β (π΄(APβπΎ)π·) β βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·)))) |
86 | 85 | biimpar 479 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ βπ β (0...(πΎ β 1))(π΄ + (π Β· π·)) = (π΄ + (π Β· π·))) β (π΄ + (π Β· π·)) β (π΄(APβπΎ)π·)) |
87 | 82, 86 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (π΄(APβπΎ)π·)) |
88 | 77, 87 | sseldd 3984 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (β‘πΊ β {πΆ})) |
89 | 18, 19 | fnmpti 6694 |
. . . . . . . . . . . . . . . 16
β’ πΊ Fn (1...π) |
90 | | fniniseg 7062 |
. . . . . . . . . . . . . . . 16
β’ (πΊ Fn (1...π) β ((π΄ + (π Β· π·)) β (β‘πΊ β {πΆ}) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((π΄ + (π Β· π·)) β (β‘πΊ β {πΆ}) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ)) |
92 | 88, 91 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + (π Β· π·)) β (1...π) β§ (πΊβ(π΄ + (π Β· π·))) = πΆ)) |
93 | 92 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β (π΄ + (π Β· π·)) β (1...π)) |
94 | | elfzuz3 13498 |
. . . . . . . . . . . . 13
β’ ((π΄ + (π Β· π·)) β (1...π) β π β (β€β₯β(π΄ + (π Β· π·)))) |
95 | | eluzelz 12832 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β(π΄ + (π Β· π·))) β π β β€) |
96 | | eluzadd 12851 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β(π΄ + (π Β· π·))) β§ π β β€) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
97 | 95, 96 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β(π΄ + (π Β· π·))) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
98 | 93, 94, 97 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β (π + π) β
(β€β₯β((π΄ + (π Β· π·)) + π))) |
99 | 8 | 2timesd 12455 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· π) = (π + π)) |
100 | 99 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β (2 Β· π) = (π + π)) |
101 | 2 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β π΄ β β) |
102 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β π β β) |
103 | 72 | nn0cnd 12534 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΎ β 1))) β (π Β· π·) β β) |
104 | 101, 102,
103 | add32d 11441 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) = ((π΄ + (π Β· π·)) + π)) |
105 | 104 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΎ β 1))) β
(β€β₯β((π΄ + π) + (π Β· π·))) = (β€β₯β((π΄ + (π Β· π·)) + π))) |
106 | 98, 100, 105 | 3eltr4d 2849 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (2 Β· π) β
(β€β₯β((π΄ + π) + (π Β· π·)))) |
107 | | elfzuzb 13495 |
. . . . . . . . . . 11
β’ (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β (((π΄ + π) + (π Β· π·)) β (β€β₯β1)
β§ (2 Β· π) β
(β€β₯β((π΄ + π) + (π Β· π·))))) |
108 | 76, 106, 107 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΎ β 1))) β ((π΄ + π) + (π Β· π·)) β (1...(2 Β· π))) |
109 | 104 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΉβ((π΄ + π) + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
110 | | fvoveq1 7432 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ + (π Β· π·)) β (πΉβ(π₯ + π)) = (πΉβ((π΄ + (π Β· π·)) + π))) |
111 | | fvex 6905 |
. . . . . . . . . . . . 13
β’ (πΉβ((π΄ + (π Β· π·)) + π)) β V |
112 | 110, 19, 111 | fvmpt 6999 |
. . . . . . . . . . . 12
β’ ((π΄ + (π Β· π·)) β (1...π) β (πΊβ(π΄ + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
113 | 93, 112 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΊβ(π΄ + (π Β· π·))) = (πΉβ((π΄ + (π Β· π·)) + π))) |
114 | 92 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΎ β 1))) β (πΊβ(π΄ + (π Β· π·))) = πΆ) |
115 | 109, 113,
114 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΎ β 1))) β (πΉβ((π΄ + π) + (π Β· π·))) = πΆ) |
116 | 108, 115 | jca 513 |
. . . . . . . . 9
β’ ((π β§ π β (0...(πΎ β 1))) β (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β§ (πΉβ((π΄ + π) + (π Β· π·))) = πΆ)) |
117 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β ((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)))) |
118 | | fveqeq2 6901 |
. . . . . . . . . 10
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β ((πΉβπ₯) = πΆ β (πΉβ((π΄ + π) + (π Β· π·))) = πΆ)) |
119 | 117, 118 | anbi12d 632 |
. . . . . . . . 9
β’ (π₯ = ((π΄ + π) + (π Β· π·)) β ((π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ) β (((π΄ + π) + (π Β· π·)) β (1...(2 Β· π)) β§ (πΉβ((π΄ + π) + (π Β· π·))) = πΆ))) |
120 | 116, 119 | syl5ibrcom 246 |
. . . . . . . 8
β’ ((π β§ π β (0...(πΎ β 1))) β (π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
121 | 120 | rexlimdva 3156 |
. . . . . . 7
β’ (π β (βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
122 | | vdwapval 16906 |
. . . . . . . 8
β’ ((πΎ β β0
β§ (π΄ + π) β β β§ π· β β) β (π₯ β ((π΄ + π)(APβπΎ)π·) β βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)))) |
123 | 83, 67, 3, 122 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β ((π΄ + π)(APβπΎ)π·) β βπ β (0...(πΎ β 1))π₯ = ((π΄ + π) + (π Β· π·)))) |
124 | | vdwlem8.f |
. . . . . . . 8
β’ (π β πΉ:(1...(2 Β· π))βΆπ
) |
125 | | ffn 6718 |
. . . . . . . 8
β’ (πΉ:(1...(2 Β· π))βΆπ
β πΉ Fn (1...(2 Β· π))) |
126 | | fniniseg 7062 |
. . . . . . . 8
β’ (πΉ Fn (1...(2 Β· π)) β (π₯ β (β‘πΉ β {πΆ}) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . 7
β’ (π β (π₯ β (β‘πΉ β {πΆ}) β (π₯ β (1...(2 Β· π)) β§ (πΉβπ₯) = πΆ))) |
128 | 121, 123,
127 | 3imtr4d 294 |
. . . . . 6
β’ (π β (π₯ β ((π΄ + π)(APβπΎ)π·) β π₯ β (β‘πΉ β {πΆ}))) |
129 | 128 | ssrdv 3989 |
. . . . 5
β’ (π β ((π΄ + π)(APβπΎ)π·) β (β‘πΉ β {πΆ})) |
130 | | fvsng 7178 |
. . . . . . . . 9
β’ ((1
β β β§ π·
β β) β ({β¨1, π·β©}β1) = π·) |
131 | 51, 3, 130 | sylancr 588 |
. . . . . . . 8
β’ (π β ({β¨1, π·β©}β1) = π·) |
132 | 131 | oveq2d 7425 |
. . . . . . 7
β’ (π β ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)) = ((π΄ + (π β π·)) + π·)) |
133 | 2, 12, 4 | addassd 11236 |
. . . . . . 7
β’ (π β ((π΄ + (π β π·)) + π·) = (π΄ + ((π β π·) + π·))) |
134 | 8, 4 | npcand 11575 |
. . . . . . . 8
β’ (π β ((π β π·) + π·) = π) |
135 | 134 | oveq2d 7425 |
. . . . . . 7
β’ (π β (π΄ + ((π β π·) + π·)) = (π΄ + π)) |
136 | 132, 133,
135 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)) = (π΄ + π)) |
137 | 136, 131 | oveq12d 7427 |
. . . . 5
β’ (π β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) = ((π΄ + π)(APβπΎ)π·)) |
138 | 136 | fveq2d 6896 |
. . . . . . . 8
β’ (π β (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) = (πΉβ(π΄ + π))) |
139 | | vdwapid1 16908 |
. . . . . . . . . . . . 13
β’ ((πΎ β β β§ π΄ β β β§ π· β β) β π΄ β (π΄(APβπΎ)π·)) |
140 | 32, 1, 3, 139 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β π΄ β (π΄(APβπΎ)π·)) |
141 | 16, 140 | sseldd 3984 |
. . . . . . . . . . 11
β’ (π β π΄ β (β‘πΊ β {πΆ})) |
142 | | fniniseg 7062 |
. . . . . . . . . . . 12
β’ (πΊ Fn (1...π) β (π΄ β (β‘πΊ β {πΆ}) β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ))) |
143 | 89, 142 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π΄ β (β‘πΊ β {πΆ}) β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ)) |
144 | 141, 143 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π΄ β (1...π) β§ (πΊβπ΄) = πΆ)) |
145 | 144 | simpld 496 |
. . . . . . . . 9
β’ (π β π΄ β (1...π)) |
146 | | fvoveq1 7432 |
. . . . . . . . . 10
β’ (π₯ = π΄ β (πΉβ(π₯ + π)) = (πΉβ(π΄ + π))) |
147 | | fvex 6905 |
. . . . . . . . . 10
β’ (πΉβ(π΄ + π)) β V |
148 | 146, 19, 147 | fvmpt 6999 |
. . . . . . . . 9
β’ (π΄ β (1...π) β (πΊβπ΄) = (πΉβ(π΄ + π))) |
149 | 145, 148 | syl 17 |
. . . . . . . 8
β’ (π β (πΊβπ΄) = (πΉβ(π΄ + π))) |
150 | 144 | simprd 497 |
. . . . . . . 8
β’ (π β (πΊβπ΄) = πΆ) |
151 | 138, 149,
150 | 3eqtr2d 2779 |
. . . . . . 7
β’ (π β (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) = πΆ) |
152 | 151 | sneqd 4641 |
. . . . . 6
β’ (π β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))} = {πΆ}) |
153 | 152 | imaeq2d 6060 |
. . . . 5
β’ (π β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) = (β‘πΉ β {πΆ})) |
154 | 129, 137,
153 | 3sstr4d 4030 |
. . . 4
β’ (π β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
155 | 154 | ralrimivw 3151 |
. . 3
β’ (π β βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
156 | 151 | mpteq2dv 5251 |
. . . . . . . 8
β’ (π β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = (π β (1...1) β¦ πΆ)) |
157 | | fconstmpt 5739 |
. . . . . . . 8
β’ ((1...1)
Γ {πΆ}) = (π β (1...1) β¦ πΆ) |
158 | 156, 157 | eqtr4di 2791 |
. . . . . . 7
β’ (π β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = ((1...1) Γ
{πΆ})) |
159 | 158 | rneqd 5938 |
. . . . . 6
β’ (π β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = ran ((1...1) Γ
{πΆ})) |
160 | | elfz3 13511 |
. . . . . . . 8
β’ (1 β
β€ β 1 β (1...1)) |
161 | | ne0i 4335 |
. . . . . . . 8
β’ (1 β
(1...1) β (1...1) β β
) |
162 | 58, 160, 161 | mp2b 10 |
. . . . . . 7
β’ (1...1)
β β
|
163 | | rnxp 6170 |
. . . . . . 7
β’ ((1...1)
β β
β ran ((1...1) Γ {πΆ}) = {πΆ}) |
164 | 162, 163 | ax-mp 5 |
. . . . . 6
β’ ran
((1...1) Γ {πΆ}) =
{πΆ} |
165 | 159, 164 | eqtrdi 2789 |
. . . . 5
β’ (π β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) = {πΆ}) |
166 | 165 | fveq2d 6896 |
. . . 4
β’ (π β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = (β―β{πΆ})) |
167 | | vdwlem8.c |
. . . . 5
β’ πΆ β V |
168 | | hashsng 14329 |
. . . . 5
β’ (πΆ β V β
(β―β{πΆ}) =
1) |
169 | 167, 168 | ax-mp 5 |
. . . 4
β’
(β―β{πΆ})
= 1 |
170 | 166, 169 | eqtrdi 2789 |
. . 3
β’ (π β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1) |
171 | | oveq1 7416 |
. . . . . . . 8
β’ (π = (π΄ + (π β π·)) β (π + (πβπ)) = ((π΄ + (π β π·)) + (πβπ))) |
172 | 171 | oveq1d 7424 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β ((π + (πβπ))(APβπΎ)(πβπ)) = (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ))) |
173 | | fvoveq1 7432 |
. . . . . . . . 9
β’ (π = (π΄ + (π β π·)) β (πΉβ(π + (πβπ))) = (πΉβ((π΄ + (π β π·)) + (πβπ)))) |
174 | 173 | sneqd 4641 |
. . . . . . . 8
β’ (π = (π΄ + (π β π·)) β {(πΉβ(π + (πβπ)))} = {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) |
175 | 174 | imaeq2d 6060 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) = (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))})) |
176 | 172, 175 | sseq12d 4016 |
. . . . . 6
β’ (π = (π΄ + (π β π·)) β (((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}))) |
177 | 176 | ralbidv 3178 |
. . . . 5
β’ (π = (π΄ + (π β π·)) β (βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}))) |
178 | 173 | mpteq2dv 5251 |
. . . . . . 7
β’ (π = (π΄ + (π β π·)) β (π β (1...1) β¦ (πΉβ(π + (πβπ)))) = (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) |
179 | 178 | rneqd 5938 |
. . . . . 6
β’ (π = (π΄ + (π β π·)) β ran (π β (1...1) β¦ (πΉβ(π + (πβπ)))) = ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) |
180 | 179 | fveqeq2d 6900 |
. . . . 5
β’ (π = (π΄ + (π β π·)) β ((β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1 β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1)) |
181 | 177, 180 | anbi12d 632 |
. . . 4
β’ (π = (π΄ + (π β π·)) β ((βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1) β (βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1))) |
182 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = {β¨1, π·β©} β (πβπ) = ({β¨1, π·β©}βπ)) |
183 | | elfz1eq 13512 |
. . . . . . . . . . 11
β’ (π β (1...1) β π = 1) |
184 | 183 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π β (1...1) β
({β¨1, π·β©}βπ) = ({β¨1, π·β©}β1)) |
185 | 182, 184 | sylan9eq 2793 |
. . . . . . . . 9
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (πβπ) = ({β¨1, π·β©}β1)) |
186 | 185 | oveq2d 7425 |
. . . . . . . 8
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β ((π΄ + (π β π·)) + (πβπ)) = ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))) |
187 | 186, 185 | oveq12d 7427 |
. . . . . . 7
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) = (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1))) |
188 | 186 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (πΉβ((π΄ + (π β π·)) + (πβπ))) = (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))) |
189 | 188 | sneqd 4641 |
. . . . . . . 8
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β {(πΉβ((π΄ + (π β π·)) + (πβπ)))} = {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) |
190 | 189 | imaeq2d 6060 |
. . . . . . 7
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) = (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))})) |
191 | 187, 190 | sseq12d 4016 |
. . . . . 6
β’ ((π = {β¨1, π·β©} β§ π β (1...1)) β ((((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β (((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}))) |
192 | 191 | ralbidva 3176 |
. . . . 5
β’ (π = {β¨1, π·β©} β (βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}))) |
193 | 188 | mpteq2dva 5249 |
. . . . . . 7
β’ (π = {β¨1, π·β©} β (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ)))) = (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) |
194 | 193 | rneqd 5938 |
. . . . . 6
β’ (π = {β¨1, π·β©} β ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ)))) = ran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) |
195 | 194 | fveqeq2d 6900 |
. . . . 5
β’ (π = {β¨1, π·β©} β ((β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1 β (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1)) |
196 | 192, 195 | anbi12d 632 |
. . . 4
β’ (π = {β¨1, π·β©} β ((βπ β (1...1)(((π΄ + (π β π·)) + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + (πβπ))))) = 1) β (βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) β§
(β―βran (π
β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1))) |
197 | 181, 196 | rspc2ev 3625 |
. . 3
β’ (((π΄ + (π β π·)) β β β§ {β¨1, π·β©} β (β
βm (1...1)) β§ (βπ β (1...1)(((π΄ + (π β π·)) + ({β¨1, π·β©}β1))(APβπΎ)({β¨1, π·β©}β1)) β (β‘πΉ β {(πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1)))}) β§
(β―βran (π
β (1...1) β¦ (πΉβ((π΄ + (π β π·)) + ({β¨1, π·β©}β1))))) = 1)) β
βπ β β
βπ β (β
βm (1...1))(βπ β (1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1)) |
198 | 50, 66, 155, 170, 197 | syl112anc 1375 |
. 2
β’ (π β βπ β β βπ β (β βm
(1...1))(βπ β
(1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1)) |
199 | | ovex 7442 |
. . 3
β’ (1...(2
Β· π)) β
V |
200 | 51 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
201 | | eqid 2733 |
. . 3
β’ (1...1) =
(1...1) |
202 | 199, 83, 124, 200, 201 | vdwpc 16913 |
. 2
β’ (π β (β¨1, πΎβ© PolyAP πΉ β βπ β β βπ β (β βm
(1...1))(βπ β
(1...1)((π + (πβπ))(APβπΎ)(πβπ)) β (β‘πΉ β {(πΉβ(π + (πβπ)))}) β§ (β―βran (π β (1...1) β¦ (πΉβ(π + (πβπ))))) = 1))) |
203 | 198, 202 | mpbird 257 |
1
β’ (π β β¨1, πΎβ© PolyAP πΉ) |