Metamath Proof Explorer

Theorem unop

Description: Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unop ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih T ⁡ B = A ⋅ ih B

Proof

Step Hyp Ref Expression
1 elunop ⊢ T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y
2 1 simprbi ⊢ T ∈ UniOp → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y
3 2 3ad2ant1 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y
4 fveq2 ⊢ x = A → T ⁡ x = T ⁡ A
5 4 oveq1d ⊢ x = A → T ⁡ x ⋅ ih T ⁡ y = T ⁡ A ⋅ ih T ⁡ y
6 oveq1 ⊢ x = A → x ⋅ ih y = A ⋅ ih y
7 5 6 eqeq12d ⊢ x = A → T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y ↔ T ⁡ A ⋅ ih T ⁡ y = A ⋅ ih y
8 fveq2 ⊢ y = B → T ⁡ y = T ⁡ B
9 8 oveq2d ⊢ y = B → T ⁡ A ⋅ ih T ⁡ y = T ⁡ A ⋅ ih T ⁡ B
10 oveq2 ⊢ y = B → A ⋅ ih y = A ⋅ ih B
11 9 10 eqeq12d ⊢ y = B → T ⁡ A ⋅ ih T ⁡ y = A ⋅ ih y ↔ T ⁡ A ⋅ ih T ⁡ B = A ⋅ ih B
12 7 11 rspc2v ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y → T ⁡ A ⋅ ih T ⁡ B = A ⋅ ih B
13 12 3adant1 ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y → T ⁡ A ⋅ ih T ⁡ B = A ⋅ ih B
14 3 13 mpd ⊢ T ∈ UniOp ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A ⋅ ih T ⁡ B = A ⋅ ih B