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

Metamath Proof Explorer

Theorem offval2f

Description: The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 offval2f.0 ⊢ Ⅎ 𝑥 𝜑
2 offval2f.a ⊢ Ⅎ 𝑥 𝐴
3 offval2f.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 offval2f.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 offval2f.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
6 offval2f.4 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
7 offval2f.5 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
8 4 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑊 ) )
9 1 8 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
10 2 fnmptf ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
11 9 10 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
12 6 fneq1d ⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) )
13 11 12 mpbird ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
14 5 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋 ) )
15 1 14 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 )
16 2 fnmptf ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝑋 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
17 15 16 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
18 7 fneq1d ⊢ ( 𝜑 → ( 𝐺 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) )
19 17 18 mpbird ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
20 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
21 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22 21 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
24 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
25 13 19 3 3 20 22 24 offval ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) )
26 nfcv ⊢ Ⅎ 𝑦 𝐴
27 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
28 nfcv ⊢ Ⅎ 𝑥 𝑅
29 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
30 27 28 29 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) )
31 nfcv ⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
32 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
33 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
34 32 33 oveq12d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
35 26 2 30 31 34 cbvmptf ⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
37 2 fvmpt2f ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
38 36 4 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
39 2 fvmpt2f ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
40 36 5 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
41 38 40 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) = ( 𝐵 𝑅 𝐶 ) )
42 1 41 mpteq2da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
43 35 42 eqtrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
44 25 43 eqtrd ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )