Metamath Proof Explorer

Theorem caofdi

Description: Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014)

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

Proof

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