Theorem kbmul

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

	Ref	Expression
Assertion	kbmul	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ketbra 𝐶 ) = ( 𝐵 ketbra ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvmulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ )
2		kbfval	⊢ ( ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ketbra 𝐶 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) ) )
3	1 2	stoic3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ketbra 𝐶 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) ) )
4		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → 𝐵 ∈ ℋ )
5		cjcl	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → 𝐶 ∈ ℋ )
8		hvmulcl	⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ∈ ℋ )
9	6 7 8	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ∈ ℋ )
10		kbfval	⊢ ( ( 𝐵 ∈ ℋ ∧ ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ∈ ℋ ) → ( 𝐵 ketbra ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) ·ℎ 𝐵 ) ) )
11	4 9 10	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ketbra ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) ·ℎ 𝐵 ) ) )
12		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
13		simpl3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐶 ∈ ℋ )
14		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑥 ·ih 𝐶 ) ∈ ℂ )
15	12 13 14	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐶 ) ∈ ℂ )
16		simpl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐴 ∈ ℂ )
17		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝐵 ∈ ℋ )
18		ax-hvmulass	⊢ ( ( ( 𝑥 ·ih 𝐶 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐶 ) · 𝐴 ) ·ℎ 𝐵 ) = ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) )
19	15 16 17 18	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐶 ) · 𝐴 ) ·ℎ 𝐵 ) = ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) )
20	15 16	mulcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐶 ) · 𝐴 ) = ( 𝐴 · ( 𝑥 ·ih 𝐶 ) ) )
21		his52	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝐴 · ( 𝑥 ·ih 𝐶 ) ) )
22	16 12 13 21	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝐴 · ( 𝑥 ·ih 𝐶 ) ) )
23	20 22	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐶 ) · 𝐴 ) = ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) )
24	23	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝐶 ) · 𝐴 ) ·ℎ 𝐵 ) = ( ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) ·ℎ 𝐵 ) )
25	19 24	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) = ( ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) ·ℎ 𝐵 ) )
26	25	mpteq2dva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) ·ℎ 𝐵 ) ) )
27	11 26	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ketbra ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑥 ·ih 𝐶 ) ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) ) )
28	3 27	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) ketbra 𝐶 ) = ( 𝐵 ketbra ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) )