Metamath Proof Explorer

Theorem kbmul

Description: Multiplication property of outer product. (Contributed by NM, 31-May-2006) (New usage is discouraged.)

Ref Expression
Assertion kbmul ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ketbra C = B ketbra A ‾ ⋅ ℎ C

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
2 kbfval ⊢ A ⋅ ℎ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ketbra C = x ∈ ℋ ⟼ x ⋅ ih C ⋅ ℎ A ⋅ ℎ B
3 1 2 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ketbra C = x ∈ ℋ ⟼ x ⋅ ih C ⋅ ℎ A ⋅ ℎ B
4 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ∈ ℋ
5 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
6 5 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ‾ ∈ ℂ
7 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → C ∈ ℋ
8 hvmulcl ⊢ A ‾ ∈ ℂ ∧ C ∈ ℋ → A ‾ ⋅ ℎ C ∈ ℋ
9 6 7 8 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ‾ ⋅ ℎ C ∈ ℋ
10 kbfval ⊢ B ∈ ℋ ∧ A ‾ ⋅ ℎ C ∈ ℋ → B ketbra A ‾ ⋅ ℎ C = x ∈ ℋ ⟼ x ⋅ ih A ‾ ⋅ ℎ C ⋅ ℎ B
11 4 9 10 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ketbra A ‾ ⋅ ℎ C = x ∈ ℋ ⟼ x ⋅ ih A ‾ ⋅ ℎ C ⋅ ℎ B
12 simpr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ∈ ℋ
13 simpl3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → C ∈ ℋ
14 hicl ⊢ x ∈ ℋ ∧ C ∈ ℋ → x ⋅ ih C ∈ ℂ
15 12 13 14 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ∈ ℂ
16 simpl1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → A ∈ ℂ
17 simpl2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → B ∈ ℋ
18 ax-hvmulass ⊢ x ⋅ ih C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℋ → x ⋅ ih C ⁢ A ⋅ ℎ B = x ⋅ ih C ⋅ ℎ A ⋅ ℎ B
19 15 16 17 18 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⁢ A ⋅ ℎ B = x ⋅ ih C ⋅ ℎ A ⋅ ℎ B
20 15 16 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⁢ A = A ⁢ x ⋅ ih C
21 his52 ⊢ A ∈ ℂ ∧ x ∈ ℋ ∧ C ∈ ℋ → x ⋅ ih A ‾ ⋅ ℎ C = A ⁢ x ⋅ ih C
22 16 12 13 21 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih A ‾ ⋅ ℎ C = A ⁢ x ⋅ ih C
23 20 22 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⁢ A = x ⋅ ih A ‾ ⋅ ℎ C
24 23 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⁢ A ⋅ ℎ B = x ⋅ ih A ‾ ⋅ ℎ C ⋅ ℎ B
25 19 24 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih C ⋅ ℎ A ⋅ ℎ B = x ⋅ ih A ‾ ⋅ ℎ C ⋅ ℎ B
26 25 mpteq2dva ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → x ∈ ℋ ⟼ x ⋅ ih C ⋅ ℎ A ⋅ ℎ B = x ∈ ℋ ⟼ x ⋅ ih A ‾ ⋅ ℎ C ⋅ ℎ B
27 11 26 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ketbra A ‾ ⋅ ℎ C = x ∈ ℋ ⟼ x ⋅ ih C ⋅ ℎ A ⋅ ℎ B
28 3 27 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ketbra C = B ketbra A ‾ ⋅ ℎ C