Axiom ax-his3 28867

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 29633 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 10524	. . . 4 class ℂ
3	1, 2	wcel 2111	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 28702	. . . 4 class ℋ
6	4, 5	wcel 2111	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2111	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1084	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28704	. . . . 5 class ·ℎ
11	1, 4, 10	co 7135	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28705	. . . 4 class ·ih
13	11, 7, 12	co 7135	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7135	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10531	. . . 4 class ·
16	1, 14, 15	co 7135	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1538	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28869  his35  28871  hiassdi  28874  his2sub  28875  hi01  28879  normlem0  28892  normlem9  28901  bcseqi  28903  polid2i  28940  ocsh  29066  h1de2i  29336  normcan  29359  eigrei  29617  eigorthi  29620  bramul  29729  lnopunilem1  29793  hmopm  29804  riesz3i  29845  cnlnadjlem2  29851  adjmul  29875  branmfn  29888  kbass2  29900  kbass5  29903  leopmuli  29916  leopnmid  29921