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 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) + ( 𝑇 ‘ 𝐵 ) ) ) |