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

Metamath Proof Explorer

Theorem his52

Description: Associative law for inner product. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
2 his5 ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐶 ) ) )
3 1 2 syl3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐶 ) ) )
4 cjcj ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
5 4 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐶 ) ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) · ( 𝐵 ·ih 𝐶 ) ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) ) )
7 3 6 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( ( ∗ ‘ 𝐴 ) ·ℎ 𝐶 ) ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) ) )