This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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