Axiom ax-his3 31056

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 31822 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 10999	. . . 4 class ℂ
3	1, 2	wcel 2111	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30891	. . . 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 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30893	. . . . 5 class ·ℎ
11	1, 4, 10	co 7341	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30894	. . . 4 class ·ih
13	11, 7, 12	co 7341	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7341	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11006	. . . 4 class ·
16	1, 14, 15	co 7341	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1541	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31058  his35  31060  hiassdi  31063  his2sub  31064  hi01  31068  normlem0  31081  normlem9  31090  bcseqi  31092  polid2i  31129  ocsh  31255  h1de2i  31525  normcan  31548  eigrei  31806  eigorthi  31809  bramul  31918  lnopunilem1  31982  hmopm  31993  riesz3i  32034  cnlnadjlem2  32040  adjmul  32064  branmfn  32077  kbass2  32089  kbass5  32092  leopmuli  32105  leopnmid  32110