# Metamath Proof Explorer

## Theorem hoddi

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoddi ( ( 𝑅 ∈ LinOp ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑅 ∘ ( 𝑆op 𝑇 ) ) = ( ( 𝑅𝑆 ) −op ( 𝑅𝑇 ) ) )

### Proof

Step Hyp Ref Expression
1 coeq1 ( 𝑅 = if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) → ( 𝑅 ∘ ( 𝑆op 𝑇 ) ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( 𝑆op 𝑇 ) ) )
2 coeq1 ( 𝑅 = if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) → ( 𝑅𝑆 ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) )
3 coeq1 ( 𝑅 = if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) → ( 𝑅𝑇 ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) )
4 2 3 oveq12d ( 𝑅 = if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) → ( ( 𝑅𝑆 ) −op ( 𝑅𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) )
5 1 4 eqeq12d ( 𝑅 = if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) → ( ( 𝑅 ∘ ( 𝑆op 𝑇 ) ) = ( ( 𝑅𝑆 ) −op ( 𝑅𝑇 ) ) ↔ ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( 𝑆op 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) ) )
6 oveq1 ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( 𝑆op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) )
7 6 coeq2d ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( 𝑆op 𝑇 ) ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) ) )
8 coeq2 ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) )
9 8 oveq1d ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) )
10 7 9 eqeq12d ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( 𝑆op 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑆 ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) ↔ ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) ) )
11 oveq2 ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
12 11 coeq2d ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) )
13 coeq2 ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) = ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
14 13 oveq2d ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) )
15 12 14 eqeq12d ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op 𝑇 ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ 𝑇 ) ) ↔ ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) ) )
16 0lnop 0hop ∈ LinOp
17 16 elimel if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∈ LinOp
18 ho0f 0hop : ℋ ⟶ ℋ
19 18 elimf if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) : ℋ ⟶ ℋ
20 18 elimf if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) : ℋ ⟶ ℋ
21 17 19 20 hoddii ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) −op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) ) = ( ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) −op ( if ( 𝑅 ∈ LinOp , 𝑅 , 0hop ) ∘ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
22 5 10 15 21 dedth3h ( ( 𝑅 ∈ LinOp ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑅 ∘ ( 𝑆op 𝑇 ) ) = ( ( 𝑅𝑆 ) −op ( 𝑅𝑇 ) ) )