Axiom ax-his3 31085

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 31851 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 11015	. . . 4 class ℂ
3	1, 2	wcel 2113	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30920	. . . 4 class ℋ
6	4, 5	wcel 2113	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2113	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30922	. . . . 5 class ·ℎ
11	1, 4, 10	co 7355	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30923	. . . 4 class ·ih
13	11, 7, 12	co 7355	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7355	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11022	. . . 4 class ·
16	1, 14, 15	co 7355	. . 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  31087  his35  31089  hiassdi  31092  his2sub  31093  hi01  31097  normlem0  31110  normlem9  31119  bcseqi  31121  polid2i  31158  ocsh  31284  h1de2i  31554  normcan  31577  eigrei  31835  eigorthi  31838  bramul  31947  lnopunilem1  32011  hmopm  32022  riesz3i  32063  cnlnadjlem2  32069  adjmul  32093  branmfn  32106  kbass2  32118  kbass5  32121  leopmuli  32134  leopnmid  32139