Step | Hyp | Ref
| Expression |
1 | | df-repr 33609 |
. . 3
β’ repr =
(π β
β0 β¦ (π β π« β, π β β€ β¦ {π β (π βm (0..^π )) β£ Ξ£π β (0..^π )(πβπ) = π})) |
2 | | oveq2 7413 |
. . . . . 6
β’ (π = π β (0..^π ) = (0..^π)) |
3 | 2 | oveq2d 7421 |
. . . . 5
β’ (π = π β (π βm (0..^π )) = (π βm (0..^π))) |
4 | 2 | sumeq1d 15643 |
. . . . . 6
β’ (π = π β Ξ£π β (0..^π )(πβπ) = Ξ£π β (0..^π)(πβπ)) |
5 | 4 | eqeq1d 2734 |
. . . . 5
β’ (π = π β (Ξ£π β (0..^π )(πβπ) = π β Ξ£π β (0..^π)(πβπ) = π)) |
6 | 3, 5 | rabeqbidv 3449 |
. . . 4
β’ (π = π β {π β (π βm (0..^π )) β£ Ξ£π β (0..^π )(πβπ) = π} = {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
7 | 6 | mpoeq3dv 7484 |
. . 3
β’ (π = π β (π β π« β, π β β€ β¦ {π β (π βm (0..^π )) β£ Ξ£π β (0..^π )(πβπ) = π}) = (π β π« β, π β β€ β¦ {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
8 | | reprval.s |
. . 3
β’ (π β π β
β0) |
9 | | nnex 12214 |
. . . . . 6
β’ β
β V |
10 | 9 | pwex 5377 |
. . . . 5
β’ π«
β β V |
11 | | zex 12563 |
. . . . 5
β’ β€
β V |
12 | 10, 11 | mpoex 8062 |
. . . 4
β’ (π β π« β, π β β€ β¦ {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) β V |
13 | 12 | a1i 11 |
. . 3
β’ (π β (π β π« β, π β β€ β¦ {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) β V) |
14 | 1, 7, 8, 13 | fvmptd3 7018 |
. 2
β’ (π β (reprβπ) = (π β π« β, π β β€ β¦ {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π})) |
15 | | simprl 769 |
. . . 4
β’ ((π β§ (π = π΄ β§ π = π)) β π = π΄) |
16 | 15 | oveq1d 7420 |
. . 3
β’ ((π β§ (π = π΄ β§ π = π)) β (π βm (0..^π)) = (π΄ βm (0..^π))) |
17 | | simprr 771 |
. . . 4
β’ ((π β§ (π = π΄ β§ π = π)) β π = π) |
18 | 17 | eqeq2d 2743 |
. . 3
β’ ((π β§ (π = π΄ β§ π = π)) β (Ξ£π β (0..^π)(πβπ) = π β Ξ£π β (0..^π)(πβπ) = π)) |
19 | 16, 18 | rabeqbidv 3449 |
. 2
β’ ((π β§ (π = π΄ β§ π = π)) β {π β (π βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
20 | 9 | a1i 11 |
. . . 4
β’ (π β β β
V) |
21 | | reprval.a |
. . . 4
β’ (π β π΄ β β) |
22 | 20, 21 | ssexd 5323 |
. . 3
β’ (π β π΄ β V) |
23 | 22, 21 | elpwd 4607 |
. 2
β’ (π β π΄ β π« β) |
24 | | reprval.m |
. 2
β’ (π β π β β€) |
25 | | ovex 7438 |
. . . 4
β’ (π΄ βm (0..^π)) β V |
26 | 25 | rabex 5331 |
. . 3
β’ {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β V |
27 | 26 | a1i 11 |
. 2
β’ (π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β V) |
28 | 14, 19, 23, 24, 27 | ovmpod 7556 |
1
β’ (π β (π΄(reprβπ)π) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |