Metamath Proof Explorer

Theorem homulass

Description: Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion homulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A ⁢ B · op T = A · op B · op T

Proof

Step Hyp Ref Expression
1 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
2 homval ⊢ A ⁢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
3 1 2 syl3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
4 3 3expia ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
5 4 3impa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
6 5 imp ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
7 homval ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → B · op T ⁡ x = B ⋅ ℎ T ⁡ x
8 7 oveq2d ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ B · op T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
9 8 3expa ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ B · op T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
10 9 3adantl1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ B · op T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
11 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
12 ax-hvmulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T ⁡ x ∈ ℋ → A ⁢ B ⋅ ℎ T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
13 11 12 syl3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B ⋅ ℎ T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
14 13 3expa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B ⋅ ℎ T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
15 14 exp43 ⊢ A ∈ ℂ → B ∈ ℂ → T : ℋ ⟶ ℋ → x ∈ ℋ → A ⁢ B ⋅ ℎ T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
16 15 3imp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B ⋅ ℎ T ⁡ x = A ⋅ ℎ B ⋅ ℎ T ⁡ x
17 10 16 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ B · op T ⁡ x = A ⁢ B ⋅ ℎ T ⁡ x
18 6 17 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
19 homulcl ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → B · op T : ℋ ⟶ ℋ
20 homval ⊢ A ∈ ℂ ∧ B · op T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
21 19 20 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
22 21 3expia ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → x ∈ ℋ → A · op B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
23 22 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → x ∈ ℋ → A · op B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
24 23 imp ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op B · op T ⁡ x = A ⋅ ℎ B · op T ⁡ x
25 18 24 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⁢ B · op T ⁡ x = A · op B · op T ⁡ x
26 25 ralrimiva ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A ⁢ B · op T ⁡ x = A · op B · op T ⁡ x
27 homulcl ⊢ A ⁢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A ⁢ B · op T : ℋ ⟶ ℋ
28 1 27 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A ⁢ B · op T : ℋ ⟶ ℋ
29 homulcl ⊢ A ∈ ℂ ∧ B · op T : ℋ ⟶ ℋ → A · op B · op T : ℋ ⟶ ℋ
30 19 29 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op B · op T : ℋ ⟶ ℋ
31 30 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op B · op T : ℋ ⟶ ℋ
32 hoeq ⊢ A ⁢ B · op T : ℋ ⟶ ℋ ∧ A · op B · op T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A ⁢ B · op T ⁡ x = A · op B · op T ⁡ x ↔ A ⁢ B · op T = A · op B · op T
33 28 31 32 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A ⁢ B · op T ⁡ x = A · op B · op T ⁡ x ↔ A ⁢ B · op T = A · op B · op T
34 26 33 mpbid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A ⁢ B · op T = A · op B · op T