Metamath Proof Explorer

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 ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y → adj h ⁡ T = S

Proof

Step Hyp Ref Expression
1 funadj ⊢ Fun ⁡ adj h
2 df-adjh ⊢ adj h = z w | z : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y
3 2 eleq2i ⊢ T S ∈ adj h ↔ T S ∈ z w | z : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y
4 ax-hilex ⊢ ℋ ∈ V
5 fex ⊢ T : ℋ ⟶ ℋ ∧ ℋ ∈ V → T ∈ V
6 4 5 mpan2 ⊢ T : ℋ ⟶ ℋ → T ∈ V
7 fex ⊢ S : ℋ ⟶ ℋ ∧ ℋ ∈ V → S ∈ V
8 4 7 mpan2 ⊢ S : ℋ ⟶ ℋ → S ∈ V
9 feq1 ⊢ z = T → z : ℋ ⟶ ℋ ↔ T : ℋ ⟶ ℋ
10 fveq1 ⊢ z = T → z ⁡ x = T ⁡ x
11 10 oveq1d ⊢ z = T → z ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y
12 11 eqeq1d ⊢ z = T → z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y
13 12 2ralbidv ⊢ z = T → ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y
14 9 13 3anbi13d ⊢ z = T → z : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y
15 feq1 ⊢ w = S → w : ℋ ⟶ ℋ ↔ S : ℋ ⟶ ℋ
16 fveq1 ⊢ w = S → w ⁡ y = S ⁡ y
17 16 oveq2d ⊢ w = S → x ⋅ ih w ⁡ y = x ⋅ ih S ⁡ y
18 17 eqeq2d ⊢ w = S → T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
19 18 2ralbidv ⊢ w = S → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
20 15 19 3anbi23d ⊢ w = S → T : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
21 14 20 opelopabg ⊢ T ∈ V ∧ S ∈ V → T S ∈ z w | z : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
22 6 8 21 syl2an ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ → T S ∈ z w | z : ℋ ⟶ ℋ ∧ w : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ z ⁡ x ⋅ ih y = x ⋅ ih w ⁡ y ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
23 3 22 syl5bb ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ → T S ∈ adj h ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
24 df-3an ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
25 24 baibr ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y ↔ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
26 23 25 bitr4d ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ → T S ∈ adj h ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y
27 26 biimp3ar ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y → T S ∈ adj h
28 funopfv ⊢ Fun ⁡ adj h → T S ∈ adj h → adj h ⁡ T = S
29 1 27 28 mpsyl ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih S ⁡ y → adj h ⁡ T = S