Theorem his5

Description: Associative law for inner product. Lemma 3.1(S5) of Beran p. 95. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hvmulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐶 ) ∈ ℋ )
2		ax-his1	⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ·ℎ 𝐶 ) ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 ·ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) ) )
3	1 2	sylan2	⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) ) → ( 𝐵 ·ih ( 𝐴 ·ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) ) )
4	3	3impb	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 ·ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) ) )
5	4	3com12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 ·ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) ) )
6		ax-his3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) = ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) )
7	6	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) = ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) )
8	7	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐴 ·ℎ 𝐶 ) ·ih 𝐵 ) ) = ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) )
9		hicl	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ·ih 𝐵 ) ∈ ℂ )
10		cjmul	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ·ih 𝐵 ) ∈ ℂ ) → ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) )
11	9 10	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ) → ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) )
12	11	3impb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) )
13	12	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) )
14		ax-his1	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) )
15	14	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) )
16	15	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐵 ·ih 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ∗ ‘ ( 𝐶 ·ih 𝐵 ) ) ) )
17	13 16	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( 𝐴 · ( 𝐶 ·ih 𝐵 ) ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐵 ·ih 𝐶 ) ) )
18	5 8 17	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 ·ℎ 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐵 ·ih 𝐶 ) ) )