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 ๐ถ ) ) )