Step |
Hyp |
Ref |
Expression |
1 |
|
lnopl.1 |
โข ๐ โ LinOp |
2 |
|
ax-1cn |
โข 1 โ โ |
3 |
1
|
lnopli |
โข ( ( 1 โ โ โง ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ( 1 ยทโ ( ๐ โ ๐ด ) ) +โ ( ๐ โ ๐ต ) ) ) |
4 |
2 3
|
mp3an1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ( 1 ยทโ ( ๐ โ ๐ด ) ) +โ ( ๐ โ ๐ต ) ) ) |
5 |
|
ax-hvmulid |
โข ( ๐ด โ โ โ ( 1 ยทโ ๐ด ) = ๐ด ) |
6 |
5
|
fvoveq1d |
โข ( ๐ด โ โ โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ๐ โ ( ๐ด +โ ๐ต ) ) ) |
7 |
6
|
adantr |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ๐ โ ( ๐ด +โ ๐ต ) ) ) |
8 |
1
|
lnopfi |
โข ๐ : โ โถ โ |
9 |
8
|
ffvelcdmi |
โข ( ๐ด โ โ โ ( ๐ โ ๐ด ) โ โ ) |
10 |
|
ax-hvmulid |
โข ( ( ๐ โ ๐ด ) โ โ โ ( 1 ยทโ ( ๐ โ ๐ด ) ) = ( ๐ โ ๐ด ) ) |
11 |
9 10
|
syl |
โข ( ๐ด โ โ โ ( 1 ยทโ ( ๐ โ ๐ด ) ) = ( ๐ โ ๐ด ) ) |
12 |
11
|
adantr |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 1 ยทโ ( ๐ โ ๐ด ) ) = ( ๐ โ ๐ด ) ) |
13 |
12
|
oveq1d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( 1 ยทโ ( ๐ โ ๐ด ) ) +โ ( ๐ โ ๐ต ) ) = ( ( ๐ โ ๐ด ) +โ ( ๐ โ ๐ต ) ) ) |
14 |
4 7 13
|
3eqtr3d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด +โ ๐ต ) ) = ( ( ๐ โ ๐ด ) +โ ( ๐ โ ๐ต ) ) ) |