Metamath Proof Explorer

Theorem hodsi

Description: Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hods.1 ⊢ 𝑅 : ℋ ⟶ ℋ
hods.2 ⊢ 𝑆 : ℋ ⟶ ℋ
hods.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hodsi ( ( 𝑅 −op 𝑆 ) = 𝑇 ↔ ( 𝑆 +op 𝑇 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 hods.1 ⊢ 𝑅 : ℋ ⟶ ℋ
2 hods.2 ⊢ 𝑆 : ℋ ⟶ ℋ
3 hods.3 ⊢ 𝑇 : ℋ ⟶ ℋ
4 1 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑅 ‘ 𝑥 ) ∈ ℋ )
5 2 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
6 3 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
7 hvsubadd ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( ( 𝑅 ‘ 𝑥 ) −ℎ ( 𝑆 ‘ 𝑥 ) ) = ( 𝑇 ‘ 𝑥 ) ↔ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) ) )
8 4 5 6 7 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 ‘ 𝑥 ) −ℎ ( 𝑆 ‘ 𝑥 ) ) = ( 𝑇 ‘ 𝑥 ) ↔ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) ) )
9 hodval ⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) −ℎ ( 𝑆 ‘ 𝑥 ) ) )
10 1 2 9 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) −ℎ ( 𝑆 ‘ 𝑥 ) ) )
11 10 eqeq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( ( 𝑅 ‘ 𝑥 ) −ℎ ( 𝑆 ‘ 𝑥 ) ) = ( 𝑇 ‘ 𝑥 ) ) )
12 hosval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
13 2 3 12 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
14 13 eqeq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) ↔ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑅 ‘ 𝑥 ) ) )
15 8 11 14 3bitr4d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) ) )
16 15 ralbiia ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
17 1 2 hosubcli ⊢ ( 𝑅 −op 𝑆 ) : ℋ ⟶ ℋ
18 17 3 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑅 −op 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( 𝑅 −op 𝑆 ) = 𝑇 )
19 2 3 hoaddcli ⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
20 19 1 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) ↔ ( 𝑆 +op 𝑇 ) = 𝑅 )
21 16 18 20 3bitr3i ⊢ ( ( 𝑅 −op 𝑆 ) = 𝑇 ↔ ( 𝑆 +op 𝑇 ) = 𝑅 )