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 ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra -1 ⁡ A · fn T = A ‾ ⋅ ℎ bra -1 ⁡ T

Proof

Step Hyp Ref Expression
1 cnvbracl ⊢ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T ∈ ℋ
2 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
3 brafnmul ⊢ A ‾ ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A ‾ ‾ · fn bra ⁡ bra -1 ⁡ T
4 2 3 sylan ⊢ A ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A ‾ ‾ · fn bra ⁡ bra -1 ⁡ T
5 cjcj ⊢ A ∈ ℂ → A ‾ ‾ = A
6 5 adantr ⊢ A ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → A ‾ ‾ = A
7 6 oveq1d ⊢ A ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → A ‾ ‾ · fn bra ⁡ bra -1 ⁡ T = A · fn bra ⁡ bra -1 ⁡ T
8 4 7 eqtrd ⊢ A ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A · fn bra ⁡ bra -1 ⁡ T
9 1 8 sylan2 ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A · fn bra ⁡ bra -1 ⁡ T
10 bracnvbra ⊢ T ∈ LinFn ∩ ContFn → bra ⁡ bra -1 ⁡ T = T
11 10 oveq2d ⊢ T ∈ LinFn ∩ ContFn → A · fn bra ⁡ bra -1 ⁡ T = A · fn T
12 11 adantl ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → A · fn bra ⁡ bra -1 ⁡ T = A · fn T
13 9 12 eqtrd ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A · fn T
14 13 fveq2d ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra -1 ⁡ bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = bra -1 ⁡ A · fn T
15 hvmulcl ⊢ A ‾ ∈ ℂ ∧ bra -1 ⁡ T ∈ ℋ → A ‾ ⋅ ℎ bra -1 ⁡ T ∈ ℋ
16 2 1 15 syl2an ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → A ‾ ⋅ ℎ bra -1 ⁡ T ∈ ℋ
17 cnvbrabra ⊢ A ‾ ⋅ ℎ bra -1 ⁡ T ∈ ℋ → bra -1 ⁡ bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A ‾ ⋅ ℎ bra -1 ⁡ T
18 16 17 syl ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra -1 ⁡ bra ⁡ A ‾ ⋅ ℎ bra -1 ⁡ T = A ‾ ⋅ ℎ bra -1 ⁡ T
19 14 18 eqtr3d ⊢ A ∈ ℂ ∧ T ∈ LinFn ∩ ContFn → bra -1 ⁡ A · fn T = A ‾ ⋅ ℎ bra -1 ⁡ T