ofres

Description: Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	ofres.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofres.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	ofres.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofres.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	ofres.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶
Assertion	ofres	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( ( 𝐹 ↾ 𝐶 ) ∘_f 𝑅 ( 𝐺 ↾ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofres.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		ofres.2	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3		ofres.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		ofres.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		ofres.5	⊢ ( 𝐴 ∩ 𝐵 ) = 𝐶
6		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
7		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
8	1 2 3 4 5 6 7	offval	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
9		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
10	5 9	eqsstrri	⊢ 𝐶 ⊆ 𝐴
11		fnssres	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
12	1 10 11	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
13		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
14	5 13	eqsstrri	⊢ 𝐶 ⊆ 𝐵
15		fnssres	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
16	2 14 15	sylancl	⊢ ( 𝜑 → ( 𝐺 ↾ 𝐶 ) Fn 𝐶 )
17		ssexg	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐶 ∈ V )
18	10 3 17	sylancr	⊢ ( 𝜑 → 𝐶 ∈ V )
19		inidm	⊢ ( 𝐶 ∩ 𝐶 ) = 𝐶
20		fvres	⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
22		fvres	⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐺 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐺 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
24	12 16 18 18 19 21 23	offval	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) ∘_f 𝑅 ( 𝐺 ↾ 𝐶 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
25	8 24	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( ( 𝐹 ↾ 𝐶 ) ∘_f 𝑅 ( 𝐺 ↾ 𝐶 ) ) )

Metamath Proof Explorer

Theorem ofres

Proof