Metamath Proof Explorer

Theorem cnvbramul

Description: Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnvbramul	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to {bra}^{-1} (A \cdot_{fn} T) = \overline{A} \cdot_{ℎ} {bra}^{-1} (T)$

Proof

Step	Hyp	Ref	Expression
1		cnvbracl	$⊢ T \in (LinFn \cap ContFn) \to {bra}^{-1} (T) \in ℋ$
2		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
3		brafnmul	$⊢ (\overline{A} \in ℂ \land {bra}^{-1} (T) \in ℋ) \to bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T)) = \overline{\overline{A}} \cdot_{fn} bra ({bra}^{-1} (T))$
4	2 3	sylan	$⊢ (A \in ℂ \land {bra}^{-1} (T) \in ℋ) \to bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T)) = \overline{\overline{A}} \cdot_{fn} bra ({bra}^{-1} (T))$
5		cjcj	$⊢ A \in ℂ \to \overline{\overline{A}} = A$
6	5	adantr	$⊢ (A \in ℂ \land {bra}^{-1} (T) \in ℋ) \to \overline{\overline{A}} = A$
7	6	oveq1d	$⊢ (A \in ℂ \land {bra}^{-1} (T) \in ℋ) \to \overline{\overline{A}} \cdot_{fn} bra ({bra}^{-1} (T)) = A \cdot_{fn} bra ({bra}^{-1} (T))$
8	4 7	eqtrd	$⊢ (A \in ℂ \land {bra}^{-1} (T) \in ℋ) \to bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T)) = A \cdot_{fn} bra ({bra}^{-1} (T))$
9	1 8	sylan2	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T)) = A \cdot_{fn} bra ({bra}^{-1} (T))$
10		bracnvbra	$⊢ T \in (LinFn \cap ContFn) \to bra ({bra}^{-1} (T)) = T$
11	10	oveq2d	$⊢ T \in (LinFn \cap ContFn) \to A \cdot_{fn} bra ({bra}^{-1} (T)) = A \cdot_{fn} T$
12	11	adantl	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to A \cdot_{fn} bra ({bra}^{-1} (T)) = A \cdot_{fn} T$
13	9 12	eqtrd	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T)) = A \cdot_{fn} T$
14	13	fveq2d	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to {bra}^{-1} (bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T))) = {bra}^{-1} (A \cdot_{fn} T)$
15		hvmulcl	$⊢ (\overline{A} \in ℂ \land {bra}^{-1} (T) \in ℋ) \to \overline{A} \cdot_{ℎ} {bra}^{-1} (T) \in ℋ$
16	2 1 15	syl2an	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to \overline{A} \cdot_{ℎ} {bra}^{-1} (T) \in ℋ$
17		cnvbrabra	$⊢ \overline{A} \cdot_{ℎ} {bra}^{-1} (T) \in ℋ \to {bra}^{-1} (bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T))) = \overline{A} \cdot_{ℎ} {bra}^{-1} (T)$
18	16 17	syl	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to {bra}^{-1} (bra (\overline{A} \cdot_{ℎ} {bra}^{-1} (T))) = \overline{A} \cdot_{ℎ} {bra}^{-1} (T)$
19	14 18	eqtr3d	$⊢ (A \in ℂ \land T \in (LinFn \cap ContFn)) \to {bra}^{-1} (A \cdot_{fn} T) = \overline{A} \cdot_{ℎ} {bra}^{-1} (T)$