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