Step |
Hyp |
Ref |
Expression |
1 |
|
lnfnl.1 |
โข ๐ โ LinFn |
2 |
|
ax-1cn |
โข 1 โ โ |
3 |
1
|
lnfnli |
โข ( ( 1 โ โ โง ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ( 1 ยท ( ๐ โ ๐ด ) ) + ( ๐ โ ๐ต ) ) ) |
4 |
2 3
|
mp3an1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ( 1 ยท ( ๐ โ ๐ด ) ) + ( ๐ โ ๐ต ) ) ) |
5 |
|
ax-hvmulid |
โข ( ๐ด โ โ โ ( 1 ยทโ ๐ด ) = ๐ด ) |
6 |
5
|
fvoveq1d |
โข ( ๐ด โ โ โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ๐ โ ( ๐ด +โ ๐ต ) ) ) |
7 |
6
|
adantr |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ( 1 ยทโ ๐ด ) +โ ๐ต ) ) = ( ๐ โ ( ๐ด +โ ๐ต ) ) ) |
8 |
1
|
lnfnfi |
โข ๐ : โ โถ โ |
9 |
8
|
ffvelrni |
โข ( ๐ด โ โ โ ( ๐ โ ๐ด ) โ โ ) |
10 |
9
|
mulid2d |
โข ( ๐ด โ โ โ ( 1 ยท ( ๐ โ ๐ด ) ) = ( ๐ โ ๐ด ) ) |
11 |
10
|
adantr |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 1 ยท ( ๐ โ ๐ด ) ) = ( ๐ โ ๐ด ) ) |
12 |
11
|
oveq1d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( 1 ยท ( ๐ โ ๐ด ) ) + ( ๐ โ ๐ต ) ) = ( ( ๐ โ ๐ด ) + ( ๐ โ ๐ต ) ) ) |
13 |
4 7 12
|
3eqtr3d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด +โ ๐ต ) ) = ( ( ๐ โ ๐ด ) + ( ๐ โ ๐ต ) ) ) |