Metamath Proof Explorer


Theorem fucco

Description: Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucco.q 𝑄 = ( 𝐶 FuncCat 𝐷 )
fucco.n 𝑁 = ( 𝐶 Nat 𝐷 )
fucco.a 𝐴 = ( Base ‘ 𝐶 )
fucco.o · = ( comp ‘ 𝐷 )
fucco.x = ( comp ‘ 𝑄 )
fucco.f ( 𝜑𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
fucco.g ( 𝜑𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
Assertion fucco ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 𝐻 ) 𝑅 ) = ( 𝑥𝐴 ↦ ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 fucco.q 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 fucco.n 𝑁 = ( 𝐶 Nat 𝐷 )
3 fucco.a 𝐴 = ( Base ‘ 𝐶 )
4 fucco.o · = ( comp ‘ 𝐷 )
5 fucco.x = ( comp ‘ 𝑄 )
6 fucco.f ( 𝜑𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
7 fucco.g ( 𝜑𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
8 eqid ( 𝐶 Func 𝐷 ) = ( 𝐶 Func 𝐷 )
9 2 natrcl ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
10 6 9 syl ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
11 10 simpld ( 𝜑𝐹 ∈ ( 𝐶 Func 𝐷 ) )
12 funcrcl ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
13 11 12 syl ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
14 13 simpld ( 𝜑𝐶 ∈ Cat )
15 13 simprd ( 𝜑𝐷 ∈ Cat )
16 1 8 2 3 4 14 15 5 fuccofval ( 𝜑 = ( 𝑣 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) , ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 𝑁 ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ) )
17 fvexd ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → ( 1st𝑣 ) ∈ V )
18 simprl ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ )
19 18 fveq2d ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → ( 1st𝑣 ) = ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
20 op1stg ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
21 10 20 syl ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
22 21 adantr ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
23 19 22 eqtrd ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → ( 1st𝑣 ) = 𝐹 )
24 fvexd ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd𝑣 ) ∈ V )
25 18 adantr ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ )
26 25 fveq2d ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd𝑣 ) = ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
27 op2ndg ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
28 10 27 syl ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
29 28 ad2antrr ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
30 26 29 eqtrd ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd𝑣 ) = 𝐺 )
31 simpr ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
32 simprr ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → = 𝐻 )
33 32 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → = 𝐻 )
34 31 33 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 𝑁 ) = ( 𝐺 𝑁 𝐻 ) )
35 simplr ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
36 35 31 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 𝑁 𝑔 ) = ( 𝐹 𝑁 𝐺 ) )
37 35 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st𝑓 ) = ( 1st𝐹 ) )
38 37 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st𝑓 ) ‘ 𝑥 ) = ( ( 1st𝐹 ) ‘ 𝑥 ) )
39 31 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st𝑔 ) = ( 1st𝐺 ) )
40 39 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st𝑔 ) ‘ 𝑥 ) = ( ( 1st𝐺 ) ‘ 𝑥 ) )
41 38 40 opeq12d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ )
42 33 fveq2d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 1st ) = ( 1st𝐻 ) )
43 42 fveq1d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 1st ) ‘ 𝑥 ) = ( ( 1st𝐻 ) ‘ 𝑥 ) )
44 41 43 oveq12d ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) = ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) )
45 44 oveqd ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) = ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) )
46 45 mpteq2dv ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) = ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) )
47 34 36 46 mpoeq123dv ( ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑏 ∈ ( 𝑔 𝑁 ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) )
48 24 30 47 csbied2 ( ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) ∧ 𝑓 = 𝐹 ) → ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 𝑁 ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) )
49 17 23 48 csbied2 ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝐹 , 𝐺 ⟩ ∧ = 𝐻 ) ) → ( 1st𝑣 ) / 𝑓 ( 2nd𝑣 ) / 𝑔 ( 𝑏 ∈ ( 𝑔 𝑁 ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝑓 ) ‘ 𝑥 ) , ( ( 1st𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1st ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) )
50 opelxpi ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) )
51 10 50 syl ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) )
52 2 natrcl ( 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
53 7 52 syl ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) )
54 53 simprd ( 𝜑𝐻 ∈ ( 𝐶 Func 𝐷 ) )
55 ovex ( 𝐺 𝑁 𝐻 ) ∈ V
56 ovex ( 𝐹 𝑁 𝐺 ) ∈ V
57 55 56 mpoex ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ V
58 57 a1i ( 𝜑 → ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) ∈ V )
59 16 49 51 54 58 ovmpod ( 𝜑 → ( ⟨ 𝐹 , 𝐺 𝐻 ) = ( 𝑏 ∈ ( 𝐺 𝑁 𝐻 ) , 𝑎 ∈ ( 𝐹 𝑁 𝐺 ) ↦ ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) ) )
60 simprl ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → 𝑏 = 𝑆 )
61 60 fveq1d ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → ( 𝑏𝑥 ) = ( 𝑆𝑥 ) )
62 simprr ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → 𝑎 = 𝑅 )
63 62 fveq1d ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → ( 𝑎𝑥 ) = ( 𝑅𝑥 ) )
64 61 63 oveq12d ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) = ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) )
65 64 mpteq2dv ( ( 𝜑 ∧ ( 𝑏 = 𝑆𝑎 = 𝑅 ) ) → ( 𝑥𝐴 ↦ ( ( 𝑏𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑎𝑥 ) ) ) = ( 𝑥𝐴 ↦ ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) )
66 3 fvexi 𝐴 ∈ V
67 66 mptex ( 𝑥𝐴 ↦ ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) ∈ V
68 67 a1i ( 𝜑 → ( 𝑥𝐴 ↦ ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) ∈ V )
69 59 65 7 6 68 ovmpod ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 𝐻 ) 𝑅 ) = ( 𝑥𝐴 ↦ ( ( 𝑆𝑥 ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑥 ) , ( ( 1st𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1st𝐻 ) ‘ 𝑥 ) ) ( 𝑅𝑥 ) ) ) )