Axiom ax-his3 31679

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 32445 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 11191	. . . 4 class ℂ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31514	. . . 4 class ℋ
6	4, 5	wcel 2145	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2145	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31516	. . . . 5 class ·ℎ
11	1, 4, 10	co 7418	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31517	. . . 4 class ·ih
13	11, 7, 12	co 7418	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7418	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11198	. . . 4 class ·
16	1, 14, 15	co 7418	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1570	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is used by:  his5  31681  his35  31683  hiassdi  31686  his2sub  31687  hi01  31691  normlem0  31704  normlem9  31713  bcseqi  31715  polid2i  31752  ocsh  31878  h1de2i  32148  normcan  32171  eigrei  32429  eigorthi  32432  bramul  32541  lnopunilem1  32605  hmopm  32616  riesz3i  32657  cnlnadjlem2  32663  adjmul  32687  branmfn  32700  kbass2  32712  kbass5  32715  leopmuli  32728  leopnmid  32733