Theorem his35

Description: Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	his35	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 ·ih 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		his5	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) )
2	1	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) )
3	2	adantll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) )
4	3	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) )
5		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐴 ∈ ℂ )
6		simprl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → 𝐶 ∈ ℋ )
7		hvmulcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ )
8	7	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ )
9		ax-his3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ ( 𝐵 ·ℎ 𝐷 ) ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) )
10	5 6 8 9	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( 𝐴 · ( 𝐶 ·ih ( 𝐵 ·ℎ 𝐷 ) ) ) )
11		cjcl	⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
12	11	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
13		hicl	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 ·ih 𝐷 ) ∈ ℂ )
14	13	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 ·ih 𝐷 ) ∈ ℂ )
15	5 12 14	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 ·ih 𝐷 ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 ·ih 𝐷 ) ) ) )
16	4 10 15	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih ( 𝐵 ·ℎ 𝐷 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 ·ih 𝐷 ) ) )