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 )