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 𝑅 𝐺 ) = ( 𝑁 ∘ 𝑀 ) )

Metamath Proof Explorer

Theorem ofoprabco

Proof