Step | Hyp | Ref
| Expression |
1 | | reprval.a |
. . 3
β’ (π β π΄ β β) |
2 | | reprval.m |
. . 3
β’ (π β π β β€) |
3 | | reprval.s |
. . . 4
β’ (π β π β
β0) |
4 | | 1nn0 12492 |
. . . . 5
β’ 1 β
β0 |
5 | 4 | a1i 11 |
. . . 4
β’ (π β 1 β
β0) |
6 | 3, 5 | nn0addcld 12540 |
. . 3
β’ (π β (π + 1) β
β0) |
7 | 1, 2, 6 | reprval 33908 |
. 2
β’ (π β (π΄(reprβ(π + 1))π) = {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π}) |
8 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β (π΄ βm (0..^(π + 1)))) |
9 | | elmapi 8845 |
. . . . . . . . . 10
β’ (π β (π΄ βm (0..^(π + 1))) β π:(0..^(π + 1))βΆπ΄) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π:(0..^(π + 1))βΆπ΄) |
11 | 3 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β
β0) |
12 | | fzonn0p1 13713 |
. . . . . . . . . 10
β’ (π β β0
β π β (0..^(π + 1))) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β (0..^(π + 1))) |
14 | 10, 13 | ffvelcdmd 7087 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β π΄) |
15 | | simpr 485 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β π = (πβπ)) |
16 | 15 | oveq2d 7427 |
. . . . . . . . . 10
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π β π) = (π β (πβπ))) |
17 | 16 | oveq2d 7427 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π΄(reprβπ)(π β π)) = (π΄(reprβπ)(π β (πβπ)))) |
18 | | opeq2 4874 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β β¨π, πβ© = β¨π, (πβπ)β©) |
19 | 18 | sneqd 4640 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β {β¨π, πβ©} = {β¨π, (πβπ)β©}) |
20 | 19 | uneq2d 4163 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (π βͺ {β¨π, πβ©}) = (π βͺ {β¨π, (πβπ)β©})) |
21 | 20 | eqeq2d 2743 |
. . . . . . . . . 10
β’ (π = (πβπ) β (π = (π βͺ {β¨π, πβ©}) β π = (π βͺ {β¨π, (πβπ)β©}))) |
22 | 21 | adantl 482 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π = (π βͺ {β¨π, πβ©}) β π = (π βͺ {β¨π, (πβπ)β©}))) |
23 | 17, 22 | rexeqbidv 3343 |
. . . . . . . 8
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©}) β βπ β (π΄(reprβπ)(π β (πβπ)))π = (π βͺ {β¨π, (πβπ)β©}))) |
24 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π:(0..^(π + 1))βΆπ΄) |
25 | 3 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π β
β0) |
26 | | fzossfzop1 13714 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^π) β (0..^(π + 1))) |
28 | 24, 27 | fssresd 6758 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (π βΎ (0..^π)):(0..^π)βΆπ΄) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)):(0..^π)βΆπ΄) |
30 | | nnex 12222 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
V) |
32 | 31, 1 | ssexd 5324 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β V) |
33 | | fzofi 13943 |
. . . . . . . . . . . . . . . 16
β’
(0..^π) β
Fin |
34 | 33 | elexi 3493 |
. . . . . . . . . . . . . . 15
β’
(0..^π) β
V |
35 | | elmapg 8835 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β V β§ (0..^π) β V) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
36 | 32, 34, 35 | sylancl 586 |
. . . . . . . . . . . . . 14
β’ (π β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
37 | 36 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
38 | 29, 37 | mpbird 256 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)) β (π΄ βm (0..^π))) |
39 | 33 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^π) β Fin) |
40 | | nnsscn 12221 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β β |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β
β) |
42 | 1, 41 | sstrd 3992 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β β) |
43 | 42 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π΄ β β) |
44 | 28 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) β π΄) |
45 | 43, 44 | sseldd 3983 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) β β) |
46 | 39, 45 | fsumcl 15683 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) β β) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) β β) |
48 | 42 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π΄ β β) |
49 | 25, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π β (0..^(π + 1))) |
50 | 24, 49 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (πβπ) β π΄) |
51 | 48, 50 | sseldd 3983 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (πβπ) β β) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β β) |
53 | 47, 52 | pncand 11576 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) β (πβπ)) = Ξ£π β (0..^π)((π βΎ (0..^π))βπ)) |
54 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β§ π β (π΄ βm (0..^(π + 1)))) |
55 | | nfcv 2903 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(πβπ) |
56 | | fzonel 13650 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬
π β (0..^π) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Β¬ π β (0..^π)) |
58 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π:(0..^(π + 1))βΆπ΄) |
59 | 27 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π β (0..^(π + 1))) |
60 | 58, 59 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β (πβπ) β π΄) |
61 | 43, 60 | sseldd 3983 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β (πβπ) β β) |
62 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
63 | 54, 55, 39, 25, 57, 61, 62, 51 | fsumsplitsn 15694 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β ((0..^π) βͺ {π})(πβπ) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
64 | | fzosplitsn 13744 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
65 | | nn0uz 12868 |
. . . . . . . . . . . . . . . . . . . 20
β’
β0 = (β€β₯β0) |
66 | 64, 65 | eleq2s 2851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (0..^(π + 1)) =
((0..^π) βͺ {π})) |
67 | 25, 66 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
68 | 67 | sumeq1d 15651 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β ((0..^π) βͺ {π})(πβπ)) |
69 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π β (0..^π)) |
70 | 69 | fvresd 6911 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) = (πβπ)) |
71 | 70 | sumeq2dv 15653 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = Ξ£π β (0..^π)(πβπ)) |
72 | 71 | oveq1d 7426 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
73 | 63, 68, 72 | 3eqtr4d 2782 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^(π + 1))(πβπ) = (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ))) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^(π + 1))(πβπ) = (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ))) |
75 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^(π + 1))(πβπ) = π) |
76 | 74, 75 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) = π) |
77 | 76 | oveq1d 7426 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) β (πβπ)) = (π β (πβπ))) |
78 | 53, 77 | eqtr3d 2774 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ))) |
79 | 38, 78 | jca 512 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ)))) |
80 | | fveq1 6890 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (0..^π)) β (πβπ) = ((π βΎ (0..^π))βπ)) |
81 | 80 | sumeq2sdv 15654 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (0..^π)) β Ξ£π β (0..^π)(πβπ) = Ξ£π β (0..^π)((π βΎ (0..^π))βπ)) |
82 | 81 | eqeq1d 2734 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (0..^π)) β (Ξ£π β (0..^π)(πβπ) = (π β (πβπ)) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ)))) |
83 | 82 | elrab 3683 |
. . . . . . . . . . 11
β’ ((π βΎ (0..^π)) β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β (πβπ))} β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ)))) |
84 | 79, 83 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)) β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β (πβπ))}) |
85 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π΄ β β) |
86 | 2 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β β€) |
87 | | nnssz 12584 |
. . . . . . . . . . . . . . 15
β’ β
β β€ |
88 | 1, 87 | sstrdi 3994 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β€) |
89 | 88 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π΄ β β€) |
90 | 89, 14 | sseldd 3983 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β β€) |
91 | 86, 90 | zsubcld 12675 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π β (πβπ)) β β€) |
92 | 85, 91, 11 | reprval 33908 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π΄(reprβπ)(π β (πβπ))) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β (πβπ))}) |
93 | 84, 92 | eleqtrrd 2836 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)) β (π΄(reprβπ)(π β (πβπ)))) |
94 | | simpr 485 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β π = (π βΎ (0..^π))) |
95 | 94 | uneq1d 4162 |
. . . . . . . . . 10
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β (π βͺ {β¨π, (πβπ)β©}) = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
96 | 95 | eqeq2d 2743 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β (π = (π βͺ {β¨π, (πβπ)β©}) β π = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©}))) |
97 | 10 | ffnd 6718 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π Fn (0..^(π + 1))) |
98 | | fnsnsplit 7184 |
. . . . . . . . . . 11
β’ ((π Fn (0..^(π + 1)) β§ π β (0..^(π + 1))) β π = ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©})) |
99 | 97, 13, 98 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π = ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©})) |
100 | 11, 65 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β
(β€β₯β0)) |
101 | | fzodif2 32258 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β0) β ((0..^(π + 1)) β {π}) = (0..^π)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((0..^(π + 1)) β {π}) = (0..^π)) |
103 | 102 | reseq2d 5981 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ ((0..^(π + 1)) β {π})) = (π βΎ (0..^π))) |
104 | 103 | uneq1d 4162 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©}) = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
105 | 99, 104 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
106 | 93, 96, 105 | rspcedvd 3614 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β (π΄(reprβπ)(π β (πβπ)))π = (π βͺ {β¨π, (πβπ)β©})) |
107 | 14, 23, 106 | rspcedvd 3614 |
. . . . . . 7
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
108 | 107 | anasss 467 |
. . . . . 6
β’ ((π β§ (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
109 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π = (π βͺ {β¨π, πβ©})) |
110 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π΄ β β) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π΄ β β) |
112 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β β€) |
113 | 88 | sselda 3982 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β β€) |
114 | 112, 113 | zsubcld 12675 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π β π) β β€) |
115 | 114 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π β π) β β€) |
116 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β
β0) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β
β0) |
118 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β (π΄(reprβπ)(π β π))) |
119 | 111, 115,
117, 118 | reprf 33910 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π:(0..^π)βΆπ΄) |
120 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β π΄) |
121 | 117, 120 | fsnd 6876 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β {β¨π, πβ©}:{π}βΆπ΄) |
122 | | fzodisjsn 13674 |
. . . . . . . . . . . . . 14
β’
((0..^π) β©
{π}) =
β
|
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((0..^π) β© {π}) = β
) |
124 | 119, 121,
123 | fun2d 6755 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆπ΄) |
125 | 117, 66 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
126 | 125 | feq2d 6703 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄ β (π βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆπ΄)) |
127 | 124, 126 | mpbird 256 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄) |
128 | | ovex 7444 |
. . . . . . . . . . . . 13
β’
(0..^(π + 1)) β
V |
129 | | elmapg 8835 |
. . . . . . . . . . . . 13
β’ ((π΄ β V β§ (0..^(π + 1)) β V) β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
130 | 32, 128, 129 | sylancl 586 |
. . . . . . . . . . . 12
β’ (π β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
131 | 130 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
132 | 127, 131 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1)))) |
133 | 132 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1)))) |
134 | 109, 133 | eqeltrd 2833 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (π΄ βm (0..^(π + 1)))) |
135 | 125 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
136 | 135 | sumeq1d 15651 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β ((0..^π) βͺ {π})(πβπ)) |
137 | | nfv 1917 |
. . . . . . . . . 10
β’
β²π(((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) |
138 | 33 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (0..^π) β Fin) |
139 | 117 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β
β0) |
140 | 56 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Β¬ π β (0..^π)) |
141 | 42 | ad4antr 730 |
. . . . . . . . . . 11
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π΄ β β) |
142 | 127 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄) |
143 | 109 | feq1d 6702 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π:(0..^(π + 1))βΆπ΄ β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
144 | 142, 143 | mpbird 256 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π:(0..^(π + 1))βΆπ΄) |
145 | 144 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π:(0..^(π + 1))βΆπ΄) |
146 | | simpr 485 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β (0..^π)) |
147 | | elun1 4176 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β ((0..^π) βͺ {π})) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β ((0..^π) βͺ {π})) |
149 | 125 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
150 | 148, 149 | eleqtrrd 2836 |
. . . . . . . . . . . 12
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β (0..^(π + 1))) |
151 | 145, 150 | ffvelcdmd 7087 |
. . . . . . . . . . 11
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) β π΄) |
152 | 141, 151 | sseldd 3983 |
. . . . . . . . . 10
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) β β) |
153 | 42 | ad3antrrr 728 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π΄ β β) |
154 | 139, 12 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (0..^(π + 1))) |
155 | 144, 154 | ffvelcdmd 7087 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) β π΄) |
156 | 153, 155 | sseldd 3983 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) β β) |
157 | 137, 55, 138, 139, 140, 152, 62, 156 | fsumsplitsn 15694 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β ((0..^π) βͺ {π})(πβπ) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
158 | | simplr 767 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π = (π βͺ {β¨π, πβ©})) |
159 | 158 | fveq1d 6893 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
160 | 119 | ffnd 6718 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π Fn (0..^π)) |
161 | 160 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π Fn (0..^π)) |
162 | 121 | ffnd 6718 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β {β¨π, πβ©} Fn {π}) |
163 | 162 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β {β¨π, πβ©} Fn {π}) |
164 | 122 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β ((0..^π) β© {π}) = β
) |
165 | | fvun1 6982 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β (0..^π))) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
166 | 161, 163,
164, 146, 165 | syl112anc 1374 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
167 | 159, 166 | eqtrd 2772 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) = (πβπ)) |
168 | 167 | ralrimiva 3146 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β βπ β (0..^π)(πβπ) = (πβπ)) |
169 | 168 | sumeq2d 15652 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = Ξ£π β (0..^π)(πβπ)) |
170 | 111 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π΄ β β) |
171 | 115 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π β π) β β€) |
172 | 118 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (π΄(reprβπ)(π β π))) |
173 | 170, 171,
139, 172 | reprsum 33911 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = (π β π)) |
174 | 169, 173 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = (π β π)) |
175 | 109 | fveq1d 6893 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
176 | 160 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π Fn (0..^π)) |
177 | 162 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β {β¨π, πβ©} Fn {π}) |
178 | 122 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((0..^π) β© {π}) = β
) |
179 | | snidg 4662 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β {π}) |
180 | 139, 179 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β {π}) |
181 | | fvun2 6983 |
. . . . . . . . . . . . 13
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β {π})) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
182 | 176, 177,
178, 180, 181 | syl112anc 1374 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
183 | 120 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β π΄) |
184 | | fvsng 7180 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β π΄) β ({β¨π, πβ©}βπ) = π) |
185 | 139, 183,
184 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ({β¨π, πβ©}βπ) = π) |
186 | 175, 182,
185 | 3eqtrd 2776 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) = π) |
187 | 174, 186 | oveq12d 7429 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (Ξ£π β (0..^π)(πβπ) + (πβπ)) = ((π β π) + π)) |
188 | | zsscn 12570 |
. . . . . . . . . . . 12
β’ β€
β β |
189 | 112 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β€) |
190 | 188, 189 | sselid 3980 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β) |
191 | 186, 156 | eqeltrrd 2834 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β) |
192 | 190, 191 | npcand 11579 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((π β π) + π) = π) |
193 | 187, 192 | eqtrd 2772 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (Ξ£π β (0..^π)(πβπ) + (πβπ)) = π) |
194 | 136, 157,
193 | 3eqtrd 2776 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^(π + 1))(πβπ) = π) |
195 | 134, 194 | jca 512 |
. . . . . . 7
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
196 | 195 | r19.29ffa 31968 |
. . . . . 6
β’ ((π β§ βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
197 | 108, 196 | impbida 799 |
. . . . 5
β’ (π β ((π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©}))) |
198 | | reprsuc.f |
. . . . . . 7
β’ πΉ = (π β (π΄(reprβπ)(π β π)) β¦ (π βͺ {β¨π, πβ©})) |
199 | | vex 3478 |
. . . . . . . 8
β’ π β V |
200 | | snex 5431 |
. . . . . . . 8
β’
{β¨π, πβ©} β
V |
201 | 199, 200 | unex 7735 |
. . . . . . 7
β’ (π βͺ {β¨π, πβ©}) β V |
202 | 198, 201 | elrnmpti 5959 |
. . . . . 6
β’ (π β ran πΉ β βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
203 | 202 | rexbii 3094 |
. . . . 5
β’
(βπ β
π΄ π β ran πΉ β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
204 | 197, 203 | bitr4di 288 |
. . . 4
β’ (π β ((π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ π β ran πΉ)) |
205 | | fveq1 6890 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
206 | 205 | sumeq2sdv 15654 |
. . . . . . 7
β’ (π = π β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β (0..^(π + 1))(πβπ)) |
207 | 206 | eqeq1d 2734 |
. . . . . 6
β’ (π = π β (Ξ£π β (0..^(π + 1))(πβπ) = π β Ξ£π β (0..^(π + 1))(πβπ) = π)) |
208 | 207 | cbvrabv 3442 |
. . . . 5
β’ {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} = {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} |
209 | 208 | reqabi 3454 |
. . . 4
β’ (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
210 | | eliun 5001 |
. . . 4
β’ (π β βͺ π β π΄ ran πΉ β βπ β π΄ π β ran πΉ) |
211 | 204, 209,
210 | 3bitr4g 313 |
. . 3
β’ (π β (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} β π β βͺ
π β π΄ ran πΉ)) |
212 | 211 | eqrdv 2730 |
. 2
β’ (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} = βͺ
π β π΄ ran πΉ) |
213 | 7, 212 | eqtrd 2772 |
1
β’ (π β (π΄(reprβ(π + 1))π) = βͺ
π β π΄ ran πΉ) |