Axiom ax-his3 30302

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 31068 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 11095	. . . 4 class ℂ
3	1, 2	wcel 2107	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 30137	. . . 4 class ℋ
6	4, 5	wcel 2107	. . 3 wff 𝐵 ∈ ℋ
7		cC	. . . 4 class 𝐶
8	7, 5	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 6, 8	w3a 1088	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 30139	. . . . 5 class ·ℎ
11	1, 4, 10	co 7396	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 30140	. . . 4 class ·ih
13	11, 7, 12	co 7396	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7396	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 11102	. . . 4 class ·
16	1, 14, 15	co 7396	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1542	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  30304  his35  30306  hiassdi  30309  his2sub  30310  hi01  30314  normlem0  30327  normlem9  30336  bcseqi  30338  polid2i  30375  ocsh  30501  h1de2i  30771  normcan  30794  eigrei  31052  eigorthi  31055  bramul  31164  lnopunilem1  31228  hmopm  31239  riesz3i  31280  cnlnadjlem2  31286  adjmul  31310  branmfn  31323  kbass2  31335  kbass5  31338  leopmuli  31351  leopnmid  31356