lnopmi - Hilbert Space Explorer

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

Theorem lnopmi 31253

Description: The scalar product of a linear operator is a linear operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.)

**Hypothesis**
Ref	Expression
lnopm.1	⊢ 𝑇 ∈ LinOp

**Assertion**
Ref	Expression
lnopmi	⊢ (𝐴 ∈ ℂ → (𝐴 ·_op 𝑇) ∈ LinOp)

Proof of Theorem lnopmi Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lnopm.1	. . . 4 ⊢ 𝑇 ∈ LinOp
2	1	lnopfi 31222	. . 3 ⊢ 𝑇: ℋ⟶ ℋ
3		homulcl 31012	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·_op 𝑇): ℋ⟶ ℋ)
4	2, 3	mpan2 690	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 ·_op 𝑇): ℋ⟶ ℋ)
5		hvmulcl 30266	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ℎ 𝑦) ∈ ℋ)
6		hvaddcl 30265	. . . . . . . 8 ⊢ (((𝑥 ·_ℎ 𝑦) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧) ∈ ℋ)
7	5, 6	sylan 581	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧) ∈ ℋ)
8		homval 30994	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ ((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧) ∈ ℋ) → ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))))
9	2, 8	mp3an2 1450	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧) ∈ ℋ) → ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))))
10	7, 9	sylan2 594	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))))
11		id 22	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
12	2	ffvelcdmi 7086	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℋ → (𝑇‘𝑦) ∈ ℋ)
13		hvmulcl 30266	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝑥 ·_ℎ (𝑇‘𝑦)) ∈ ℋ)
14	12, 13	sylan2 594	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ℎ (𝑇‘𝑦)) ∈ ℋ)
15	2	ffvelcdmi 7086	. . . . . . . . 9 ⊢ (𝑧 ∈ ℋ → (𝑇‘𝑧) ∈ ℋ)
16		ax-hvdistr1 30261	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ·_ℎ (𝑇‘𝑦)) ∈ ℋ ∧ (𝑇‘𝑧) ∈ ℋ) → (𝐴 ·_ℎ ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧))) = ((𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) +_ℎ (𝐴 ·_ℎ (𝑇‘𝑧))))
17	11, 14, 15, 16	syl3an 1161	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐴 ·_ℎ ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧))) = ((𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) +_ℎ (𝐴 ·_ℎ (𝑇‘𝑧))))
18	17	3expb 1121	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝐴 ·_ℎ ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧))) = ((𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) +_ℎ (𝐴 ·_ℎ (𝑇‘𝑧))))
19	1	lnopli 31221	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧)))
20	19	3expa 1119	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧)))
21	20	oveq2d 7425	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))) = (𝐴 ·_ℎ ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧))))
22	21	adantl 483	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))) = (𝐴 ·_ℎ ((𝑥 ·_ℎ (𝑇‘𝑦)) +_ℎ (𝑇‘𝑧))))
23		homval 30994	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝐴 ·_op 𝑇)‘𝑦) = (𝐴 ·_ℎ (𝑇‘𝑦)))
24	2, 23	mp3an2 1450	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝐴 ·_op 𝑇)‘𝑦) = (𝐴 ·_ℎ (𝑇‘𝑦)))
25	24	adantrl 715	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝐴 ·_op 𝑇)‘𝑦) = (𝐴 ·_ℎ (𝑇‘𝑦)))
26	25	oveq2d 7425	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) = (𝑥 ·_ℎ (𝐴 ·_ℎ (𝑇‘𝑦))))
27		hvmulcom 30296	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ (𝑇‘𝑦) ∈ ℋ) → (𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) = (𝑥 ·_ℎ (𝐴 ·_ℎ (𝑇‘𝑦))))
28	12, 27	syl3an3 1166	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) = (𝑥 ·_ℎ (𝐴 ·_ℎ (𝑇‘𝑦))))
29	28	3expb 1121	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) = (𝑥 ·_ℎ (𝐴 ·_ℎ (𝑇‘𝑦))))
30	26, 29	eqtr4d 2776	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) = (𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))))
31		homval 30994	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑧 ∈ ℋ) → ((𝐴 ·_op 𝑇)‘𝑧) = (𝐴 ·_ℎ (𝑇‘𝑧)))
32	2, 31	mp3an2 1450	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℋ) → ((𝐴 ·_op 𝑇)‘𝑧) = (𝐴 ·_ℎ (𝑇‘𝑧)))
33	30, 32	oveqan12d 7428	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ (𝐴 ∈ ℂ ∧ 𝑧 ∈ ℋ)) → ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)) = ((𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) +_ℎ (𝐴 ·_ℎ (𝑇‘𝑧))))
34	33	anandis 677	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)) = ((𝐴 ·_ℎ (𝑥 ·_ℎ (𝑇‘𝑦))) +_ℎ (𝐴 ·_ℎ (𝑇‘𝑧))))
35	18, 22, 34	3eqtr4rd 2784	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)) = (𝐴 ·_ℎ (𝑇‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧))))
36	10, 35	eqtr4d 2776	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ)) → ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)))
37	36	exp32 422	. . . 4 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑧 ∈ ℋ → ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)))))
38	37	ralrimdv 3153	. . 3 ⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ∀𝑧 ∈ ℋ ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧))))
39	38	ralrimivv 3199	. 2 ⊢ (𝐴 ∈ ℂ → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧)))
40		ellnop 31111	. 2 ⊢ ((𝐴 ·_op 𝑇) ∈ LinOp ↔ ((𝐴 ·_op 𝑇): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((𝐴 ·_op 𝑇)‘((𝑥 ·_ℎ 𝑦) +_ℎ 𝑧)) = ((𝑥 ·_ℎ ((𝐴 ·_op 𝑇)‘𝑦)) +_ℎ ((𝐴 ·_op 𝑇)‘𝑧))))
41	4, 39, 40	sylanbrc 584	1 ⊢ (𝐴 ∈ ℂ → (𝐴 ·_op 𝑇) ∈ LinOp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ℂcc 11108 ℋchba 30172 +_ℎ cva 30173 ·_ℎ csm 30174 ·_op chot 30192 LinOpclo 30200

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-mulcom 11174 ax-hilex 30252 ax-hfvadd 30253 ax-hfvmul 30258 ax-hvmulass 30260 ax-hvdistr1 30261

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-map 8822 df-homul 30984 df-lnop 31094

This theorem is referenced by: lnophdi 31255 bdophmi 31285

W3C validator