Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hvmulid |
โข ( ๐ด โ โ โ ( 1 ยทโ ๐ด ) = ๐ด ) |
2 |
1
|
oveq1d |
โข ( ๐ด โ โ โ ( ( 1 ยทโ ๐ด ) +โ ( - 1 ยทโ ๐ด ) ) = ( ๐ด +โ ( - 1 ยทโ ๐ด ) ) ) |
3 |
|
ax-1cn |
โข 1 โ โ |
4 |
|
neg1cn |
โข - 1 โ โ |
5 |
|
ax-hvdistr2 |
โข ( ( 1 โ โ โง - 1 โ โ โง ๐ด โ โ ) โ ( ( 1 + - 1 ) ยทโ ๐ด ) = ( ( 1 ยทโ ๐ด ) +โ ( - 1 ยทโ ๐ด ) ) ) |
6 |
3 4 5
|
mp3an12 |
โข ( ๐ด โ โ โ ( ( 1 + - 1 ) ยทโ ๐ด ) = ( ( 1 ยทโ ๐ด ) +โ ( - 1 ยทโ ๐ด ) ) ) |
7 |
|
hvsubval |
โข ( ( ๐ด โ โ โง ๐ด โ โ ) โ ( ๐ด โโ ๐ด ) = ( ๐ด +โ ( - 1 ยทโ ๐ด ) ) ) |
8 |
7
|
anidms |
โข ( ๐ด โ โ โ ( ๐ด โโ ๐ด ) = ( ๐ด +โ ( - 1 ยทโ ๐ด ) ) ) |
9 |
2 6 8
|
3eqtr4rd |
โข ( ๐ด โ โ โ ( ๐ด โโ ๐ด ) = ( ( 1 + - 1 ) ยทโ ๐ด ) ) |
10 |
|
1pneg1e0 |
โข ( 1 + - 1 ) = 0 |
11 |
10
|
oveq1i |
โข ( ( 1 + - 1 ) ยทโ ๐ด ) = ( 0 ยทโ ๐ด ) |
12 |
9 11
|
eqtrdi |
โข ( ๐ด โ โ โ ( ๐ด โโ ๐ด ) = ( 0 ยทโ ๐ด ) ) |
13 |
|
ax-hvmul0 |
โข ( ๐ด โ โ โ ( 0 ยทโ ๐ด ) = 0โ ) |
14 |
12 13
|
eqtrd |
โข ( ๐ด โ โ โ ( ๐ด โโ ๐ด ) = 0โ ) |