Axiom ax-his3 31172

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 31938 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 11036	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31007	. . . 4 class ℋ
6	4, 5	wcel 2114	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31009	. . . . 5 class ·ℎ
11	1, 4, 10	co 7368	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31010	. . . 4 class ·ih
13	11, 7, 12	co 7368	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7368	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11043	. . . 4 class ·
16	1, 14, 15	co 7368	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1542	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31174  his35  31176  hiassdi  31179  his2sub  31180  hi01  31184  normlem0  31197  normlem9  31206  bcseqi  31208  polid2i  31245  ocsh  31371  h1de2i  31641  normcan  31664  eigrei  31922  eigorthi  31925  bramul  32034  lnopunilem1  32098  hmopm  32109  riesz3i  32150  cnlnadjlem2  32156  adjmul  32180  branmfn  32193  kbass2  32205  kbass5  32208  leopmuli  32221  leopnmid  32226