Axiom ax-his3 8872

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 9693 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 5204	. . . 4 class CC
3	1, 2	wcel 955	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 8727	. . . 4 class H~
6	4, 5	wcel 955	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 955	. . 3 wff C e. H~
9	3, 6, 8	w3a 773	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		csm 8729	. . . . 5 class .h
11	1, 4, 10	co 3948	. . . 4 class (A .h B)
12		csp 8732	. . . 4 class .ih
13	11, 7, 12	co 3948	. . 3 class ((A .h B) .ih C)
14	4, 7, 12	co 3948	. . . 4 class (B .ih C)
15		cmul 5211	. . . 4 class x.
16	1, 14, 15	co 3948	. . 3 class (A x. (B .ih C))
17	13, 16	wceq 953	. 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 8874  his35 8876  hiassdit 8878  his2subt 8879  hi01t 8883  normlem0 8896  normlem9 8905  bcseq 8907  polid2 8945  ocsh 9072  occllem1 9089  h1de2 9391  normcant 9416  eigre 9677  eigorth 9680  bramult 9786  lnopunilem1 9850  hmopmt 9861  riesz3 9910  cnlnadjlem2 9916  adjmult 9939  branmfnt 9951  kbass2t 9962  kbass5t 9965  leopmulit 9978  leopnmidt 9982

Copyright terms: Public domain