Metamath Proof Explorer

Theorem caofdir

Description: Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses caofdi.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
caofdi.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐾 )
caofdi.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
caofdi.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
caofdir.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( 𝑥 𝑇 𝑧 ) 𝑂 ( 𝑦 𝑇 𝑧 ) ) )
Assertion caofdir ( 𝜑 → ( ( 𝐺 ∘f 𝑅 𝐻 ) ∘f 𝑇 𝐹 ) = ( ( 𝐺 ∘f 𝑇 𝐹 ) ∘f 𝑂 ( 𝐻 ∘f 𝑇 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 caofdi.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofdi.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐾 )
3 caofdi.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4 caofdi.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
5 caofdir.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( 𝑥 𝑇 𝑧 ) 𝑂 ( 𝑦 𝑇 𝑧 ) ) )
6 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( 𝑥 𝑇 𝑧 ) 𝑂 ( 𝑦 𝑇 𝑧 ) ) )
7 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
8 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 )
9 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐾 )
10 6 7 8 9 caovdird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) = ( ( ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) 𝑂 ( ( 𝐻 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) )
11 10 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) 𝑂 ( ( 𝐻 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) ) )
12 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) ∈ V )
13 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
14 4 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑤 ) ) )
15 1 7 8 13 14 offval2 ⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐻 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) ) )
16 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) )
17 1 12 9 15 16 offval2 ⊢ ( 𝜑 → ( ( 𝐺 ∘f 𝑅 𝐻 ) ∘f 𝑇 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐻 ‘ 𝑤 ) ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) )
18 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ∈ V )
19 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ∈ V )
20 1 7 9 13 16 offval2 ⊢ ( 𝜑 → ( 𝐺 ∘f 𝑇 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) )
21 1 8 9 14 16 offval2 ⊢ ( 𝜑 → ( 𝐻 ∘f 𝑇 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐻 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) )
22 1 18 19 20 21 offval2 ⊢ ( 𝜑 → ( ( 𝐺 ∘f 𝑇 𝐹 ) ∘f 𝑂 ( 𝐻 ∘f 𝑇 𝐹 ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) 𝑂 ( ( 𝐻 ‘ 𝑤 ) 𝑇 ( 𝐹 ‘ 𝑤 ) ) ) ) )
23 11 17 22 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐺 ∘f 𝑅 𝐻 ) ∘f 𝑇 𝐹 ) = ( ( 𝐺 ∘f 𝑇 𝐹 ) ∘f 𝑂 ( 𝐻 ∘f 𝑇 𝐹 ) ) )