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 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ⋅ ih C = A ⁢ B ⋅ ih C

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class ℂ
2 0 1 wcel wff A ∈ ℂ
3 cB class B
4 chba class ℋ
5 3 4 wcel wff B ∈ ℋ
6 cC class C
7 6 4 wcel wff C ∈ ℋ
8 2 5 7 w3a wff A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ
9 csm class ⋅ ℎ
10 0 3 9 co class A ⋅ ℎ B
11 csp class ⋅ ih
12 10 6 11 co class A ⋅ ℎ B ⋅ ih C
13 cmul class ×
14 3 6 11 co class B ⋅ ih C
15 0 14 13 co class A ⁢ B ⋅ ih C
16 12 15 wceq wff A ⋅ ℎ B ⋅ ih C = A ⁢ B ⋅ ih C
17 8 16 wi wff A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ⋅ ih C = A ⁢ B ⋅ ih C