Theorem offval2f

Description: The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017)

	Ref	Expression
Hypotheses	offval2f.0	⊢ Ⅎ 𝑥 𝜑
	offval2f.a	⊢ Ⅎ 𝑥 𝐴
	offval2f.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offval2f.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
	offval2f.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
	offval2f.4	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
	offval2f.5	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
Assertion	offval2f	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		offval2f.0	⊢ Ⅎ 𝑥 𝜑
2		offval2f.a	⊢ Ⅎ 𝑥 𝐴
3		offval2f.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		offval2f.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5		offval2f.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
6		offval2f.4	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
7		offval2f.5	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
8	4	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑊 ) )
9	1 8	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
10	2	fnmptf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
11	9 10	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
12	6	fneq1d	⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) )
13	11 12	mpbird	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
14	5	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋 ) )
15	1 14	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 )
16	2	fnmptf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
17	15 16	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
18	7	fneq1d	⊢ ( 𝜑 → ( 𝐺 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) )
19	17 18	mpbird	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
20		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
21	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22	21	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
23	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
24	23	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
25	13 19 3 3 20 22 24	offval	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
26		nfcv	⊢ Ⅎ 𝑦 𝐴
27		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
28		nfcv	⊢ Ⅎ 𝑥 𝑅
29		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
30	27 28 29	nfov	⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
31		nfcv	⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
32		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
33		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
34	32 33	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
35	26 2 30 31 34	cbvmptf	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
36		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
37	2	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
38	36 4 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
39	2	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
40	36 5 39	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
41	38 40	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) = ( 𝐵 𝑅 𝐶 ) )
42	1 41	mpteq2da	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
43	35 42	eqtrid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
44	25 43	eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )