Theorem adjeq

Description: A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjeq	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ( adjℎ ‘ 𝑇 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		funadj	⊢ Fun adjℎ
2		df-adjh	⊢ adjℎ = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) }
3	2	eleq2i	⊢ ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } )
4		ax-hilex	⊢ ℋ ∈ V
5		fex	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ℋ ∈ V ) → 𝑇 ∈ V )
6	4 5	mpan2	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 ∈ V )
7		fex	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ℋ ∈ V ) → 𝑆 ∈ V )
8	4 7	mpan2	⊢ ( 𝑆 : ℋ ⟶ ℋ → 𝑆 ∈ V )
9		feq1	⊢ ( 𝑧 = 𝑇 → ( 𝑧 : ℋ ⟶ ℋ ↔ 𝑇 : ℋ ⟶ ℋ ) )
10		fveq1	⊢ ( 𝑧 = 𝑇 → ( 𝑧 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
11	10	oveq1d	⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
12	11	eqeq1d	⊢ ( 𝑧 = 𝑇 → ( ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) )
13	12	2ralbidv	⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) )
14	9 13	3anbi13d	⊢ ( 𝑧 = 𝑇 → ( ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ) )
15		feq1	⊢ ( 𝑤 = 𝑆 → ( 𝑤 : ℋ ⟶ ℋ ↔ 𝑆 : ℋ ⟶ ℋ ) )
16		fveq1	⊢ ( 𝑤 = 𝑆 → ( 𝑤 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
17	16	oveq2d	⊢ ( 𝑤 = 𝑆 → ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) )
18	17	eqeq2d	⊢ ( 𝑤 = 𝑆 → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
19	18	2ralbidv	⊢ ( 𝑤 = 𝑆 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
20	15 19	3anbi23d	⊢ ( 𝑤 = 𝑆 → ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
21	14 20	opelopabg	⊢ ( ( 𝑇 ∈ V ∧ 𝑆 ∈ V ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
22	6 8 21	syl2an	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 : ℋ ⟶ ℋ ∧ 𝑤 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑧 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑤 ‘ 𝑦 ) ) ) } ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
23	3 22	syl5bb	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
24		df-3an	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ↔ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
25	24	baibr	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) ) )
26	23 25	bitr4d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) )
27	26	biimp3ar	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ )
28		funopfv	⊢ ( Fun adjℎ → ( ⟨ 𝑇 , 𝑆 ⟩ ∈ adjℎ → ( adjℎ ‘ 𝑇 ) = 𝑆 ) )
29	1 27 28	mpsyl	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑆 ‘ 𝑦 ) ) ) → ( adjℎ ‘ 𝑇 ) = 𝑆 )