Axiom ax-his3 8890

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 9716 for why the physics definition is swapped.

Assertion

Ref	Expression
ax-his3	⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A ·h B) ·ih C) = (A · (B ·ih C)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 5212	. . . 4 class ℂ
3	1, 2	wcel 956	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5		chil 8727	. . . 4 class ℋ
6	4, 5	wcel 956	. . 3 wff B ∈ ℋ
7		cC	. . . 4 class C
8	7, 5	wcel 956	. . 3 wff C ∈ ℋ
9	3, 6, 8	w3a 774	. 2 wff (A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ )
10		csm 8729	. . . . 5 class ·h
11	1, 4, 10	co 3954	. . . 4 class (A ·h B)
12		csp 8732	. . . 4 class ·ih
13	11, 7, 12	co 3954	. . 3 class ((A ·h B) ·ih C)
14	4, 7, 12	co 3954	. . . 4 class (B ·ih C)
15		cmul 5219	. . . 4 class ·
16	1, 14, 15	co 3954	. . 3 class (A · (B ·ih C))
17	13, 16	wceq 954	. 2 wff ((A ·h B) ·ih C) = (A · (B ·ih C))
18	9, 17	wi 3	1 wff ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A ·h B) ·ih C) = (A · (B ·ih C)))

This axiom is referenced by:  his5t 8892  his35 8894  hiassdit 8896  his2subt 8897  hi01t 8901  normlem0 8914  normlem9 8923  bcseq 8925  polid2 8963  ocsh 9095  occllem1 9112  h1de2 9414  normcant 9439  eigre 9700  eigorth 9703  bramult 9809  lnopunilem1 9873  hmopmt 9884  riesz3 9933  cnlnadjlem2 9939  adjmult 9963  branmfnt 9976  kbass2t 9988  kbass5t 9991  leopmulit 10004  leopnmidt 10009

Copyright terms: Public domain