Metamath Proof Explorer

Theorem hoadddir

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

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

Proof

Step Hyp Ref Expression
1 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
2 1 anim1i ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A + B ∈ ℂ ∧ T : ℋ ⟶ ℋ
3 2 3impa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A + B ∈ ℂ ∧ T : ℋ ⟶ ℋ
4 homval ⊢ A + B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B · op T ⁡ x = A + B ⋅ ℎ T ⁡ x
5 4 3expa ⊢ A + B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B · op T ⁡ x = A + B ⋅ ℎ T ⁡ x
6 3 5 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B · op T ⁡ x = A + B ⋅ ℎ T ⁡ x
7 homval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
8 7 3expa ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
9 8 3adantl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
10 homval ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → B · op T ⁡ x = B ⋅ ℎ T ⁡ x
11 10 3expa ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → B · op T ⁡ x = B ⋅ ℎ T ⁡ x
12 11 3adantl1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → B · op T ⁡ x = B ⋅ ℎ T ⁡ x
13 9 12 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x + ℎ B · op T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
14 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
15 ax-hvdistr2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T ⁡ x ∈ ℋ → A + B ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
16 14 15 syl3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
17 16 3exp ⊢ A ∈ ℂ → B ∈ ℂ → T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
18 17 exp4a ⊢ A ∈ ℂ → B ∈ ℂ → T : ℋ ⟶ ℋ → x ∈ ℋ → A + B ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
19 18 3imp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B ⋅ ℎ T ⁡ x = A ⋅ ℎ T ⁡ x + ℎ B ⋅ ℎ T ⁡ x
20 13 19 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x + ℎ B · op T ⁡ x = A + B ⋅ ℎ T ⁡ x
21 6 20 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B · op T ⁡ x = A · op T ⁡ x + ℎ B · op T ⁡ x
22 homulcl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ
23 homulcl ⊢ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → B · op T : ℋ ⟶ ℋ
24 22 23 anim12i ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ ∧ B · op T : ℋ ⟶ ℋ
25 24 3impdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ ∧ B · op T : ℋ ⟶ ℋ
26 hosval ⊢ A · op T : ℋ ⟶ ℋ ∧ B · op T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T + op B · op T ⁡ x = A · op T ⁡ x + ℎ B · op T ⁡ x
27 26 3expa ⊢ A · op T : ℋ ⟶ ℋ ∧ B · op T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T + op B · op T ⁡ x = A · op T ⁡ x + ℎ B · op T ⁡ x
28 25 27 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T + op B · op T ⁡ x = A · op T ⁡ x + ℎ B · op T ⁡ x
29 21 28 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A + B · op T ⁡ x = A · op T + op B · op T ⁡ x
30 29 ralrimiva ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A + B · op T ⁡ x = A · op T + op B · op T ⁡ x
31 homulcl ⊢ A + B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A + B · op T : ℋ ⟶ ℋ
32 1 31 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A + B · op T : ℋ ⟶ ℋ
33 hoaddcl ⊢ A · op T : ℋ ⟶ ℋ ∧ B · op T : ℋ ⟶ ℋ → A · op T + op B · op T : ℋ ⟶ ℋ
34 22 23 33 syl2an ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T + op B · op T : ℋ ⟶ ℋ
35 34 3impdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T + op B · op T : ℋ ⟶ ℋ
36 hoeq ⊢ A + B · op T : ℋ ⟶ ℋ ∧ A · op T + op B · op T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A + B · op T ⁡ x = A · op T + op B · op T ⁡ x ↔ A + B · op T = A · op T + op B · op T
37 32 35 36 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ A + B · op T ⁡ x = A · op T + op B · op T ⁡ x ↔ A + B · op T = A · op T + op B · op T
38 30 37 mpbid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ T : ℋ ⟶ ℋ → A + B · op T = A · op T + op B · op T