# 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 ( 𝜑 → ( ( 𝐹𝑓 𝑅 𝐺 ) ∘𝑓 𝑇 𝐻 ) = ( 𝐹𝑓 𝑂 ( 𝐺𝑓 𝑃 𝐻 ) ) )

### 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 ( 𝜑 → ( 𝐹𝑓 𝑅 𝐺 ) = ( 𝑤𝐴 ↦ ( ( 𝐹𝑤 ) 𝑅 ( 𝐺𝑤 ) ) ) )
32 4 feqmptd ( 𝜑𝐻 = ( 𝑤𝐴 ↦ ( 𝐻𝑤 ) ) )
33 1 28 10 31 32 offval2 ( 𝜑 → ( ( 𝐹𝑓 𝑅 𝐺 ) ∘𝑓 𝑇 𝐻 ) = ( 𝑤𝐴 ↦ ( ( ( 𝐹𝑤 ) 𝑅 ( 𝐺𝑤 ) ) 𝑇 ( 𝐻𝑤 ) ) ) )
34 ovexd ( ( 𝜑𝑤𝐴 ) → ( ( 𝐺𝑤 ) 𝑃 ( 𝐻𝑤 ) ) ∈ V )
35 1 9 10 30 32 offval2 ( 𝜑 → ( 𝐺𝑓 𝑃 𝐻 ) = ( 𝑤𝐴 ↦ ( ( 𝐺𝑤 ) 𝑃 ( 𝐻𝑤 ) ) ) )
36 1 8 34 29 35 offval2 ( 𝜑 → ( 𝐹𝑓 𝑂 ( 𝐺𝑓 𝑃 𝐻 ) ) = ( 𝑤𝐴 ↦ ( ( 𝐹𝑤 ) 𝑂 ( ( 𝐺𝑤 ) 𝑃 ( 𝐻𝑤 ) ) ) ) )
37 27 33 36 3eqtr4d ( 𝜑 → ( ( 𝐹𝑓 𝑅 𝐺 ) ∘𝑓 𝑇 𝐻 ) = ( 𝐹𝑓 𝑂 ( 𝐺𝑓 𝑃 𝐻 ) ) )