This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )