Axiom ax-his3 31103

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 31869 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 11153	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30938	. . . 4 class ℋ
6	4, 5	wcel 2108	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2108	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30940	. . . . 5 class ·ℎ
11	1, 4, 10	co 7431	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30941	. . . 4 class ·ih
13	11, 7, 12	co 7431	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7431	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11160	. . . 4 class ·
16	1, 14, 15	co 7431	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1540	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  31105  his35  31107  hiassdi  31110  his2sub  31111  hi01  31115  normlem0  31128  normlem9  31137  bcseqi  31139  polid2i  31176  ocsh  31302  h1de2i  31572  normcan  31595  eigrei  31853  eigorthi  31856  bramul  31965  lnopunilem1  32029  hmopm  32040  riesz3i  32081  cnlnadjlem2  32087  adjmul  32111  branmfn  32124  kbass2  32136  kbass5  32139  leopmuli  32152  leopnmid  32157