This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofoprabco

Description: Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017)

Ref Expression
Hypotheses ofoprabco.1 ⊢ Ⅎ 𝑎 𝑀
ofoprabco.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
ofoprabco.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
ofoprabco.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ofoprabco.5 ⊢ ( 𝜑 → 𝑀 = ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) )
ofoprabco.6 ⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) )
Assertion ofoprabco ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑁 ∘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ofoprabco.1 ⊢ Ⅎ 𝑎 𝑀
2 ofoprabco.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 ofoprabco.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
4 ofoprabco.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 ofoprabco.5 ⊢ ( 𝜑 → 𝑀 = ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) )
6 ofoprabco.6 ⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) )
7 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
8 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐶 )
9 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑎 ) ∈ 𝐶 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
10 7 8 9 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
11 5 10 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑎 ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝑀 ‘ 𝑎 ) ) = ( 𝑁 ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) )
13 df-ov ⊢ ( ( 𝐹 ‘ 𝑎 ) 𝑁 ( 𝐺 ‘ 𝑎 ) ) = ( 𝑁 ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) 𝑁 ( 𝐺 ‘ 𝑎 ) ) = ( 𝑁 ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) )
16 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑎 ) ) ) → 𝑥 = ( 𝐹 ‘ 𝑎 ) )
17 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑎 ) ) ) → 𝑦 = ( 𝐺 ‘ 𝑎 ) )
18 16 17 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑎 ) ) ) → ( 𝑥 𝑅 𝑦 ) = ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) )
19 ovexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) ∈ V )
20 15 18 7 8 19 ovmpod ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) 𝑁 ( 𝐺 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) )
21 12 14 20 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑁 ‘ ( 𝑀 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) )
22 21 mpteq2dva ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝑀 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) ) )
23 ovex ⊢ ( 𝑥 𝑅 𝑦 ) ∈ V
24 23 rgen2w ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ) ∈ V
25 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) )
26 25 fmpo ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ) ∈ V ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) : ( 𝐵 × 𝐶 ) ⟶ V )
27 24 26 mpbi ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) : ( 𝐵 × 𝐶 ) ⟶ V
28 6 feq1d ⊢ ( 𝜑 → ( 𝑁 : ( 𝐵 × 𝐶 ) ⟶ V ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) : ( 𝐵 × 𝐶 ) ⟶ V ) )
29 27 28 mpbiri ⊢ ( 𝜑 → 𝑁 : ( 𝐵 × 𝐶 ) ⟶ V )
30 5 10 fmpt3d ⊢ ( 𝜑 → 𝑀 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) )
31 1 fcomptf ⊢ ( ( 𝑁 : ( 𝐵 × 𝐶 ) ⟶ V ∧ 𝑀 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) ) → ( 𝑁 ∘ 𝑀 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝑀 ‘ 𝑎 ) ) ) )
32 29 30 31 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑀 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑁 ‘ ( 𝑀 ‘ 𝑎 ) ) ) )
33 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
34 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑎 ) ) )
35 4 7 8 33 34 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐺 ‘ 𝑎 ) ) ) )
36 22 32 35 3eqtr4rd ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑁 ∘ 𝑀 ) )