adj2

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

		Ref	Expression
	Assertion	adj2	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) = ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		adj1	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·_ih ( 𝑇 ‘ 𝐴 ) ) = ( ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ·_ih 𝐴 ) )
2		simp2	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → 𝐵 ∈ ℋ )
3		dmadjop	⊢ ( 𝑇 ∈ dom adj_ℎ → 𝑇 : ℋ ⟶ ℋ )
4	3	ffvelrnda	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
5	4	3adant2	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
6		ax-his1	⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ) → ( 𝐵 ·_ih ( 𝑇 ‘ 𝐴 ) ) = ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ) )
7	2 5 6	syl2anc	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·_ih ( 𝑇 ‘ 𝐴 ) ) = ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ) )
8		adjcl	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ) → ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ )
9	8	3adant3	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ )
10		simp3	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 ∈ ℋ )
11		ax-his1	⊢ ( ( ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ·_ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
12	9 10 11	syl2anc	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ·_ih 𝐴 ) = ( ∗ ‘ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
13	1 7 12	3eqtr3d	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
14		hicl	⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ∈ ℂ )
15	5 2 14	syl2anc	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ∈ ℂ )
16		hicl	⊢ ( ( 𝐴 ∈ ℋ ∧ ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ∈ ℋ ) → ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ )
17	10 9 16	syl2anc	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ )
18		cj11	⊢ ( ( ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ∈ ℂ ∧ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ∈ ℂ ) → ( ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) = ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
19	15 17 18	syl2anc	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ∗ ‘ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) ↔ ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) = ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
20	13 19	mpbid	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) = ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )
21	20	3com23	⊢ ( ( 𝑇 ∈ dom adj_ℎ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·_ih 𝐵 ) = ( 𝐴 ·_ih ( ( adj_ℎ ‘ 𝑇 ) ‘ 𝐵 ) ) )

Metamath Proof Explorer

Theorem adj2

Proof