Theorem ofmpteq

Description: Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014)

	Ref	Expression
Assertion	ofmpteq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f 𝑅 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → 𝐴 ∈ 𝑉 )
2		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
3		simpl2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	mptfng	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
6	3 5	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
7		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵
8	7	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V
9		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝐵 = ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
10	9	eleq1d	⊢ ( 𝑥 = 𝑎 → ( 𝐵 ∈ V ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V ) )
11	8 10	rspc	⊢ ( 𝑎 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V ) )
12	2 6 11	sylc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∈ V )
13		simpl3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
14		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
15	14	mptfng	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
16	13 15	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V )
17		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
18	17	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ V
19		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
20	19	eleq1d	⊢ ( 𝑥 = 𝑎 → ( 𝐶 ∈ V ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ V ) )
21	18 20	rspc	⊢ ( 𝑎 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ V ) )
22	2 16 21	sylc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ V )
23		nfcv	⊢ Ⅎ 𝑎 𝐵
24	23 7 9	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑎 ∈ 𝐴 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
25	24	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑎 ∈ 𝐴 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
26		nfcv	⊢ Ⅎ 𝑎 𝐶
27	26 17 19	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑎 ∈ 𝐴 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
28	27	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑎 ∈ 𝐴 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
29	1 12 22 25 28	offval2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f 𝑅 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 𝑅 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ) )
30		nfcv	⊢ Ⅎ 𝑎 ( 𝐵 𝑅 𝐶 )
31		nfcv	⊢ Ⅎ 𝑥 𝑅
32	7 31 17	nfov	⊢ Ⅎ 𝑥 ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 𝑅 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
33	9 19	oveq12d	⊢ ( 𝑥 = 𝑎 → ( 𝐵 𝑅 𝐶 ) = ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 𝑅 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
34	30 32 33	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 𝑅 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
35	29 34	eqtr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f 𝑅 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )