Axiom ax-his3 31112

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 31878 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 11150	. . . 4 class ℂ
3	1, 2	wcel 2105	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30947	. . . 4 class ℋ
6	4, 5	wcel 2105	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2105	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30949	. . . . 5 class ·ℎ
11	1, 4, 10	co 7430	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30950	. . . 4 class ·ih
13	11, 7, 12	co 7430	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7430	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11157	. . . 4 class ·
16	1, 14, 15	co 7430	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1536	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31114  his35  31116  hiassdi  31119  his2sub  31120  hi01  31124  normlem0  31137  normlem9  31146  bcseqi  31148  polid2i  31185  ocsh  31311  h1de2i  31581  normcan  31604  eigrei  31862  eigorthi  31865  bramul  31974  lnopunilem1  32038  hmopm  32049  riesz3i  32090  cnlnadjlem2  32096  adjmul  32120  branmfn  32133  kbass2  32145  kbass5  32148  leopmuli  32161  leopnmid  32166