Metamath Proof Explorer

Theorem hosub4

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosub4 ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) −op ( 𝑇 +op 𝑈 ) ) = ( ( 𝑅 −op 𝑇 ) +op ( 𝑆 −op 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 honegdi ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) )
2 1 adantl ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) )
3 2 oveq2d ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) +op ( - 1 ·op ( 𝑇 +op 𝑈 ) ) ) = ( ( 𝑅 +op 𝑆 ) +op ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) )
4 neg1cn ⊢ - 1 ∈ ℂ
5 homulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
6 4 5 mpan ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
7 homulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
8 4 7 mpan ⊢ ( 𝑈 : ℋ ⟶ ℋ → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
9 6 8 anim12i ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ ) )
10 hoadd4 ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( ( - 1 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) +op ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) = ( ( 𝑅 +op ( - 1 ·op 𝑇 ) ) +op ( 𝑆 +op ( - 1 ·op 𝑈 ) ) ) )
11 9 10 sylan2 ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) +op ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) = ( ( 𝑅 +op ( - 1 ·op 𝑇 ) ) +op ( 𝑆 +op ( - 1 ·op 𝑈 ) ) ) )
12 3 11 eqtrd ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) +op ( - 1 ·op ( 𝑇 +op 𝑈 ) ) ) = ( ( 𝑅 +op ( - 1 ·op 𝑇 ) ) +op ( 𝑆 +op ( - 1 ·op 𝑈 ) ) ) )
13 hoaddcl ⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( 𝑅 +op 𝑆 ) : ℋ ⟶ ℋ )
14 hoaddcl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op 𝑈 ) : ℋ ⟶ ℋ )
15 honegsub ⊢ ( ( ( 𝑅 +op 𝑆 ) : ℋ ⟶ ℋ ∧ ( 𝑇 +op 𝑈 ) : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑆 ) +op ( - 1 ·op ( 𝑇 +op 𝑈 ) ) ) = ( ( 𝑅 +op 𝑆 ) −op ( 𝑇 +op 𝑈 ) ) )
16 13 14 15 syl2an ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) +op ( - 1 ·op ( 𝑇 +op 𝑈 ) ) ) = ( ( 𝑅 +op 𝑆 ) −op ( 𝑇 +op 𝑈 ) ) )
17 honegsub ⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑅 +op ( - 1 ·op 𝑇 ) ) = ( 𝑅 −op 𝑇 ) )
18 17 ad2ant2r ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( 𝑅 +op ( - 1 ·op 𝑇 ) ) = ( 𝑅 −op 𝑇 ) )
19 honegsub ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( - 1 ·op 𝑈 ) ) = ( 𝑆 −op 𝑈 ) )
20 19 ad2ant2l ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( 𝑆 +op ( - 1 ·op 𝑈 ) ) = ( 𝑆 −op 𝑈 ) )
21 18 20 oveq12d ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op ( - 1 ·op 𝑇 ) ) +op ( 𝑆 +op ( - 1 ·op 𝑈 ) ) ) = ( ( 𝑅 −op 𝑇 ) +op ( 𝑆 −op 𝑈 ) ) )
22 12 16 21 3eqtr3d ⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑆 ) −op ( 𝑇 +op 𝑈 ) ) = ( ( 𝑅 −op 𝑇 ) +op ( 𝑆 −op 𝑈 ) ) )