This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) ∈ LinFn )

Proof

Step Hyp Ref Expression
1 brafn ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ )
2 simpll ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → 𝐴 ∈ ℋ )
3 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
4 3 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
5 simprr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → 𝑧 ∈ ℋ )
6 braadd ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
7 2 4 5 6 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
8 bramul ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) )
9 8 3expa ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) )
10 9 adantrr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) )
11 10 oveq1d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( ( bra ‘ 𝐴 ) ‘ ( 𝑥 ·ℎ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) = ( ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
12 7 11 eqtrd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ) → ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
13 12 ralrimivva ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℂ ) → ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
14 13 ralrimiva ⊢ ( 𝐴 ∈ ℋ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) )
15 ellnfn ⊢ ( ( bra ‘ 𝐴 ) ∈ LinFn ↔ ( ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( bra ‘ 𝐴 ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( bra ‘ 𝐴 ) ‘ 𝑦 ) ) + ( ( bra ‘ 𝐴 ) ‘ 𝑧 ) ) ) )
16 1 14 15 sylanbrc ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) ∈ LinFn )