Theorem adj1

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adj1	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		funadj	⊢ Fun adjℎ
2		funfvop	⊢ ( ( Fun adjℎ ∧ 𝑇 ∈ dom adjℎ ) → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ adjℎ )
3	1 2	mpan	⊢ ( 𝑇 ∈ dom adjℎ → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ adjℎ )
4		dfadj2	⊢ adjℎ = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) }
5	3 4	eleqtrdi	⊢ ( 𝑇 ∈ dom adjℎ → ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } )
6		fvex	⊢ ( adjℎ ‘ 𝑇 ) ∈ V
7		feq1	⊢ ( 𝑧 = 𝑇 → ( 𝑧 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ ℋ ) )
8		fveq1	⊢ ( 𝑧 = 𝑇 → ( 𝑧 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
9	8	oveq2d	⊢ ( 𝑧 = 𝑇 → ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) )
10	9	eqeq1d	⊢ ( 𝑧 = 𝑇 → ( ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) )
11	10	2ralbidv	⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) )
12	7 11	3anbi13d	⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
13		feq1	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( 𝑤 : ℋ ⟶ ℋ ↔ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) )
14		fveq1	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( 𝑤 ‘ 𝑥 ) = ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) )
15	14	oveq1d	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
16	15	eqeq2d	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
17	16	2ralbidv	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
18	13 17	3anbi23d	⊢ ( 𝑤 = ( adjℎ ‘ 𝑇 ) → ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
19	12 18	opelopabg	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) ∈ V ) → ( ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
20	6 19	mpan2	⊢ ( 𝑇 ∈ dom adjℎ → ( ⟨ 𝑇 , ( adjℎ ‘ 𝑇 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑧 ‘ 𝑦 ) ) = ( ( 𝑤 ‘ 𝑥 ) ·ih 𝑦 ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
21	5 20	mpbid	⊢ ( 𝑇 ∈ dom adjℎ → ( 𝑇 : ℋ ⟶ ℋ ∧ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
22	21	simp3d	⊢ ( 𝑇 ∈ dom adjℎ → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
23		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) )
24		fveq2	⊢ ( 𝑥 = 𝐴 → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) )
25	24	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) )
26	23 25	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) ) )
27		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ 𝐵 ) )
28	27	oveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) )
29		oveq2	⊢ ( 𝑦 = 𝐵 → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) )
30	28 29	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝑦 ) ↔ ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
31	26 30	rspc2v	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
32	22 31	syl5com	⊢ ( 𝑇 ∈ dom adjℎ → ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) ) )
33	32	3impib	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐵 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ·ih 𝐵 ) )