elhmop - Hilbert Space Explorer

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

Theorem elhmop 32484

Description: Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)

**Assertion**
Ref	Expression
elhmop	⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))

Distinct variable group: 𝑥,𝑦,𝑇

Proof of Theorem elhmop Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq1 6889	. . . . . 6 ⊢ (𝑡 = 𝑇 → (𝑡‘𝑦) = (𝑇‘𝑦))
2	1	oveq2d 7440	. . . . 5 ⊢ (𝑡 = 𝑇 → (𝑥 ·_ih (𝑡‘𝑦)) = (𝑥 ·_ih (𝑇‘𝑦)))
3		fveq1 6889	. . . . . 6 ⊢ (𝑡 = 𝑇 → (𝑡‘𝑥) = (𝑇‘𝑥))
4	3	oveq1d 7439	. . . . 5 ⊢ (𝑡 = 𝑇 → ((𝑡‘𝑥) ·_ih 𝑦) = ((𝑇‘𝑥) ·_ih 𝑦))
5	2, 4	eqeq12d 2776	. . . 4 ⊢ (𝑡 = 𝑇 → ((𝑥 ·_ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·_ih 𝑦) ↔ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
6	5	2ralbidv 3226	. . 3 ⊢ (𝑡 = 𝑇 → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
7		df-hmop 32455	. . 3 ⊢ HrmOp = {𝑡 ∈ ( ℋ ↑_m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·_ih 𝑦)}
8	6, 7	elrab2 3648	. 2 ⊢ (𝑇 ∈ HrmOp ↔ (𝑇 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
9		ax-hilex 31610	. . . 4 ⊢ ℋ ∈ V
10	9, 9	elmap 8907	. . 3 ⊢ (𝑇 ∈ ( ℋ ↑_m ℋ) ↔ 𝑇: ℋ⟶ ℋ)
11	10	anbi1i 636	. 2 ⊢ ((𝑇 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))
12	8, 11	bitri 278	1 ⊢ (𝑇 ∈ HrmOp ↔ (𝑇: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ⟶wf 6539 ‘cfv 6543 (class class class)co 7424 ↑_m cmap 8855 ℋchba 31530 ·_ih csp 31533 HrmOpcho 31561

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-hilex 31610

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-fv 6551 df-ov 7427 df-oprab 7428 df-mpo 7429 df-map 8857 df-hmop 32455

This theorem is used by: hmopf 32485 hmop 32533 hmopadj2 32552 idhmop 32593 0hmop 32594 lnophmi 32629 hmops 32631 hmopm 32632 hmopco 32634 pjhmopi 32757

W3C validator