Axiom ax-his3 31436

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 32202 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 11093	. . . 4 class ℂ
3	1, 2	wcel 2143	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31271	. . . 4 class ℋ
6	4, 5	wcel 2143	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2143	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31273	. . . . 5 class ·ℎ
11	1, 4, 10	co 7410	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31274	. . . 4 class ·ih
13	11, 7, 12	co 7410	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7410	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11100	. . . 4 class ·
16	1, 14, 15	co 7410	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1570	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31438  his35  31440  hiassdi  31443  his2sub  31444  hi01  31448  normlem0  31461  normlem9  31470  bcseqi  31472  polid2i  31509  ocsh  31635  h1de2i  31905  normcan  31928  eigrei  32186  eigorthi  32189  bramul  32298  lnopunilem1  32362  hmopm  32373  riesz3i  32414  cnlnadjlem2  32420  adjmul  32444  branmfn  32457  kbass2  32469  kbass5  32472  leopmuli  32485  leopnmid  32490