Axiom ax-his3 28221

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 28989 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 10097	. . . 4 class ℂ
3	1, 2	wcel 2127	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chil 28056	. . . 4 class ℋ
6	4, 5	wcel 2127	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2127	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1072	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 28058	. . . . 5 class ·ℎ
11	1, 4, 10	co 6801	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 28059	. . . 4 class ·ih
13	11, 7, 12	co 6801	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 6801	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10104	. . . 4 class ·
16	1, 14, 15	co 6801	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1620	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  28223  his35  28225  hiassdi  28228  his2sub  28229  hi01  28233  normlem0  28246  normlem9  28255  bcseqi  28257  polid2i  28294  ocsh  28422  h1de2i  28692  normcan  28715  eigrei  28973  eigorthi  28976  bramul  29085  lnopunilem1  29149  hmopm  29160  riesz3i  29201  cnlnadjlem2  29207  adjmul  29231  branmfn  29244  kbass2  29256  kbass5  29259  leopmuli  29272  leopnmid  29277