Axiom ax-his3 9227

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 10056 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 5386	. . . 4 class CC
3	1, 2	wcel 994	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 9063	. . . 4 class H~
6	4, 5	wcel 994	. . 3 wff B e. H~
7		cC	. . . 4 class C
8	7, 5	wcel 994	. . 3 wff C e. H~
9	3, 6, 8	w3a 781	. 2 wff (A e. CC /\ B e. H~ /\ C e. H~)
10		csm 9065	. . . . 5 class .h
11	1, 4, 10	co 4021	. . . 4 class (A .h B)
12		csp 9068	. . . 4 class .ih
13	11, 7, 12	co 4021	. . 3 class ((A .h B) .ih C)
14	4, 7, 12	co 4021	. . . 4 class (B .ih C)
15		cmul 5393	. . . 4 class x.
16	1, 14, 15	co 4021	. . 3 class (A x. (B .ih C))
17	13, 16	wceq 992	. 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:  his5 9229  his35i 9231  hiassdi 9233  his2sub 9234  hi01 9238  normlem0 9251  normlem9 9260  bcseqi 9262  polid2i 9300  ocsh 9432  occllem1 9449  h1de2i 9752  normcan 9775  eigrei 10040  eigorthi 10043  bramul 10150  lnopunilem1 10214  hmopm 10225  riesz3i 10274  cnlnadjlem2 10280  adjmul 10304  branmfn 10317  branmfnOLD 10318  kbass2 10330  kbass5 10333  leopmuli 10346  leopnmid 10351

Copyright terms: Public domain