adjval - Hilbert Space Explorer

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

Theorem adjval 31648

Description: Value of the adjoint function for 𝑇 in the domain of adj_ℎ. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 24-Dec-2016.) (New usage is discouraged.)

**Assertion**
Ref	Expression
adjval	⊢ (𝑇 ∈ dom adj_ℎ → (adj_ℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑_m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))

Distinct variable group: 𝑥,𝑢,𝑦,𝑇

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

Step	Hyp	Ref	Expression
1		dmadjop 31646	. . . . 5 ⊢ (𝑇 ∈ dom adj_ℎ → 𝑇: ℋ⟶ ℋ)
2	1	biantrurd 532	. . . 4 ⊢ (𝑇 ∈ dom adj_ℎ → ((𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))))
3		ax-hilex 30757	. . . . . 6 ⊢ ℋ ∈ V
4	3, 3	elmap 8864	. . . . 5 ⊢ (𝑢 ∈ ( ℋ ↑_m ℋ) ↔ 𝑢: ℋ⟶ ℋ)
5	4	anbi1i 623	. . . 4 ⊢ ((𝑢 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) ↔ (𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))
6		3anass 1092	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
7	2, 5, 6	3bitr4g 314	. . 3 ⊢ (𝑇 ∈ dom adj_ℎ → ((𝑢 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
8	7	iotabidv 6520	. 2 ⊢ (𝑇 ∈ dom adj_ℎ → (℩𝑢(𝑢 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))) = (℩𝑢(𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
9		df-riota 7360	. . 3 ⊢ (℩𝑢 ∈ ( ℋ ↑_m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) = (℩𝑢(𝑢 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))
10	9	a1i 11	. 2 ⊢ (𝑇 ∈ dom adj_ℎ → (℩𝑢 ∈ ( ℋ ↑_m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) = (℩𝑢(𝑢 ∈ ( ℋ ↑_m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
11		dfadj2 31643	. . 3 ⊢ adj_ℎ = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))}
12		feq1 6691	. . . 4 ⊢ (𝑡 = 𝑇 → (𝑡: ℋ⟶ ℋ ↔ 𝑇: ℋ⟶ ℋ))
13		fveq1 6883	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (𝑡‘𝑦) = (𝑇‘𝑦))
14	13	oveq2d 7420	. . . . . 6 ⊢ (𝑡 = 𝑇 → (𝑥 ·_ih (𝑡‘𝑦)) = (𝑥 ·_ih (𝑇‘𝑦)))
15	14	eqeq1d 2728	. . . . 5 ⊢ (𝑡 = 𝑇 → ((𝑥 ·_ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦) ↔ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))
16	15	2ralbidv 3212	. . . 4 ⊢ (𝑡 = 𝑇 → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))
17	12, 16	3anbi13d 1434	. . 3 ⊢ (𝑡 = 𝑇 → ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
18	11, 17	fvopab5 7023	. 2 ⊢ (𝑇 ∈ dom adj_ℎ → (adj_ℎ‘𝑇) = (℩𝑢(𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦))))
19	8, 10, 18	3eqtr4rd 2777	1 ⊢ (𝑇 ∈ dom adj_ℎ → (adj_ℎ‘𝑇) = (℩𝑢 ∈ ( ℋ ↑_m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·_ih 𝑦)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3055 dom cdm 5669 ℩cio 6486 ⟶wf 6532 ‘cfv 6536 ℩crio 7359 (class class class)co 7404 ↑_m cmap 8819 ℋchba 30677 ·_ih csp 30680 adj_ℎcado 30713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-hilex 30757 ax-hfi 30837 ax-his1 30840

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-po 5581 df-so 5582 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-er 8702 df-map 8821 df-en 8939 df-dom 8940 df-sdom 8941 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11447 df-neg 11448 df-div 11873 df-2 12276 df-cj 15050 df-re 15051 df-im 15052 df-adjh 31607

This theorem is referenced by: adjval2 31649 adjbdln 31841

W3C validator