Axiom ax-his3 31244

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 32010 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 11065	. . . 4 class ℂ
3	1, 2	wcel 2141	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31079	. . . 4 class ℋ
6	4, 5	wcel 2141	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2141	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1097	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31081	. . . . 5 class ·ℎ
11	1, 4, 10	co 7391	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31082	. . . 4 class ·ih
13	11, 7, 12	co 7391	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7391	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11072	. . . 4 class ·
16	1, 14, 15	co 7391	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1559	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31246  his35  31248  hiassdi  31251  his2sub  31252  hi01  31256  normlem0  31269  normlem9  31278  bcseqi  31280  polid2i  31317  ocsh  31443  h1de2i  31713  normcan  31736  eigrei  31994  eigorthi  31997  bramul  32106  lnopunilem1  32170  hmopm  32181  riesz3i  32222  cnlnadjlem2  32228  adjmul  32252  branmfn  32265  kbass2  32277  kbass5  32280  leopmuli  32293  leopnmid  32298