Metamath Proof Explorer


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 𝐷 ) ) )