This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 ∘ 𝑇 ) ) )