Axiom ax-his3 29347

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 30113 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 10800	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5		chba 29182	. . . 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 1085	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ)
10		csm 29184	. . . . 5 class ·ℎ
11	1, 4, 10	co 7255	. . . 4 class (𝐴 ·ℎ 𝐵)
12		csp 29185	. . . 4 class ·ih
13	11, 7, 12	co 7255	. . 3 class ((𝐴 ·ℎ 𝐵) ·ih 𝐶)
14	4, 7, 12	co 7255	. . . 4 class (𝐵 ·ih 𝐶)
15		cmul 10807	. . . 4 class ·
16	1, 14, 15	co 7255	. . 3 class (𝐴 · (𝐵 ·ih 𝐶))
17	13, 16	wceq 1539	. 2 wff ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))
18	9, 17	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))

This axiom is referenced by:  his5  29349  his35  29351  hiassdi  29354  his2sub  29355  hi01  29359  normlem0  29372  normlem9  29381  bcseqi  29383  polid2i  29420  ocsh  29546  h1de2i  29816  normcan  29839  eigrei  30097  eigorthi  30100  bramul  30209  lnopunilem1  30273  hmopm  30284  riesz3i  30325  cnlnadjlem2  30331  adjmul  30355  branmfn  30368  kbass2  30380  kbass5  30383  leopmuli  30396  leopnmid  30401