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⋅ℎBketbraC=BketbraA‾⋅ℎC

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢A∈ℂ∧B∈ℋ→A⋅ℎB∈ℋ
2 kbfval ⊢A⋅ℎB∈ℋ∧C∈ℋ→A⋅ℎBketbraC=x∈ℋ⟼x⋅ihC⋅ℎA⋅ℎB
3 1 2 stoic3 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⋅ℎBketbraC=x∈ℋ⟼x⋅ihC⋅ℎ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∈ℋ→BketbraA‾⋅ℎC=x∈ℋ⟼x⋅ihA‾⋅ℎC⋅ℎB
11 4 9 10 syl2anc ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→BketbraA‾⋅ℎC=x∈ℋ⟼x⋅ihA‾⋅ℎC⋅ℎB
12 simpr ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x∈ℋ
13 simpl3 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→C∈ℋ
14 hicl ⊢x∈ℋ∧C∈ℋ→x⋅ihC∈ℂ
15 12 13 14 syl2anc ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC∈ℂ
16 simpl1 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→A∈ℂ
17 simpl2 ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→B∈ℋ
18 ax-hvmulass ⊢x⋅ihC∈ℂ∧A∈ℂ∧B∈ℋ→x⋅ihC⁢A⋅ℎB=x⋅ihC⋅ℎA⋅ℎB
19 15 16 17 18 syl3anc ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⁢A⋅ℎB=x⋅ihC⋅ℎA⋅ℎB
20 15 16 mulcomd ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⁢A=A⁢x⋅ihC
21 his52 ⊢A∈ℂ∧x∈ℋ∧C∈ℋ→x⋅ihA‾⋅ℎC=A⁢x⋅ihC
22 16 12 13 21 syl3anc ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihA‾⋅ℎC=A⁢x⋅ihC
23 20 22 eqtr4d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⁢A=x⋅ihA‾⋅ℎC
24 23 oveq1d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⁢A⋅ℎB=x⋅ihA‾⋅ℎC⋅ℎB
25 19 24 eqtr3d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ∧x∈ℋ→x⋅ihC⋅ℎA⋅ℎB=x⋅ihA‾⋅ℎC⋅ℎB
26 25 mpteq2dva ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→x∈ℋ⟼x⋅ihC⋅ℎA⋅ℎB=x∈ℋ⟼x⋅ihA‾⋅ℎC⋅ℎB
27 11 26 eqtr4d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→BketbraA‾⋅ℎC=x∈ℋ⟼x⋅ihC⋅ℎA⋅ℎB
28 3 27 eqtr4d ⊢A∈ℂ∧B∈ℋ∧C∈ℋ→A⋅ℎBketbraC=BketbraA‾⋅ℎC