Step | Hyp | Ref
| Expression |
1 | | vdwapfval 16903 |
. . . . . . 7
โข (๐พ โ โ0
โ (APโ๐พ) =
(๐ โ โ, ๐ โ โ โฆ ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))))) |
2 | 1 | 3ad2ant1 1133 |
. . . . . 6
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (APโ๐พ) =
(๐ โ โ, ๐ โ โ โฆ ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))))) |
3 | 2 | oveqd 7425 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด(APโ๐พ)๐ท) = (๐ด(๐ โ โ, ๐ โ โ โฆ ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))))๐ท)) |
4 | | oveq2 7416 |
. . . . . . . . . 10
โข (๐ = ๐ท โ (๐ ยท ๐) = (๐ ยท ๐ท)) |
5 | | oveq12 7417 |
. . . . . . . . . 10
โข ((๐ = ๐ด โง (๐ ยท ๐) = (๐ ยท ๐ท)) โ (๐ + (๐ ยท ๐)) = (๐ด + (๐ ยท ๐ท))) |
6 | 4, 5 | sylan2 593 |
. . . . . . . . 9
โข ((๐ = ๐ด โง ๐ = ๐ท) โ (๐ + (๐ ยท ๐)) = (๐ด + (๐ ยท ๐ท))) |
7 | 6 | mpteq2dv 5250 |
. . . . . . . 8
โข ((๐ = ๐ด โง ๐ = ๐ท) โ (๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))) = (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท)))) |
8 | 7 | rneqd 5937 |
. . . . . . 7
โข ((๐ = ๐ด โง ๐ = ๐ท) โ ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))) = ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท)))) |
9 | | eqid 2732 |
. . . . . . 7
โข (๐ โ โ, ๐ โ โ โฆ ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐)))) = (๐ โ โ, ๐ โ โ โฆ ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐)))) |
10 | | ovex 7441 |
. . . . . . . . 9
โข
(0...(๐พ โ 1))
โ V |
11 | 10 | mptex 7224 |
. . . . . . . 8
โข (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท))) โ V |
12 | 11 | rnex 7902 |
. . . . . . 7
โข ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท))) โ V |
13 | 8, 9, 12 | ovmpoa 7562 |
. . . . . 6
โข ((๐ด โ โ โง ๐ท โ โ) โ (๐ด(๐ โ โ, ๐ โ โ โฆ ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))))๐ท) = ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท)))) |
14 | 13 | 3adant1 1130 |
. . . . 5
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด(๐ โ โ, ๐ โ โ โฆ ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ + (๐ ยท ๐))))๐ท) = ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท)))) |
15 | 3, 14 | eqtrd 2772 |
. . . 4
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด(APโ๐พ)๐ท) = ran (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท)))) |
16 | | eqid 2732 |
. . . . 5
โข (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท))) = (๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท))) |
17 | 16 | rnmpt 5954 |
. . . 4
โข ran
(๐ โ (0...(๐พ โ 1)) โฆ (๐ด + (๐ ยท ๐ท))) = {๐ฅ โฃ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท))} |
18 | 15, 17 | eqtrdi 2788 |
. . 3
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ด(APโ๐พ)๐ท) = {๐ฅ โฃ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท))}) |
19 | 18 | eleq2d 2819 |
. 2
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ โ (๐ด(APโ๐พ)๐ท) โ ๐ โ {๐ฅ โฃ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท))})) |
20 | | id 22 |
. . . . 5
โข (๐ = (๐ด + (๐ ยท ๐ท)) โ ๐ = (๐ด + (๐ ยท ๐ท))) |
21 | | ovex 7441 |
. . . . 5
โข (๐ด + (๐ ยท ๐ท)) โ V |
22 | 20, 21 | eqeltrdi 2841 |
. . . 4
โข (๐ = (๐ด + (๐ ยท ๐ท)) โ ๐ โ V) |
23 | 22 | rexlimivw 3151 |
. . 3
โข
(โ๐ โ
(0...(๐พ โ 1))๐ = (๐ด + (๐ ยท ๐ท)) โ ๐ โ V) |
24 | | eqeq1 2736 |
. . . 4
โข (๐ฅ = ๐ โ (๐ฅ = (๐ด + (๐ ยท ๐ท)) โ ๐ = (๐ด + (๐ ยท ๐ท)))) |
25 | 24 | rexbidv 3178 |
. . 3
โข (๐ฅ = ๐ โ (โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท)) โ โ๐ โ (0...(๐พ โ 1))๐ = (๐ด + (๐ ยท ๐ท)))) |
26 | 23, 25 | elab3 3676 |
. 2
โข (๐ โ {๐ฅ โฃ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ด + (๐ ยท ๐ท))} โ โ๐ โ (0...(๐พ โ 1))๐ = (๐ด + (๐ ยท ๐ท))) |
27 | 19, 26 | bitrdi 286 |
1
โข ((๐พ โ โ0
โง ๐ด โ โ
โง ๐ท โ โ)
โ (๐ โ (๐ด(APโ๐พ)๐ท) โ โ๐ โ (0...(๐พ โ 1))๐ = (๐ด + (๐ ยท ๐ท)))) |