# 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 ( 𝑅𝑇 ) ) )
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://metamath.tirix.org/mpeuni/hoddi", "fetch_time": 1718969828000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-26/segments/1718198862070.5/warc/CC-MAIN-20240621093735-20240621123735-00686.warc.gz", "warc_record_offset": 23475702, "warc_record_length": 2614, "token_count": 2534, "char_count": 3930, "score": 3.5, "int_score": 4, "crawl": "CC-MAIN-2024-26", "snapshot_type": "latest", "language": "en", "language_score": 0.1517561674118042, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00003-of-00064.parquet"}