lnfnaddi - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > lnfnaddi		Structured version Visualization version GIF version

Theorem lnfnaddi 32099

Description: Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
lnfnl.1	⊢ 𝑇 ∈ LinFn

**Assertion**
Ref	Expression
lnfnaddi	⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +_ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))

**Proof of Theorem lnfnaddi**
Step	Hyp	Ref	Expression
1		ax-1cn 11086	. . 3 ⊢ 1 ∈ ℂ
2		lnfnl.1	. . . 4 ⊢ 𝑇 ∈ LinFn
3	2	lnfnli 32096	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((1 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((1 · (𝑇‘𝐴)) + (𝑇‘𝐵)))
4	1, 3	mp3an1 1451	. 2 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((1 ·_ℎ 𝐴) +_ℎ 𝐵)) = ((1 · (𝑇‘𝐴)) + (𝑇‘𝐵)))
5		ax-hvmulid 31062	. . . 4 ⊢ (𝐴 ∈ ℋ → (1 ·_ℎ 𝐴) = 𝐴)
6	5	fvoveq1d 7380	. . 3 ⊢ (𝐴 ∈ ℋ → (𝑇‘((1 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝑇‘(𝐴 +_ℎ 𝐵)))
7	6	adantr 480	. 2 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘((1 ·_ℎ 𝐴) +_ℎ 𝐵)) = (𝑇‘(𝐴 +_ℎ 𝐵)))
8	2	lnfnfi 32097	. . . . . 6 ⊢ 𝑇: ℋ⟶ℂ
9	8	ffvelcdmi 7028	. . . . 5 ⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℂ)
10	9	mullidd 11152	. . . 4 ⊢ (𝐴 ∈ ℋ → (1 · (𝑇‘𝐴)) = (𝑇‘𝐴))
11	10	adantr 480	. . 3 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (1 · (𝑇‘𝐴)) = (𝑇‘𝐴))
12	11	oveq1d 7373	. 2 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((1 · (𝑇‘𝐴)) + (𝑇‘𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))
13	4, 7, 12	3eqtr3d 2778	1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +_ℎ 𝐵)) = ((𝑇‘𝐴) + (𝑇‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ‘cfv 6491 (class class class)co 7358 ℂcc 11026 1c1 11029 + caddc 11031 · cmul 11033 ℋchba 30975 +_ℎ cva 30976 ·_ℎ csm 30977 LinFnclf 31010

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-mulcl 11090 ax-mulcom 11092 ax-mulass 11094 ax-distr 11095 ax-1rid 11098 ax-cnre 11101 ax-hilex 31055 ax-hvmulid 31062

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-rab 3399 df-v 3441 df-sbc 3740 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-fv 6499 df-ov 7361 df-oprab 7362 df-mpo 7363 df-map 8767 df-lnfn 31904

This theorem is referenced by: lnfnaddmuli 32101 nlelshi 32116

W3C validator