Axiom ax-his3 9100

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 9907 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 5155	. . . 4 class CC
3	1, 2	wcel 1105	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 8968	. . . 4 class H~
6	4, 5	wcel 1105	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 1105	. . 3 wff C e. H~
9	3, 6, 8	w3a 772	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		csm 8970	. . . . 5 class .h
11	1, 4, 10	co 3902	. . . 4 class (A .h B)
12		csp 8973	. . . 4 class .ih
13	11, 7, 12	co 3902	. . 3 class ((A .h B) .ih C)
14	4, 7, 12	co 3902	. . . 4 class (B .ih C)
15		cmul 5162	. . . 4 class x.
16	1, 14, 15	co 3902	. . 3 class (A x. (B .ih C))
17	13, 16	wceq 1099	. 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 9102  his35 9104  hiassdit 9106  his2subt 9107  hi01t 9111  normlem0 9124  normlem9 9133  bcseq 9135  polid2 9173  ocsh 9286  occllem1 9303  h1de2 9605  normcant 9630  eigre 9891  eigorth 9894  bramult 10000  lnopunilem1 10064  hmopmt 10075  riesz3 10124  cnlnadjlem2 10130  adjmult 10153  branmfnt 10165  kbass2t 10176  kbass5t 10179  leopmulit 10192  leopnmidt 10196

Copyright terms: Public domain