Metamath Proof Explorer

Theorem caofass

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

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

Proof

Step Hyp Ref Expression
1 caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3 caofcom.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4 caofass.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
5 caofass.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) )
6 5 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) )
8 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
9 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
10 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 )
11 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) )
12 11 oveq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) 𝑇 𝑧 ) )
13 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( 𝑦 𝑃 𝑧 ) ) )
14 12 13 eqeq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( 𝑦 𝑃 𝑧 ) ) ) )
15 oveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
16 15 oveq1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 𝑧 ) )
17 oveq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( 𝑦 𝑃 𝑧 ) = ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) )
18 17 oveq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( 𝑦 𝑃 𝑧 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) 𝑇 𝑧 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( 𝑦 𝑃 𝑧 ) ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 𝑧 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) ) ) )
20 oveq2 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 𝑧 ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) )
21 oveq2 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) = ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) )
22 21 oveq2d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) )
23 20 22 eqeq12d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 𝑧 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 𝑧 ) ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) ) )
24 14 19 23 rspc3v ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) ) )
25 8 9 10 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ) 𝑇 𝑧 ) = ( 𝑥 𝑂 ( 𝑦 𝑃 𝑧 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) ) )
26 7 25 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) )
27 26 mpteq2dva ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) ) )
28 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ∈ V )
29 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) )
30 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
31 1 8 9 29 30 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) )
32 4 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑤 ) ) )
33 1 28 10 31 32 offval2 ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘f 𝑇 𝐻 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ) )
34 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ∈ V )
35 1 9 10 30 32 offval2 ⊢ ( 𝜑 → ( 𝐺 ∘f 𝑃 𝐻 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) )
36 1 8 34 29 35 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑂 ( 𝐺 ∘f 𝑃 𝐻 ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑂 ( ( 𝐺 ‘ 𝑤 ) 𝑃 ( 𝐻 ‘ 𝑤 ) ) ) ) )
37 27 33 36 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘f 𝑇 𝐻 ) = ( 𝐹 ∘f 𝑂 ( 𝐺 ∘f 𝑃 𝐻 ) ) )