Axiom ax-his3 30604

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 31370 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 11110	. . . 4 class ℂ
3	1, 2	wcel 2104	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30439	. . . 4 class ℋ
6	4, 5	wcel 2104	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2104	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1085	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30441	. . . . 5 class ·ℎ
11	1, 4, 10	co 7411	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30442	. . . 4 class ·ih
13	11, 7, 12	co 7411	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7411	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11117	. . . 4 class ·
16	1, 14, 15	co 7411	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1539	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  30606  his35  30608  hiassdi  30611  his2sub  30612  hi01  30616  normlem0  30629  normlem9  30638  bcseqi  30640  polid2i  30677  ocsh  30803  h1de2i  31073  normcan  31096  eigrei  31354  eigorthi  31357  bramul  31466  lnopunilem1  31530  hmopm  31541  riesz3i  31582  cnlnadjlem2  31588  adjmul  31612  branmfn  31625  kbass2  31637  kbass5  31640  leopmuli  31653  leopnmid  31658