Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ๐ด) = (๐โif(๐ด โ โ, ๐ด, 0โ))) |
2 | | oveq2 7366 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ถ
ยทโ ๐ด) = (๐ถ ยทโ if(๐ด โ โ, ๐ด,
0โ))) |
3 | 1, 2 | eqeq12d 2749 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ๐ด) = (๐ถ ยทโ ๐ด) โ (๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)))) |
4 | 3 | anbi1d 631 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)))) |
5 | 4 | anbi1d 631 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)))) |
6 | | oveq1 7365 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด
ยทih (๐โ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต))) |
7 | 1 | oveq1d 7373 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ๐ด) ยทih ๐ต) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต)) |
8 | 6, 7 | eqeq12d 2749 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด
ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต))) |
9 | | oveq1 7365 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด
ยทih ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต)) |
10 | 9 | eqeq1d 2735 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด
ยทih ๐ต) = 0 โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0)) |
11 | 8, 10 | bibi12d 346 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐ด
ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0))) |
12 | 5, 11 | imbi12d 345 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0)) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0)))) |
13 | | fveq2 6843 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐โ๐ต) = (๐โif(๐ต โ โ, ๐ต, 0โ))) |
14 | | oveq2 7366 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐ท
ยทโ ๐ต) = (๐ท ยทโ if(๐ต โ โ, ๐ต,
0โ))) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โ๐ต) = (๐ท ยทโ ๐ต) โ (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ)))) |
16 | 15 | anbi2d 630 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))))) |
17 | 16 | anbi1d 631 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง ๐ถ โ (โโ๐ท)))) |
18 | 13 | oveq2d 7374 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ)))) |
19 | | oveq2 7366 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ))) |
20 | 18, 19 | eqeq12d 2749 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)))) |
21 | | oveq2 7366 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) |
22 | 21 | eqeq1d 2735 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0 โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0)) |
23 | 20, 22 | bibi12d 346 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0))) |
24 | 17, 23 | imbi12d 345 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โ๐ต)) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = 0)) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง ๐ถ โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0)))) |
25 | | oveq1 7365 |
. . . . . . 7
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ (๐ถ ยทโ if(๐ด โ โ, ๐ด, 0โ)) =
(if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ))) |
26 | 25 | eqeq2d 2744 |
. . . . . 6
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โ (๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)))) |
27 | 26 | anbi1d 631 |
. . . . 5
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))))) |
28 | | neeq1 3003 |
. . . . 5
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ (๐ถ โ (โโ๐ท) โ if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท))) |
29 | 27, 28 | anbi12d 632 |
. . . 4
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง ๐ถ โ (โโ๐ท)) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท)))) |
30 | 29 | imbi1d 342 |
. . 3
โข (๐ถ = if(๐ถ โ โ, ๐ถ, 0) โ (((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (๐ถ
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง ๐ถ โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) = 0)) โ
((((๐โif(๐ด โ โ, ๐ด, 0โ)) =
(if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0)))) |
31 | | oveq1 7365 |
. . . . . . 7
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ (๐ท ยทโ if(๐ต โ โ, ๐ต, 0โ)) =
(if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ))) |
32 | 31 | eqeq2d 2744 |
. . . . . 6
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ ((๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ)) โ (๐โif(๐ต โ โ, ๐ต, 0โ)) = (if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ)))) |
33 | 32 | anbi2d 630 |
. . . . 5
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โ ((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ))))) |
34 | | fveq2 6843 |
. . . . . 6
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ (โโ๐ท) = (โโif(๐ท โ โ, ๐ท, 0))) |
35 | 34 | neeq2d 3001 |
. . . . 5
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ (if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท) โ if(๐ถ โ โ, ๐ถ, 0) โ (โโif(๐ท โ โ, ๐ท, 0)))) |
36 | 33, 35 | anbi12d 632 |
. . . 4
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท)) โ (((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ
(โโif(๐ท โ
โ, ๐ท,
0))))) |
37 | 36 | imbi1d 342 |
. . 3
โข (๐ท = if(๐ท โ โ, ๐ท, 0) โ (((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (๐ท
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ (โโ๐ท)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) = 0)) โ
((((๐โif(๐ด โ โ, ๐ด, 0โ)) =
(if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ
(โโif(๐ท โ
โ, ๐ท, 0))) โ
((if(๐ด โ โ,
๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0)))) |
38 | | ifhvhv0 30006 |
. . . 4
โข if(๐ด โ โ, ๐ด, 0โ) โ
โ |
39 | | ifhvhv0 30006 |
. . . 4
โข if(๐ต โ โ, ๐ต, 0โ) โ
โ |
40 | | 0cn 11152 |
. . . . 5
โข 0 โ
โ |
41 | 40 | elimel 4556 |
. . . 4
โข if(๐ถ โ โ, ๐ถ, 0) โ
โ |
42 | 40 | elimel 4556 |
. . . 4
โข if(๐ท โ โ, ๐ท, 0) โ
โ |
43 | 38, 39, 41, 42 | eigorthi 30821 |
. . 3
โข ((((๐โif(๐ด โ โ, ๐ด, 0โ)) = (if(๐ถ โ โ, ๐ถ, 0)
ยทโ if(๐ด โ โ, ๐ด, 0โ)) โง (๐โif(๐ต โ โ, ๐ต, 0โ)) = (if(๐ท โ โ, ๐ท, 0)
ยทโ if(๐ต โ โ, ๐ต, 0โ))) โง if(๐ถ โ โ, ๐ถ, 0) โ
(โโif(๐ท โ
โ, ๐ท, 0))) โ
((if(๐ด โ โ,
๐ด, 0โ)
ยทih (๐โif(๐ต โ โ, ๐ต, 0โ))) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) =
0)) |
44 | 12, 24, 30, 37, 43 | dedth4h 4548 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
((((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท)) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0))) |
45 | 44 | imp 408 |
1
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (((๐โ๐ด) = (๐ถ ยทโ ๐ด) โง (๐โ๐ต) = (๐ท ยทโ ๐ต)) โง ๐ถ โ (โโ๐ท))) โ ((๐ด ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) โ (๐ด ยทih ๐ต) = 0)) |