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·opT=A·opB·opT

Proof

Step Hyp Ref Expression
1 mulcl ⊢A∈ℂ∧B∈ℂ→A⁢B∈ℂ
2 homval ⊢A⁢B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⁢B·opT⁡x=A⁢B⋅ℎT⁡x
3 1 2 syl3an1 ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⁢B·opT⁡x=A⁢B⋅ℎT⁡x
4 3 3expia ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→x∈ℋ→A⁢B·opT⁡x=A⁢B⋅ℎT⁡x
5 4 3impa ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→x∈ℋ→A⁢B·opT⁡x=A⁢B⋅ℎT⁡x
6 5 imp ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⁢B·opT⁡x=A⁢B⋅ℎT⁡x
7 homval ⊢B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→B·opT⁡x=B⋅ℎT⁡x
8 7 oveq2d ⊢B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⋅ℎB·opT⁡x=A⋅ℎB⋅ℎT⁡x
9 8 3expa ⊢B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⋅ℎB·opT⁡x=A⋅ℎB⋅ℎT⁡x
10 9 3adantl1 ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⋅ℎB·opT⁡x=A⋅ℎB⋅ℎT⁡x
11 ffvelcdm ⊢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·opT⁡x=A⁢B⋅ℎT⁡x
18 6 17 eqtr4d ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⁢B·opT⁡x=A⋅ℎB·opT⁡x
19 homulcl ⊢B∈ℂ∧T:ℋ⟶ℋ→B·opT:ℋ⟶ℋ
20 homval ⊢A∈ℂ∧B·opT:ℋ⟶ℋ∧x∈ℋ→A·opB·opT⁡x=A⋅ℎB·opT⁡x
21 19 20 syl3an2 ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opB·opT⁡x=A⋅ℎB·opT⁡x
22 21 3expia ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→x∈ℋ→A·opB·opT⁡x=A⋅ℎB·opT⁡x
23 22 3impb ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→x∈ℋ→A·opB·opT⁡x=A⋅ℎB·opT⁡x
24 23 imp ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opB·opT⁡x=A⋅ℎB·opT⁡x
25 18 24 eqtr4d ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⁢B·opT⁡x=A·opB·opT⁡x
26 25 ralrimiva ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→∀x∈ℋA⁢B·opT⁡x=A·opB·opT⁡x
27 homulcl ⊢A⁢B∈ℂ∧T:ℋ⟶ℋ→A⁢B·opT:ℋ⟶ℋ
28 1 27 stoic3 ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→A⁢B·opT:ℋ⟶ℋ
29 homulcl ⊢A∈ℂ∧B·opT:ℋ⟶ℋ→A·opB·opT:ℋ⟶ℋ
30 19 29 sylan2 ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→A·opB·opT:ℋ⟶ℋ
31 30 3impb ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→A·opB·opT:ℋ⟶ℋ
32 hoeq ⊢A⁢B·opT:ℋ⟶ℋ∧A·opB·opT:ℋ⟶ℋ→∀x∈ℋA⁢B·opT⁡x=A·opB·opT⁡x↔A⁢B·opT=A·opB·opT
33 28 31 32 syl2anc ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→∀x∈ℋA⁢B·opT⁡x=A·opB·opT⁡x↔A⁢B·opT=A·opB·opT
34 26 33 mpbid ⊢A∈ℂ∧B∈ℂ∧T:ℋ⟶ℋ→A⁢B·opT=A·opB·opT