Theorem ofval

Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Hypotheses	offval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offval.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	offval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offval.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	offval.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
	ofval.6	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
	ofval.7	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
Assertion	ofval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑋 ) = ( 𝐶 𝑅 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		offval.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		offval.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		offval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		offval.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		offval.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
6		ofval.6	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
7		ofval.7	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
8		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
10	1 2 3 4 5 8 9	offval	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑋 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑋 ) )
13		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
14		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
15	13 14	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
16		eqid	⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
17		ovex	⊢ ( ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) ∈ V
18	15 16 17	fvmpt	⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
20		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
21	5 20	eqsstrri	⊢ 𝑆 ⊆ 𝐴
22	21	sseli	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐴 )
23	22 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
24		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
25	5 24	eqsstrri	⊢ 𝑆 ⊆ 𝐵
26	25	sseli	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵 )
27	26 7	sylan2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
28	23 27	oveq12d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) = ( 𝐶 𝑅 𝐷 ) )
29	12 19 28	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑋 ) = ( 𝐶 𝑅 𝐷 ) )