Axiom ax-his3 31159

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 31925 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 11024	. . . 4 class ℂ
3	1, 2	wcel 2113	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30994	. . . 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 30996	. . . . 5 class ·ℎ
11	1, 4, 10	co 7358	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30997	. . . 4 class ·ih
13	11, 7, 12	co 7358	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7358	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11031	. . . 4 class ·
16	1, 14, 15	co 7358	. . 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  31161  his35  31163  hiassdi  31166  his2sub  31167  hi01  31171  normlem0  31184  normlem9  31193  bcseqi  31195  polid2i  31232  ocsh  31358  h1de2i  31628  normcan  31651  eigrei  31909  eigorthi  31912  bramul  32021  lnopunilem1  32085  hmopm  32096  riesz3i  32137  cnlnadjlem2  32143  adjmul  32167  branmfn  32180  kbass2  32192  kbass5  32195  leopmuli  32208  leopnmid  32213