offval2

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		offval2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offval2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3		offval2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
4		offval2.4	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
5		offval2.5	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
6	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
7		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8	7	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
9	6 8	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
10	4	fneq1d	⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) )
11	9 10	mpbird	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
12	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 )
13		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
14	13	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
15	12 14	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
16	5	fneq1d	⊢ ( 𝜑 → ( 𝐺 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) )
17	15 16	mpbird	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
18		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
20	19	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
21	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
22	21	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
23	11 17 1 1 18 20 22	offval	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
24		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
25		nfcv	⊢ Ⅎ 𝑥 𝑅
26		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
27	24 25 26	nfov	⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
28		nfcv	⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
29		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
30		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
31	29 30	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
32	27 28 31	cbvmpt	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
33		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
34	7	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
35	33 2 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
36	13	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
37	33 3 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
38	35 37	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) = ( 𝐵 𝑅 𝐶 ) )
39	38	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
40	32 39	syl5eq	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
41	23 40	eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

Metamath Proof Explorer

Theorem offval2

Proof