Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ๐ด) = (๐โif(๐ด โ โ, ๐ด, 0โ))) |
2 | | oveq2 7366 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ต
ยทโ ๐ด) = (๐ต ยทโ if(๐ด โ โ, ๐ด,
0โ))) |
3 | 1, 2 | eqeq12d 2749 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ (๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)))) |
4 | | neeq1 3003 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด โ 0โ
โ if(๐ด โ โ,
๐ด, 0โ)
โ 0โ)) |
5 | 3, 4 | anbi12d 632 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ))) |
6 | | id 22 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ๐ด = if(๐ด โ โ, ๐ด, 0โ)) |
7 | 6, 1 | oveq12d 7376 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด
ยทih (๐โ๐ด)) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ)))) |
8 | 1, 6 | oveq12d 7376 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ๐ด) ยทih ๐ด) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ))) |
9 | 7, 8 | eqeq12d 2749 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)))) |
10 | 9 | bibi1d 344 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ ๐ต โ
โ))) |
11 | 5, 10 | imbi12d 345 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ ๐ต โ
โ)))) |
12 | | oveq1 7365 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ (๐ต ยทโ if(๐ด โ โ, ๐ด, 0โ)) =
(if(๐ต โ โ, ๐ต, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ))) |
13 | 12 | eqeq2d 2744 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โ (๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ต โ โ, ๐ต, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)))) |
14 | 13 | anbi1d 631 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ต โ โ, ๐ต, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ))) |
15 | | eleq1 2822 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ (๐ต โ โ โ if(๐ต โ โ, ๐ต, 0) โ โ)) |
16 | 15 | bibi2d 343 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ (((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ ๐ต โ โ) โ
((if(๐ด โ โ,
๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ if(๐ต โ โ, ๐ต, 0) โ
โ))) |
17 | 14, 16 | imbi12d 345 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ต
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ ๐ต โ โ)) โ
(((๐โif(๐ด โ โ, ๐ด, 0โ)) =
(if(๐ต โ โ, ๐ต, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ if(๐ต โ โ, ๐ต, 0) โ
โ)))) |
18 | | ifhvhv0 30006 |
. . . 4
โข if(๐ด โ โ, ๐ด, 0โ) โ
โ |
19 | | 0cn 11152 |
. . . . 5
โข 0 โ
โ |
20 | 19 | elimel 4556 |
. . . 4
โข if(๐ต โ โ, ๐ต, 0) โ
โ |
21 | 18, 20 | eigrei 30818 |
. . 3
โข (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ต โ โ, ๐ต, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง if(๐ด โ โ, ๐ด, 0โ) โ
0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ด โ โ, ๐ด, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ด โ โ, ๐ด, 0โ)) โ if(๐ต โ โ, ๐ต, 0) โ
โ)) |
22 | 11, 17, 21 | dedth2h 4546 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ))) |
23 | 22 | imp 408 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) |