Metamath Proof Explorer

Theorem brafval

Description: The bra of a vector, expressed as <. A | in Dirac notation. See df-bra . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion brafval ⊢ A ∈ ℋ → bra ⁡ A = x ∈ ℋ ⟼ x ⋅ ih A

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ y = A → x ⋅ ih y = x ⋅ ih A
2 1 mpteq2dv ⊢ y = A → x ∈ ℋ ⟼ x ⋅ ih y = x ∈ ℋ ⟼ x ⋅ ih A
3 df-bra ⊢ bra = y ∈ ℋ ⟼ x ∈ ℋ ⟼ x ⋅ ih y
4 ax-hilex ⊢ ℋ ∈ V
5 4 mptex ⊢ x ∈ ℋ ⟼ x ⋅ ih A ∈ V
6 2 3 5 fvmpt ⊢ A ∈ ℋ → bra ⁡ A = x ∈ ℋ ⟼ x ⋅ ih A