Axiom ax-his3 8953

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

Assertion

Ref	Expression
ax-his3	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) .ih C) = (A x. (B .ih C)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 5251	. . . 4 class CC
3	1, 2	wcel 960	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 8790	. . . 4 class H~
6	4, 5	wcel 960	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 960	. . 3 wff C e. H~
9	3, 6, 8	w3a 777	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		csm 8792	. . . . 5 class .h
11	1, 4, 10	co 3970	. . . 4 class (A .h B)
12		csp 8795	. . . 4 class .ih
13	11, 7, 12	co 3970	. . 3 class ((A .h B) .ih C)
14	4, 7, 12	co 3970	. . . 4 class (B .ih C)
15		cmul 5258	. . . 4 class x.
16	1, 14, 15	co 3970	. . 3 class (A x. (B .ih C))
17	13, 16	wceq 958	. 2 wff ((A .h B) .ih C) = (A x. (B .ih C))
18	9, 17	wi 3	1 wff ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) .ih C) = (A x. (B .ih C)))

This axiom is referenced by:  his5t 8955  his35 8957  hiassdit 8959  his2subt 8960  hi01t 8964  normlem0 8977  normlem9 8986  bcseq 8988  polid2 9026  ocsh 9158  occllem1 9175  h1de2 9478  normcant 9501  eigre 9762  eigorth 9765  bramult 9872  lnopunilem1 9937  hmopmt 9948  riesz3 9997  cnlnadjlem2 10003  adjmult 10027  branmfnt 10040  kbass2t 10052  kbass5t 10055  leopmulit 10068  leopnmidt 10073

Copyright terms: Public domain