Metamath Proof Explorer

Theorem bralnfn

Description: The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion bralnfn ⊢ A ∈ ℋ → bra ⁡ A ∈ LinFn

Proof

Step Hyp Ref Expression
1 brafn ⊢ A ∈ ℋ → bra ⁡ A : ℋ ⟶ ℂ
2 simpll ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → A ∈ ℋ
3 hvmulcl ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ y ∈ ℋ
4 3 ad2ant2lr ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y ∈ ℋ
5 simprr ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → z ∈ ℋ
6 braadd ⊢ A ∈ ℋ ∧ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = bra ⁡ A ⁡ x ⋅ ℎ y + bra ⁡ A ⁡ z
7 2 4 5 6 syl3anc ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = bra ⁡ A ⁡ x ⋅ ℎ y + bra ⁡ A ⁡ z
8 bramul ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y = x ⁢ bra ⁡ A ⁡ y
9 8 3expa ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y = x ⁢ bra ⁡ A ⁡ y
10 9 adantrr ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y = x ⁢ bra ⁡ A ⁡ y
11 10 oveq1d ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y + bra ⁡ A ⁡ z = x ⁢ bra ⁡ A ⁡ y + bra ⁡ A ⁡ z
12 7 11 eqtrd ⊢ A ∈ ℋ ∧ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = x ⁢ bra ⁡ A ⁡ y + bra ⁡ A ⁡ z
13 12 ralrimivva ⊢ A ∈ ℋ ∧ x ∈ ℂ → ∀ y ∈ ℋ ∀ z ∈ ℋ bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = x ⁢ bra ⁡ A ⁡ y + bra ⁡ A ⁡ z
14 13 ralrimiva ⊢ A ∈ ℋ → ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = x ⁢ bra ⁡ A ⁡ y + bra ⁡ A ⁡ z
15 ellnfn ⊢ bra ⁡ A ∈ LinFn ↔ bra ⁡ A : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ bra ⁡ A ⁡ x ⋅ ℎ y + ℎ z = x ⁢ bra ⁡ A ⁡ y + bra ⁡ A ⁡ z
16 1 14 15 sylanbrc ⊢ A ∈ ℋ → bra ⁡ A ∈ LinFn