Step | Hyp | Ref
| Expression |
1 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ = ๐ด โ (๐โ2) = (๐ดโ2)) |
2 | 1 | fvoveq1d 7383 |
. . . . . . . . 9
โข (๐ = ๐ด โ (โโ((๐โ2) โ 1)) = (โโ((๐ดโ2) โ
1))) |
3 | 2 | oveq1d 7376 |
. . . . . . . 8
โข (๐ = ๐ด โ ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)) =
((โโ((๐ดโ2)
โ 1)) ยท (2nd โ๐))) |
4 | 3 | oveq2d 7377 |
. . . . . . 7
โข (๐ = ๐ด โ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท
(2nd โ๐)))
= ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐)))) |
5 | 4 | mpteq2dv 5211 |
. . . . . 6
โข (๐ = ๐ด โ (๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) = (๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))) |
6 | 5 | cnveqd 5835 |
. . . . 5
โข (๐ = ๐ด โ โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) = โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))) |
7 | 6 | adantr 482 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) = โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))) |
8 | | id 22 |
. . . . . 6
โข (๐ = ๐ด โ ๐ = ๐ด) |
9 | 8, 2 | oveq12d 7379 |
. . . . 5
โข (๐ = ๐ด โ (๐ + (โโ((๐โ2) โ 1))) = (๐ด + (โโ((๐ดโ2) โ 1)))) |
10 | | id 22 |
. . . . 5
โข (๐ = ๐ โ ๐ = ๐) |
11 | 9, 10 | oveqan12d 7380 |
. . . 4
โข ((๐ = ๐ด โง ๐ = ๐) โ ((๐ + (โโ((๐โ2) โ 1)))โ๐) = ((๐ด + (โโ((๐ดโ2) โ 1)))โ๐)) |
12 | 7, 11 | fveq12d 6853 |
. . 3
โข ((๐ = ๐ด โง ๐ = ๐) โ (โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)) = (โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ((๐ด + (โโ((๐ดโ2) โ 1)))โ๐))) |
13 | 12 | fveq2d 6850 |
. 2
โข ((๐ = ๐ด โง ๐ = ๐) โ (1st โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐))) = (1st
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ((๐ด + (โโ((๐ดโ2) โ 1)))โ๐)))) |
14 | | df-rmx 41272 |
. 2
โข
Xrm = (๐ โ
(โคโฅโ2), ๐ โ โค โฆ (1st
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)))) |
15 | | fvex 6859 |
. 2
โข
(1st โ(โก(๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ((๐ด + (โโ((๐ดโ2) โ 1)))โ๐))) โ V |
16 | 13, 14, 15 | ovmpoa 7514 |
1
โข ((๐ด โ
(โคโฅโ2) โง ๐ โ โค) โ (๐ด Xrm ๐) = (1st โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐ดโ2) โ 1)) ยท
(2nd โ๐))))โ((๐ด + (โโ((๐ดโ2) โ 1)))โ๐)))) |