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 𝐶 ) ) )

Metamath Proof Explorer

Axiom ax-his3

Detailed syntax breakdown