Step | Hyp | Ref
| Expression |
1 | | reprval.a |
. . 3
β’ (π β π΄ β β) |
2 | | reprval.m |
. . 3
β’ (π β π β β€) |
3 | | reprval.s |
. . . 4
β’ (π β π β
β0) |
4 | | 1nn0 12488 |
. . . . 5
β’ 1 β
β0 |
5 | 4 | a1i 11 |
. . . 4
β’ (π β 1 β
β0) |
6 | 3, 5 | nn0addcld 12536 |
. . 3
β’ (π β (π + 1) β
β0) |
7 | 1, 2, 6 | reprval 33653 |
. 2
β’ (π β (π΄(reprβ(π + 1))π) = {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π}) |
8 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β (π΄ βm (0..^(π + 1)))) |
9 | | elmapi 8843 |
. . . . . . . . . 10
β’ (π β (π΄ βm (0..^(π + 1))) β π:(0..^(π + 1))βΆπ΄) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π:(0..^(π + 1))βΆπ΄) |
11 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β
β0) |
12 | | fzonn0p1 13709 |
. . . . . . . . . 10
β’ (π β β0
β π β (0..^(π + 1))) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β (0..^(π + 1))) |
14 | 10, 13 | ffvelcdmd 7088 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β π΄) |
15 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β π = (πβπ)) |
16 | 15 | oveq2d 7425 |
. . . . . . . . . 10
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π β π) = (π β (πβπ))) |
17 | 16 | oveq2d 7425 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π΄(reprβπ)(π β π)) = (π΄(reprβπ)(π β (πβπ)))) |
18 | | opeq2 4875 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β β¨π, πβ© = β¨π, (πβπ)β©) |
19 | 18 | sneqd 4641 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β {β¨π, πβ©} = {β¨π, (πβπ)β©}) |
20 | 19 | uneq2d 4164 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (π βͺ {β¨π, πβ©}) = (π βͺ {β¨π, (πβπ)β©})) |
21 | 20 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (π = (πβπ) β (π = (π βͺ {β¨π, πβ©}) β π = (π βͺ {β¨π, (πβπ)β©}))) |
22 | 21 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (π = (π βͺ {β¨π, πβ©}) β π = (π βͺ {β¨π, (πβπ)β©}))) |
23 | 17, 22 | rexeqbidv 3344 |
. . . . . . . 8
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (πβπ)) β (βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©}) β βπ β (π΄(reprβπ)(π β (πβπ)))π = (π βͺ {β¨π, (πβπ)β©}))) |
24 | 9 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π:(0..^(π + 1))βΆπ΄) |
25 | 3 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π β
β0) |
26 | | fzossfzop1 13710 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^π) β (0..^(π + 1))) |
28 | 24, 27 | fssresd 6759 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (π βΎ (0..^π)):(0..^π)βΆπ΄) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)):(0..^π)βΆπ΄) |
30 | | nnex 12218 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
V) |
32 | 31, 1 | ssexd 5325 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β V) |
33 | | fzofi 13939 |
. . . . . . . . . . . . . . . 16
β’
(0..^π) β
Fin |
34 | 33 | elexi 3494 |
. . . . . . . . . . . . . . 15
β’
(0..^π) β
V |
35 | | elmapg 8833 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β V β§ (0..^π) β V) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
36 | 32, 34, 35 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β (π βΎ (0..^π)):(0..^π)βΆπ΄)) |
38 | 29, 37 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)) β (π΄ βm (0..^π))) |
39 | 33 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^π) β Fin) |
40 | | nnsscn 12217 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β β |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β
β) |
42 | 1, 41 | sstrd 3993 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β β) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π΄ β β) |
44 | 28 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) β π΄) |
45 | 43, 44 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) β β) |
46 | 39, 45 | fsumcl 15679 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) β β) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) β β) |
48 | 42 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π΄ β β) |
49 | 25, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β π β (0..^(π + 1))) |
50 | 24, 49 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (πβπ) β π΄) |
51 | 48, 50 | sseldd 3984 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (πβπ) β β) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β β) |
53 | 47, 52 | pncand 11572 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) β (πβπ)) = Ξ£π β (0..^π)((π βΎ (0..^π))βπ)) |
54 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β§ π β (π΄ βm (0..^(π + 1)))) |
55 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(πβπ) |
56 | | fzonel 13646 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬
π β (0..^π) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Β¬ π β (0..^π)) |
58 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π:(0..^(π + 1))βΆπ΄) |
59 | 27 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π β (0..^(π + 1))) |
60 | 58, 59 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β (πβπ) β π΄) |
61 | 43, 60 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β (πβπ) β β) |
62 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
63 | 54, 55, 39, 25, 57, 61, 62, 51 | fsumsplitsn 15690 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β ((0..^π) βͺ {π})(πβπ) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
64 | | fzosplitsn 13740 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
65 | | nn0uz 12864 |
. . . . . . . . . . . . . . . . . . . 20
β’
β0 = (β€β₯β0) |
66 | 64, 65 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (0..^(π + 1)) =
((0..^π) βͺ {π})) |
67 | 25, 66 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
68 | 67 | sumeq1d 15647 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β ((0..^π) βͺ {π})(πβπ)) |
69 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β π β (0..^π)) |
70 | 69 | fvresd 6912 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ π β (0..^π)) β ((π βΎ (0..^π))βπ) = (πβπ)) |
71 | 70 | sumeq2dv 15649 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = Ξ£π β (0..^π)(πβπ)) |
72 | 71 | oveq1d 7424 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
73 | 63, 68, 72 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΄ βm (0..^(π + 1)))) β Ξ£π β (0..^(π + 1))(πβπ) = (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ))) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^(π + 1))(πβπ) = (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ))) |
75 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^(π + 1))(πβπ) = π) |
76 | 74, 75 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) = π) |
77 | 76 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((Ξ£π β (0..^π)((π βΎ (0..^π))βπ) + (πβπ)) β (πβπ)) = (π β (πβπ))) |
78 | 53, 77 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ))) |
79 | 38, 78 | jca 513 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ (0..^π)) β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ)))) |
80 | | fveq1 6891 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (0..^π)) β (πβπ) = ((π βΎ (0..^π))βπ)) |
81 | 80 | sumeq2sdv 15650 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (0..^π)) β Ξ£π β (0..^π)(πβπ) = Ξ£π β (0..^π)((π βΎ (0..^π))βπ)) |
82 | 81 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (0..^π)) β (Ξ£π β (0..^π)(πβπ) = (π β (πβπ)) β Ξ£π β (0..^π)((π βΎ (0..^π))βπ) = (π β (πβπ)))) |
83 | 82 | elrab 3684 |
. . . . . . . . . . 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 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π΄ β β) |
86 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β β€) |
87 | | nnssz 12580 |
. . . . . . . . . . . . . . 15
β’ β
β β€ |
88 | 1, 87 | sstrdi 3995 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β€) |
89 | 88 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π΄ β β€) |
90 | 89, 14 | sseldd 3984 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (πβπ) β β€) |
91 | 86, 90 | zsubcld 12671 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π β (πβπ)) β β€) |
92 | 85, 91, 11 | reprval 33653 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π΄(reprβπ)(π β (πβπ))) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β (πβπ))}) |
93 | 84, 92 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ (0..^π)) β (π΄(reprβπ)(π β (πβπ)))) |
94 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β π = (π βΎ (0..^π))) |
95 | 94 | uneq1d 4163 |
. . . . . . . . . 10
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β (π βͺ {β¨π, (πβπ)β©}) = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
96 | 95 | eqeq2d 2744 |
. . . . . . . . 9
β’ ((((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β§ π = (π βΎ (0..^π))) β (π = (π βͺ {β¨π, (πβπ)β©}) β π = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©}))) |
97 | 10 | ffnd 6719 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π Fn (0..^(π + 1))) |
98 | | fnsnsplit 7182 |
. . . . . . . . . . 11
β’ ((π Fn (0..^(π + 1)) β§ π β (0..^(π + 1))) β π = ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©})) |
99 | 97, 13, 98 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π = ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©})) |
100 | 11, 65 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π β
(β€β₯β0)) |
101 | | fzodif2 32034 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β0) β ((0..^(π + 1)) β {π}) = (0..^π)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((0..^(π + 1)) β {π}) = (0..^π)) |
103 | 102 | reseq2d 5982 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β (π βΎ ((0..^(π + 1)) β {π})) = (π βΎ (0..^π))) |
104 | 103 | uneq1d 4163 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β ((π βΎ ((0..^(π + 1)) β {π})) βͺ {β¨π, (πβπ)β©}) = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
105 | 99, 104 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β π = ((π βΎ (0..^π)) βͺ {β¨π, (πβπ)β©})) |
106 | 93, 96, 105 | rspcedvd 3615 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β (π΄(reprβπ)(π β (πβπ)))π = (π βͺ {β¨π, (πβπ)β©})) |
107 | 14, 23, 106 | rspcedvd 3615 |
. . . . . . 7
β’ (((π β§ π β (π΄ βm (0..^(π + 1)))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
108 | 107 | anasss 468 |
. . . . . 6
β’ ((π β§ (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
109 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π = (π βͺ {β¨π, πβ©})) |
110 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π΄ β β) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π΄ β β) |
112 | 2 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β β€) |
113 | 88 | sselda 3983 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β β€) |
114 | 112, 113 | zsubcld 12671 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π β π) β β€) |
115 | 114 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π β π) β β€) |
116 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β
β0) |
117 | 116 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β
β0) |
118 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β (π΄(reprβπ)(π β π))) |
119 | 111, 115,
117, 118 | reprf 33655 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π:(0..^π)βΆπ΄) |
120 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π β π΄) |
121 | 117, 120 | fsnd 6877 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β {β¨π, πβ©}:{π}βΆπ΄) |
122 | | fzodisjsn 13670 |
. . . . . . . . . . . . . 14
β’
((0..^π) β©
{π}) =
β
|
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((0..^π) β© {π}) = β
) |
124 | 119, 121,
123 | fun2d 6756 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆπ΄) |
125 | 117, 66 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
126 | 125 | feq2d 6704 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄ β (π βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆπ΄)) |
127 | 124, 126 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄) |
128 | | ovex 7442 |
. . . . . . . . . . . . 13
β’
(0..^(π + 1)) β
V |
129 | | elmapg 8833 |
. . . . . . . . . . . . 13
β’ ((π΄ β V β§ (0..^(π + 1)) β V) β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
130 | 32, 128, 129 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
131 | 130 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1))) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
132 | 127, 131 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1)))) |
133 | 132 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π βͺ {β¨π, πβ©}) β (π΄ βm (0..^(π + 1)))) |
134 | 109, 133 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (π΄ βm (0..^(π + 1)))) |
135 | 125 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
136 | 135 | sumeq1d 15647 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β ((0..^π) βͺ {π})(πβπ)) |
137 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) |
138 | 33 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (0..^π) β Fin) |
139 | 117 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β
β0) |
140 | 56 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Β¬ π β (0..^π)) |
141 | 42 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π΄ β β) |
142 | 127 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄) |
143 | 109 | feq1d 6703 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π:(0..^(π + 1))βΆπ΄ β (π βͺ {β¨π, πβ©}):(0..^(π + 1))βΆπ΄)) |
144 | 142, 143 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π:(0..^(π + 1))βΆπ΄) |
145 | 144 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π:(0..^(π + 1))βΆπ΄) |
146 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β (0..^π)) |
147 | | elun1 4177 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β ((0..^π) βͺ {π})) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β ((0..^π) βͺ {π})) |
149 | 125 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
150 | 148, 149 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π β (0..^(π + 1))) |
151 | 145, 150 | ffvelcdmd 7088 |
. . . . . . . . . . 11
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) β π΄) |
152 | 141, 151 | sseldd 3984 |
. . . . . . . . . 10
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) β β) |
153 | 42 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π΄ β β) |
154 | 139, 12 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (0..^(π + 1))) |
155 | 144, 154 | ffvelcdmd 7088 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) β π΄) |
156 | 153, 155 | sseldd 3984 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) β β) |
157 | 137, 55, 138, 139, 140, 152, 62, 156 | fsumsplitsn 15690 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β ((0..^π) βͺ {π})(πβπ) = (Ξ£π β (0..^π)(πβπ) + (πβπ))) |
158 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π = (π βͺ {β¨π, πβ©})) |
159 | 158 | fveq1d 6894 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
160 | 119 | ffnd 6719 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β π Fn (0..^π)) |
161 | 160 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β π Fn (0..^π)) |
162 | 121 | ffnd 6719 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β {β¨π, πβ©} Fn {π}) |
163 | 162 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β {β¨π, πβ©} Fn {π}) |
164 | 122 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β ((0..^π) β© {π}) = β
) |
165 | | fvun1 6983 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β (0..^π))) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
166 | 161, 163,
164, 146, 165 | syl112anc 1375 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
167 | 159, 166 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β§ π β (0..^π)) β (πβπ) = (πβπ)) |
168 | 167 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β βπ β (0..^π)(πβπ) = (πβπ)) |
169 | 168 | sumeq2d 15648 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = Ξ£π β (0..^π)(πβπ)) |
170 | 111 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π΄ β β) |
171 | 115 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π β π) β β€) |
172 | 118 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β (π΄(reprβπ)(π β π))) |
173 | 170, 171,
139, 172 | reprsum 33656 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = (π β π)) |
174 | 169, 173 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^π)(πβπ) = (π β π)) |
175 | 109 | fveq1d 6894 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
176 | 160 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π Fn (0..^π)) |
177 | 162 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β {β¨π, πβ©} Fn {π}) |
178 | 122 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((0..^π) β© {π}) = β
) |
179 | | snidg 4663 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β {π}) |
180 | 139, 179 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β {π}) |
181 | | fvun2 6984 |
. . . . . . . . . . . . 13
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β {π})) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
182 | 176, 177,
178, 180, 181 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
183 | 120 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β π΄) |
184 | | fvsng 7178 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β π΄) β ({β¨π, πβ©}βπ) = π) |
185 | 139, 183,
184 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ({β¨π, πβ©}βπ) = π) |
186 | 175, 182,
185 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (πβπ) = π) |
187 | 174, 186 | oveq12d 7427 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (Ξ£π β (0..^π)(πβπ) + (πβπ)) = ((π β π) + π)) |
188 | | zsscn 12566 |
. . . . . . . . . . . 12
β’ β€
β β |
189 | 112 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β€) |
190 | 188, 189 | sselid 3981 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β) |
191 | 186, 156 | eqeltrrd 2835 |
. . . . . . . . . . 11
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β π β β) |
192 | 190, 191 | npcand 11575 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β ((π β π) + π) = π) |
193 | 187, 192 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (Ξ£π β (0..^π)(πβπ) + (πβπ)) = π) |
194 | 136, 157,
193 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β Ξ£π β (0..^(π + 1))(πβπ) = π) |
195 | 134, 194 | jca 513 |
. . . . . . 7
β’ ((((π β§ π β π΄) β§ π β (π΄(reprβπ)(π β π))) β§ π = (π βͺ {β¨π, πβ©})) β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
196 | 195 | r19.29ffa 31744 |
. . . . . 6
β’ ((π β§ βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
197 | 108, 196 | impbida 800 |
. . . . 5
β’ (π β ((π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©}))) |
198 | | reprsuc.f |
. . . . . . 7
β’ πΉ = (π β (π΄(reprβπ)(π β π)) β¦ (π βͺ {β¨π, πβ©})) |
199 | | vex 3479 |
. . . . . . . 8
β’ π β V |
200 | | snex 5432 |
. . . . . . . 8
β’
{β¨π, πβ©} β
V |
201 | 199, 200 | unex 7733 |
. . . . . . 7
β’ (π βͺ {β¨π, πβ©}) β V |
202 | 198, 201 | elrnmpti 5960 |
. . . . . 6
β’ (π β ran πΉ β βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
203 | 202 | rexbii 3095 |
. . . . 5
β’
(βπ β
π΄ π β ran πΉ β βπ β π΄ βπ β (π΄(reprβπ)(π β π))π = (π βͺ {β¨π, πβ©})) |
204 | 197, 203 | bitr4di 289 |
. . . 4
β’ (π β ((π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π) β βπ β π΄ π β ran πΉ)) |
205 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
206 | 205 | sumeq2sdv 15650 |
. . . . . . 7
β’ (π = π β Ξ£π β (0..^(π + 1))(πβπ) = Ξ£π β (0..^(π + 1))(πβπ)) |
207 | 206 | eqeq1d 2735 |
. . . . . 6
β’ (π = π β (Ξ£π β (0..^(π + 1))(πβπ) = π β Ξ£π β (0..^(π + 1))(πβπ) = π)) |
208 | 207 | cbvrabv 3443 |
. . . . 5
β’ {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} = {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} |
209 | 208 | reqabi 3455 |
. . . 4
β’ (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} β (π β (π΄ βm (0..^(π + 1))) β§ Ξ£π β (0..^(π + 1))(πβπ) = π)) |
210 | | eliun 5002 |
. . . 4
β’ (π β βͺ π β π΄ ran πΉ β βπ β π΄ π β ran πΉ) |
211 | 204, 209,
210 | 3bitr4g 314 |
. . 3
β’ (π β (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} β π β βͺ
π β π΄ ran πΉ)) |
212 | 211 | eqrdv 2731 |
. 2
β’ (π β {π β (π΄ βm (0..^(π + 1))) β£ Ξ£π β (0..^(π + 1))(πβπ) = π} = βͺ
π β π΄ ran πΉ) |
213 | 7, 212 | eqtrd 2773 |
1
β’ (π β (π΄(reprβ(π + 1))π) = βͺ
π β π΄ ran πΉ) |