Axiom ax-his3 28959

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 (𝐵 ·_ih (𝐴 ·_ℎ 𝐶)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 29725 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-his3	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

Detailed syntax breakdown of Axiom ax-his3

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cc 10566	. . . 4 class ℂ
3	1, 2	wcel 2112	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 28794	. . . 4 class ℋ
6	4, 5	wcel 2112	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2112	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1085	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28796	. . . . 5 class ·ℎ
11	1, 4, 10	co 7151	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28797	. . . 4 class ·ih
13	11, 7, 12	co 7151	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7151	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10573	. . . 4 class ·
16	1, 14, 15	co 7151	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1539	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28961  his35  28963  hiassdi  28966  his2sub  28967  hi01  28971  normlem0  28984  normlem9  28993  bcseqi  28995  polid2i  29032  ocsh  29158  h1de2i  29428  normcan  29451  eigrei  29709  eigorthi  29712  bramul  29821  lnopunilem1  29885  hmopm  29896  riesz3i  29937  cnlnadjlem2  29943  adjmul  29967  branmfn  29980  kbass2  29992  kbass5  29995  leopmuli  30008  leopnmid  30013