Metamath Proof Explorer

Theorem lnopeq

Description: Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopeq ⊢ T ∈ LinOp ∧ U ∈ LinOp → ∀ x ∈ ℋ T ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ T = U

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ LinOp T 0 hop → T ⁡ x = if T ∈ LinOp T 0 hop ⁡ x
2 1 oveq1d ⊢ T = if T ∈ LinOp T 0 hop → T ⁡ x ⋅ ih x = if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x
3 2 eqeq1d ⊢ T = if T ∈ LinOp T 0 hop → T ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x
4 3 ralbidv ⊢ T = if T ∈ LinOp T 0 hop → ∀ x ∈ ℋ T ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x
5 eqeq1 ⊢ T = if T ∈ LinOp T 0 hop → T = U ↔ if T ∈ LinOp T 0 hop = U
6 4 5 bibi12d ⊢ T = if T ∈ LinOp T 0 hop → ∀ x ∈ ℋ T ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ T = U ↔ ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop = U
7 fveq1 ⊢ U = if U ∈ LinOp U 0 hop → U ⁡ x = if U ∈ LinOp U 0 hop ⁡ x
8 7 oveq1d ⊢ U = if U ∈ LinOp U 0 hop → U ⁡ x ⋅ ih x = if U ∈ LinOp U 0 hop ⁡ x ⋅ ih x
9 8 eqeq2d ⊢ U = if U ∈ LinOp U 0 hop → if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = if U ∈ LinOp U 0 hop ⁡ x ⋅ ih x
10 9 ralbidv ⊢ U = if U ∈ LinOp U 0 hop → ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = if U ∈ LinOp U 0 hop ⁡ x ⋅ ih x
11 eqeq2 ⊢ U = if U ∈ LinOp U 0 hop → if T ∈ LinOp T 0 hop = U ↔ if T ∈ LinOp T 0 hop = if U ∈ LinOp U 0 hop
12 10 11 bibi12d ⊢ U = if U ∈ LinOp U 0 hop → ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop = U ↔ ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = if U ∈ LinOp U 0 hop ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop = if U ∈ LinOp U 0 hop
13 0lnop ⊢ 0 hop ∈ LinOp
14 13 elimel ⊢ if T ∈ LinOp T 0 hop ∈ LinOp
15 13 elimel ⊢ if U ∈ LinOp U 0 hop ∈ LinOp
16 14 15 lnopeqi ⊢ ∀ x ∈ ℋ if T ∈ LinOp T 0 hop ⁡ x ⋅ ih x = if U ∈ LinOp U 0 hop ⁡ x ⋅ ih x ↔ if T ∈ LinOp T 0 hop = if U ∈ LinOp U 0 hop
17 6 12 16 dedth2h ⊢ T ∈ LinOp ∧ U ∈ LinOp → ∀ x ∈ ℋ T ⁡ x ⋅ ih x = U ⁡ x ⋅ ih x ↔ T = U