# Metamath Proof Explorer

## Axiom ax-his3

Description: Associative law for inner product. Postulate (S3) of Beran p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with ( B .ih ( A .h C ) ) (e.g., Equation 1.21b of Hughes p. 44; Definition (iii) of ReedSimon p. 36). See the comments in df-bra for why the physics definition is swapped. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-his3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 · 𝐵 ) ·ih 𝐶 ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) ) )

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cc
2 0 1 wcel 𝐴 ∈ ℂ
3 cB 𝐵
4 chba
5 3 4 wcel 𝐵 ∈ ℋ
6 cC 𝐶
7 6 4 wcel 𝐶 ∈ ℋ
8 2 5 7 w3a ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ )
9 csm ·
10 0 3 9 co ( 𝐴 · 𝐵 )
11 csp ·ih
12 10 6 11 co ( ( 𝐴 · 𝐵 ) ·ih 𝐶 )
13 cmul ·
14 3 6 11 co ( 𝐵 ·ih 𝐶 )
15 0 14 13 co ( 𝐴 · ( 𝐵 ·ih 𝐶 ) )
16 12 15 wceq ( ( 𝐴 · 𝐵 ) ·ih 𝐶 ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) )
17 8 16 wi ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 · 𝐵 ) ·ih 𝐶 ) = ( 𝐴 · ( 𝐵 ·ih 𝐶 ) ) )