Metamath Proof Explorer

Theorem kbass3

Description: Dirac bra-ket associative law <. A | B >. <. C | D >. = ( <. A | B >. <. C | ) | D >. . (Contributed by NM, 30-May-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	kbass3	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to bra (A) (B) bra (C) (D) = (bra (A) (B) \cdot_{fn} bra (C)) (D)$

Proof

Step	Hyp	Ref	Expression
1		bracl	$⊢ (A \in ℋ \land B \in ℋ) \to bra (A) (B) \in ℂ$
2	1	adantr	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to bra (A) (B) \in ℂ$
3		brafn	$⊢ C \in ℋ \to bra (C) : ℋ ⟶ ℂ$
4	3	ad2antrl	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to bra (C) : ℋ ⟶ ℂ$
5		simprr	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to D \in ℋ$
6		hfmval	$⊢ (bra (A) (B) \in ℂ \land bra (C) : ℋ ⟶ ℂ \land D \in ℋ) \to (bra (A) (B) \cdot_{fn} bra (C)) (D) = bra (A) (B) bra (C) (D)$
7	2 4 5 6	syl3anc	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to (bra (A) (B) \cdot_{fn} bra (C)) (D) = bra (A) (B) bra (C) (D)$
8	7	eqcomd	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to bra (A) (B) bra (C) (D) = (bra (A) (B) \cdot_{fn} bra (C)) (D)$