Axiom ax-his3 31173

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 31939 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 11027	. . . 4 class ℂ
3	1, 2	wcel 2119	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 31008	. . . 4 class ℋ
6	4, 5	wcel 2119	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2119	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1092	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 31010	. . . . 5 class ·ℎ
11	1, 4, 10	co 7356	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 31011	. . . 4 class ·ih
13	11, 7, 12	co 7356	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7356	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11034	. . . 4 class ·
16	1, 14, 15	co 7356	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1547	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31175  his35  31177  hiassdi  31180  his2sub  31181  hi01  31185  normlem0  31198  normlem9  31207  bcseqi  31209  polid2i  31246  ocsh  31372  h1de2i  31642  normcan  31665  eigrei  31923  eigorthi  31926  bramul  32035  lnopunilem1  32099  hmopm  32110  riesz3i  32151  cnlnadjlem2  32157  adjmul  32181  branmfn  32194  kbass2  32206  kbass5  32209  leopmuli  32222  leopnmid  32227