Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
โข ( ๐ = 0 โ ( 1 โ ๐ ) = ( 1 โ 0 ) ) |
2 |
|
1m0e1 |
โข ( 1 โ 0 ) = 1 |
3 |
1 2
|
eqtrdi |
โข ( ๐ = 0 โ ( 1 โ ๐ ) = 1 ) |
4 |
3
|
oveq1d |
โข ( ๐ = 0 โ ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) = ( 1 ยท ( ๐ด โ ๐ ) ) ) |
5 |
|
oveq1 |
โข ( ๐ = 0 โ ( ๐ ยท ( ๐ถ โ ๐ ) ) = ( 0 ยท ( ๐ถ โ ๐ ) ) ) |
6 |
4 5
|
oveq12d |
โข ( ๐ = 0 โ ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) |
7 |
6
|
eqeq2d |
โข ( ๐ = 0 โ ( ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) โ ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) ) |
8 |
7
|
ralbidv |
โข ( ๐ = 0 โ ( โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) โ โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) ) |
9 |
8
|
biimpac |
โข ( ( โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) โง ๐ = 0 ) โ โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) |
10 |
|
eqeefv |
โข ( ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) ) โ ( ๐ด = ๐ต โ โ ๐ โ ( 1 ... ๐ ) ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) ) ) |
11 |
10
|
3adant1 |
โข ( ( ๐ โ โ โง ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) ) โ ( ๐ด = ๐ต โ โ ๐ โ ( 1 ... ๐ ) ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) ) ) |
12 |
11
|
3adant3r3 |
โข ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โ ( ๐ด = ๐ต โ โ ๐ โ ( 1 ... ๐ ) ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) ) ) |
13 |
|
simplr1 |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ๐ด โ ( ๐ผ โ ๐ ) ) |
14 |
|
fveecn |
โข ( ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ๐ด โ ๐ ) โ โ ) |
15 |
13 14
|
sylancom |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ๐ด โ ๐ ) โ โ ) |
16 |
|
simplr3 |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ๐ถ โ ( ๐ผ โ ๐ ) ) |
17 |
|
fveecn |
โข ( ( ๐ถ โ ( ๐ผ โ ๐ ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ๐ถ โ ๐ ) โ โ ) |
18 |
16 17
|
sylancom |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ๐ถ โ ๐ ) โ โ ) |
19 |
|
mullid |
โข ( ( ๐ด โ ๐ ) โ โ โ ( 1 ยท ( ๐ด โ ๐ ) ) = ( ๐ด โ ๐ ) ) |
20 |
|
mul02 |
โข ( ( ๐ถ โ ๐ ) โ โ โ ( 0 ยท ( ๐ถ โ ๐ ) ) = 0 ) |
21 |
19 20
|
oveqan12d |
โข ( ( ( ๐ด โ ๐ ) โ โ โง ( ๐ถ โ ๐ ) โ โ ) โ ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) = ( ( ๐ด โ ๐ ) + 0 ) ) |
22 |
|
addrid |
โข ( ( ๐ด โ ๐ ) โ โ โ ( ( ๐ด โ ๐ ) + 0 ) = ( ๐ด โ ๐ ) ) |
23 |
22
|
adantr |
โข ( ( ( ๐ด โ ๐ ) โ โ โง ( ๐ถ โ ๐ ) โ โ ) โ ( ( ๐ด โ ๐ ) + 0 ) = ( ๐ด โ ๐ ) ) |
24 |
21 23
|
eqtrd |
โข ( ( ( ๐ด โ ๐ ) โ โ โง ( ๐ถ โ ๐ ) โ โ ) โ ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) = ( ๐ด โ ๐ ) ) |
25 |
15 18 24
|
syl2anc |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) = ( ๐ด โ ๐ ) ) |
26 |
25
|
eqeq1d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) = ( ๐ต โ ๐ ) โ ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) ) ) |
27 |
|
eqcom |
โข ( ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) = ( ๐ต โ ๐ ) โ ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) |
28 |
26 27
|
bitr3di |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง ๐ โ ( 1 ... ๐ ) ) โ ( ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) โ ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) ) |
29 |
28
|
ralbidva |
โข ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โ ( โ ๐ โ ( 1 ... ๐ ) ( ๐ด โ ๐ ) = ( ๐ต โ ๐ ) โ โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) ) |
30 |
12 29
|
bitrd |
โข ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โ ( ๐ด = ๐ต โ โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( 1 ยท ( ๐ด โ ๐ ) ) + ( 0 ยท ( ๐ถ โ ๐ ) ) ) ) ) |
31 |
9 30
|
imbitrrid |
โข ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โ ( ( โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) โง ๐ = 0 ) โ ๐ด = ๐ต ) ) |
32 |
31
|
expdimp |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) ) โ ( ๐ = 0 โ ๐ด = ๐ต ) ) |
33 |
32
|
necon3d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) ) โ ( ๐ด โ ๐ต โ ๐ โ 0 ) ) |
34 |
33
|
3impia |
โข ( ( ( ๐ โ โ โง ( ๐ด โ ( ๐ผ โ ๐ ) โง ๐ต โ ( ๐ผ โ ๐ ) โง ๐ถ โ ( ๐ผ โ ๐ ) ) ) โง โ ๐ โ ( 1 ... ๐ ) ( ๐ต โ ๐ ) = ( ( ( 1 โ ๐ ) ยท ( ๐ด โ ๐ ) ) + ( ๐ ยท ( ๐ถ โ ๐ ) ) ) โง ๐ด โ ๐ต ) โ ๐ โ 0 ) |