Axiom ax-his3 10376

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 11205 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 6180	. . . 4 class CC
3	1, 2	wcel 1138	. . 3 wff A e. CC
4		cB	. . . 4 class B
5		chil 10212	. . . 4 class ~H
6	4, 5	wcel 1138	. . 3 wff B e. ~H
7		cC	. . . 4 class C
8	7, 5	wcel 1138	. . 3 wff C e. ~H
9	3, 6, 8	w3a 855	. 2 wff (A e. CC /\ B e. ~H /\ C e. ~H)
10		csm 10214	. . . . 5 class .h
11	1, 4, 10	co 4695	. . . 4 class (A .h B)
12		csp 10217	. . . 4 class .ih
13	11, 7, 12	co 4695	. . 3 class ((A .h B) .ih C)
14	4, 7, 12	co 4695	. . . 4 class (B .ih C)
15		cmul 6187	. . . 4 class x.
16	1, 14, 15	co 4695	. . 3 class (A x. (B .ih C))
17	13, 16	wceq 1136	. 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 10378  his35i 10380  hiassdi 10382  his2sub 10383  hi01 10387  normlem0 10400  normlem9 10409  bcseqi 10411  polid2i 10449  ocsh 10581  occllem1 10598  h1de2i 10901  normcan 10924  eigrei 11189  eigorthi 11192  bramul 11299  lnopunilem1 11364  hmopm 11375  riesz3i 11424  cnlnadjlem2 11430  adjmul 11454  branmfn 11467  branmfnOLD 11468  kbass2 11480  kbass5 11483  leopmuli 11496  leopnmid 11501

Copyright terms: Public domain