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

Metamath Proof Explorer

Theorem uncfval

Description: Value of the uncurry functor, which is the reverse of the curry functor, taking G : C --> ( D --> E ) to uncurryF ( G ) : C X. D --> E . (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfval.g ⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
uncfval.c ⊢ ( 𝜑 → 𝐷 ∈ Cat )
uncfval.d ⊢ ( 𝜑 → 𝐸 ∈ Cat )
uncfval.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
Assertion uncfval ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 uncfval.g ⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
2 uncfval.c ⊢ ( 𝜑 → 𝐷 ∈ Cat )
3 uncfval.d ⊢ ( 𝜑 → 𝐸 ∈ Cat )
4 uncfval.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
5 df-uncf ⊢ uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) )
6 5 a1i ⊢ ( 𝜑 → uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) ) )
7 simprl ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ )
8 7 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 1 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) )
9 s3fv1 ⊢ ( 𝐷 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
10 2 9 syl ⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
12 8 11 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 1 ) = 𝐷 )
13 7 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 2 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) )
14 s3fv2 ⊢ ( 𝐸 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
15 3 14 syl ⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
17 13 16 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 2 ) = 𝐸 )
18 12 17 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) = ( 𝐷 evalF 𝐸 ) )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → 𝑓 = 𝐺 )
20 7 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 0 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) )
21 funcrcl ⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
22 4 21 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
23 22 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
24 s3fv0 ⊢ ( 𝐶 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
25 23 24 syl ⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
27 20 26 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 0 ) = 𝐶 )
28 27 12 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) = ( 𝐶 1stF 𝐷 ) )
29 19 28 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) = ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) )
30 27 12 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) = ( 𝐶 2ndF 𝐷 ) )
31 29 30 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) = ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) )
32 18 31 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )
33 s3cli ⊢ ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ Word V
34 elex ⊢ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ Word V → ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ V )
35 33 34 mp1i ⊢ ( 𝜑 → ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ V )
36 4 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
37 ovexd ⊢ ( 𝜑 → ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) ∈ V )
38 6 32 35 36 37 ovmpod ⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )
39 1 38 eqtrid ⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )