Pensieve header: Double Integration.

Startup

SetDirectory["C:\\drorbn\\AcademicPensieve\\People\\Frohlich"];
(Subscript[PP, _]):=Identity;
<<"../../Projects/SL2Portfolio2/Engine-Speedy.m";
<<"../../Projects/SL2Portfolio2/Objects.m";
$k=1;
HL[ℰ_] := Style[ℰ, Background -> Green];

(Subscript[(OverBar[R]), 3,4])

(Subscript[P, 1,2])

(Subscript[(OverBar[R]), 3,4])//(Subscript[P, 4,3])

{
int=((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]*(Subscript[(OverBar[R]), 3,4]))//(Subscript[bm, 3,1->1])//(Subscript[am, 4,2->2])//(Subscript[P, 1,2]),
 (Subscript[dΔ, i->i,j])//int
} // Column

(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])

Block[{$k=1},Module[
{RR=(Subscript[R, 3,4]),AM=(Subscript[am, 2,4->2]),BM=(Subscript[bm, 3,1->1])},
{
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
),
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->j,i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
),
HL[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint]
}]] // Column

Block[{$k=1},Table[
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->j,i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
Echo@HL@TrueQ[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint],
{RR,{(*(Subscript[R, 3,4]),*)(Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])(*,(Subscript[R, 3,4])//(Subscript[dS, 3])//(Subscript[dS, 3])*)}},{AM,{(Subscript[am, 2,4->2])(*,(Subscript[am, 4,2->2])*)}},{BM,{(*(Subscript[bm, 1,3->1]),*)(Subscript[bm, 3,1->1])}}
]]

Block[{$k=1},Table[
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->j,i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
Echo@HL@TrueQ[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint],
{RR,{(*(Subscript[R, 3,4]),*)(Subscript[R, 3,4])//(Subscript[bS, 3])//(Subscript[bS, 3])}},{AM,{(Subscript[am, 2,4->2]),(Subscript[am, 2,4->2])}},{BM,{(*(Subscript[bm, 1,3->1]),*)(Subscript[bm, 3,1->1])}}
]]

Dimensions[{{{Style[False,Background->RGBColor[0,1,0]],Style[True,Background->RGBColor[0,1,0]]}},{{Style[False,Background->RGBColor[0,1,0]],Style[False,Background->RGBColor[0,1,0]]}}}]

((Subscript[(OverBar[R]), 3,4])//(Subscript[bS, 3]))≡((Subscript[R, 3,4])//(Subscript[bS, 3])//(Subscript[bS, 3]))

Block[{$k=0},Table[
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->i,j])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
Echo@HL@TrueQ[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint],
{RR,{(*(Subscript[R, 3,4]),*)(Subscript[R, 3,4])//(Subscript[bS, 3])//(Subscript[bS, 3]),(Subscript[R, 3,4])//(Subscript[(OverBar[bS]), 3])//(Subscript[(OverBar[bS]), 3]),(Subscript[R, 3,4])//(Subscript[aS, 4])//(Subscript[aS, 4]),(Subscript[R, 3,4])//(Subscript[(OverBar[aS]), 4])//(Subscript[(OverBar[aS]), 4])}},{AM,{(*(Subscript[am, 2,4->2]),*)(Subscript[am, 2,4->2])}},{BM,{(Subscript[bm, 1,3->1]),(Subscript[bm, 3,1->1])}}
]]

The following verifies ∫ϕ⊗x = (Subscript[x, 1])∫ϕ⊗(Subscript[x, 2]) in this case:

n=0;While[ n ≤1,
Block[{$k=n},
steps=Simplify /@{
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]), (* Integral *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[dΔ, 2->2,3])//(Subscript[dΔ, 3->3,4])//(Subscript[dS, 3])//(Subscript[dm, 2,3->2])//(Subscript[P, 1,4])//(Subscript[dm, 2,j->j]), (* Antipode axiom *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[dΔ, 2->2,3])//(Subscript[dΔ, 3->3,4])//(Subscript[R, b1,b2])//(Subscript[dS, b2])//(Subscript[dm, 2,b2->2])//(Subscript[P, b1,3])//(Subscript[P, 1,4])//(Subscript[dm, 2,j->j]), (* R=Id *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[dΔ, 2->2,3])//(Subscript[R, b1,b2])//(Subscript[dS, b2])//(Subscript[dm, b1,1->1])//(Subscript[dm, 2,b2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Pairing axiom *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dΔ, 4->(Subscript[4, 1]),(Subscript[4, 2])])//(Subscript[am, (Subscript[2, 1]),(Subscript[4, 1])->2])//(Subscript[dm, (Subscript[2, 2]),(Subscript[4, 2])->3])
//(Subscript[R, b1,b2])//(Subscript[dS, b2])//(Subscript[dm, b1,1->1])//(Subscript[dm, 2,b2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Bialgebra *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])
//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dΔ, 4->(Subscript[4, 1]),(Subscript[4, 2])])//(Subscript[dS, (Subscript[4, 1])])//(Subscript[dS, (Subscript[4, 1])])//(Subscript[dS, (Subscript[4, 2])])//(Subscript[dS, (Subscript[4, 2])])//(Subscript[am, (Subscript[2, 1]),(Subscript[4, 1])->2])//(Subscript[dm, (Subscript[2, 2]),(Subscript[4, 2])->3])
//(Subscript[R, b1,b2])//(Subscript[dS, b2])//(Subscript[dm, b1,1->1])//(Subscript[dm, 2,b2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Antipode anticohomomorphism *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[R, a1,a2])//(Subscript[dm, a1,3->3])
//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dS, a2])//(Subscript[dS, a2])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[am, (Subscript[2, 1]),a2->2])//(Subscript[dm, (Subscript[2, 2]),4->3])
//(Subscript[R, b1,b2])//(Subscript[dS, b2])//(Subscript[dm, b1,1->1])//(Subscript[dm, 2,b2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Quasitriangularity axiom *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[R, a1,a2])//(Subscript[dm, a1,3->3])
//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dS, a2])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[dm, (Subscript[2, 2]),4->3])
//(Subscript[R, b1,b2])//(Subscript[dm, b1,1->1])//(Subscript[am, b2,a2->2])//(Subscript[dS, 2])//(Subscript[dm, (Subscript[2, 1]),2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Antipode antihomomorphism *) (* $k=2 passes up to here *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]
//(Subscript[R, 3,4])//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[dm, (Subscript[2, 2]),4->3])(Subscript[𝔼, {}->{2}])[0,0,1]//(Subscript[dS, 2])//(Subscript[dm, (Subscript[2, 1]),2->2])//(Subscript[P, 1,3])//(Subscript[dm, 2,j->j]), (* Reidemeister 2 *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]
//(Subscript[R, 3,4])//(Subscript[bm, 3,1->1])//(Subscript[dΔ, 2->(Subscript[2, 1]),(Subscript[2, 2])])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[dm, (Subscript[2, 2]),4->3])//(Subscript[P, 1,3])//(Subscript[dm, (Subscript[2, 1]),j->j]) ,(* Antipode is unital *)
(*(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//
 (Subscript[dΔ, i->j,i])
//(Subscript[𝔼, {j}->{j}])[2(Subscript[α, j])(Subscript[a, j]),(Subscript[ξ, j])(Subscript[x, j]),1] (* Why does this term not affect anything? One can even remove it. *)
//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]), (* Integral with comultiplicaion *)*)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 2->j,2])
//(Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]) (* Integral with comultiplicaion *)
};
(*Echo[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]]];*)
If[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]],
Echo["$k="<>ToString[n]<> " passes."],
Echo["$k="<>ToString[n]<> " fails."];
Table[Echo@HL[steps[[$i]]],{$i,Length[steps]}];
Break[]
];n++]
]

The following (will) verify ∫ϕ⊗x = (Subscript[ϕ, 1])∫(Subscript[ϕ, 2])⊗x in this case:

n=0;While[ n ≤1,
Block[{$k=n},
steps=Simplify /@{
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 1->j,1])//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]), (* Integral with comultiplicaion *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 1->j,1])//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[R, a1,a2])//(Subscript[(OverBar[dS]), a1])//(Subscript[R, b1,b2])//(Subscript[am, 2,a2->2])//(Subscript[am, 2,b2->2])//(Subscript[bm, a1,b1->ab])//(Subscript[bm, ab,j->j])//(Subscript[P, 1,2]), (* Reidemeister 2 *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 1->j,1])
//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[R, a1,a2])//(Subscript[(OverBar[dS]), a1])//(Subscript[R, b1,b2])//(Subscript[am, 2,a2->2])//(Subscript[am, 2,b2->2])//(Subscript[bm, a1,b1->ab])//(Subscript[(OverBar[dS]), ab])//(Subscript[am, ab,j->j])
//(Subscript[P, 1,2]), (* Antipode is unital *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 1->j,1])
//(Subscript[R, 3,4])//(Subscript[dΔ, 3->(Subscript[3, 1]),(Subscript[3, 2])])//(Subscript[(OverBar[dS]), (Subscript[3, 2])])//(Subscript[(OverBar[dS]), (Subscript[3, 2])])//(Subscript[bm, (Subscript[3, 2]),1->1])//(Subscript[(OverBar[dS]), (Subscript[3, 1])])//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[am, 2,b2->2])//(Subscript[bm, (Subscript[3, 1]),b1->ab])//(Subscript[(OverBar[dS]), ab])//(Subscript[am, ab,j->j])
//(Subscript[P, 1,2]), (* R-matrix and strand doubling *)
(*(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[dΔ, 1->j,1])
//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[dΔ, 3->(Subscript[3, 1]),(Subscript[3, 2])])//(Subscript[bm, (Subscript[3, 2]),1->1])//(Subscript[(OverBar[dS]), (Subscript[3, 1])])//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[am, 2,b2->2])//(Subscript[am, (Subscript[3, 1]),b1->ab])//(Subscript[(OverBar[dS]), ab])//(Subscript[am, ab,j->j])
//(Subscript[P, 1,2]), (* THIS LOOKS WRONG YET THIS ROUTINE FINDS NO FAULT *)*)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]
//(Subscript[dΔ, 1->j,1])//(Subscript[R, 3,4])//(Subscript[dΔ, 3->(Subscript[3, 1]),(Subscript[3, 2])])//(Subscript[(OverBar[dS]), (Subscript[3, 2])])//(Subscript[(OverBar[dS]), (Subscript[3, 2])])//(Subscript[bm, (Subscript[3, 2]),1->1])//(Subscript[(OverBar[dS]), (Subscript[3, 1])])//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[am, 2,b2->2])//(Subscript[(OverBar[dS]), (Subscript[3, 1])])//(Subscript[(OverBar[dS]), b1])//(Subscript[dm, b1,(Subscript[3, 1])->ab])//(Subscript[dm, ab,j->j])//(Subscript[P, 1,2]), (* (OverBar[dS]) is antimorphism *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]
//(Subscript[dΔ, 1->j,1])//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[dΔ, 3->(Subscript[3, 1]),(Subscript[3, 2])])//(Subscript[bm, (Subscript[3, 2]),1->1])//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[am, 2,b2->2])//(Subscript[(OverBar[dS]), b1])//(Subscript[dm, b1,(Subscript[3, 1])->ab])//(Subscript[dm, ab,j->j])//(Subscript[P, 1,2]), (* ((OverBar[dS])^2) is coalgebra morphism *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])
//(Subscript[dΔ, 1->j,1])//(Subscript[dΔ, 3->(Subscript[3, 1]),(Subscript[3, 2])])//(Subscript[bm, (Subscript[3, 2]),1->1])//(Subscript[bm, (Subscript[3, 1]),j->j])
//(Subscript[dm, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[dm, 2,b2->2])//(Subscript[(OverBar[dS]), b1])//(Subscript[dm, b1,j->j])//(Subscript[P, 1,2]), (* [re-arrangement of commuting terms] *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[dm, 3,1->j])//(Subscript[dΔ, j->j,1])
//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[(OverBar[dS]), b1])//(Subscript[bm, b1,j->j])//(Subscript[am, 2,b2->2])//(Subscript[P, 1,2]), (* Δ is m-morphism *) (* ERROR: One of 2, b2 have B-algebra factors?? *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[dm, 3,1->j])//(Subscript[dΔ, j->j,1])
//(Subscript[am, 2,4->2])//(Subscript[R, b1,b2])//(Subscript[(OverBar[dS]), b1])//(Subscript[bm, b1,j->j])//(Subscript[bΔ, 1->(Subscript[1, 1]),(Subscript[1, 2])])//(Subscript[P, (Subscript[1, 2]),2])//(Subscript[P, (Subscript[1, 1]),b2]), (* Pairing with (co)multiplication *)
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])))
//(Subscript[dm, 3,1->1])//(Subscript[dm, 2,4->2])//(Subscript[P, 1,2]) (* Integral *)
};
(*Echo[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]]];*)
If[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]],
Echo["$k="<>ToString[n]<> " passes."],
Echo["$k="<>ToString[n]<> " fails."];
Table[Echo@HL[steps[[$i]]],{$i,Length[steps]}];
Break[]
];n++]
]

WARNING : "am" and "bm" are used in the wrong places above. Take care to replace them with “dm”, and do be smart about such transformations.

The following verifies ∫ϕ⊗x=(Subscript[ϕ, 1])⊗(Subscript[x, 1])∫(Subscript[ϕ, 2])⊗(Subscript[x, 2])  (this should follow from the above two proofs, the second of which I cannot quite get):

n=0;While[ n ≤1,
Block[{$k=n},
steps=Simplify /@{
(Subscript[𝔼, {}->{1,j}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]((Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4])))
//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]), (* Integral *)
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//(Subscript[dΔ, i->j,i])//(Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]
//(Subscript[R, 3,4])//(Subscript[(OverBar[dS]), 3])//(Subscript[(OverBar[dS]), 3])//(Subscript[bm, 3,1->1])//(Subscript[am, 2,4->2])//(Subscript[P, 1,2]) (* Integral with comultiplicaion *)
};
(*Echo[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]]];*)
If[TrueQ[And@@Table[steps[[$i]]≡steps[[$i+1]],{$i,Length[steps]-1}]],
Echo["$k="<>ToString[n]<> " passes."],
Echo["$k="<>ToString[n]<> " fails."];
Table[Echo@HL[steps[[$i]]],{$i,Length[steps]}];
Break[],
Echo["Other error."]
];n++]
]

Tests for the R-matrix:

((Subscript[R, a1,a2])//(Subscript[R, b1,b2])//(Subscript[(OverBar[dS]), a1])//(Subscript[am, i2,a2->i2])//(Subscript[am, i2,b2->i2])//(Subscript[bm, i1,a1->i1])//(Subscript[bm, i1,b1->i1]))≡((Subscript[𝔼, {i1,i2}->{i1,i2}])[(Subscript[a, i2]) (Subscript[α, i2])+(Subscript[b, i1]) (Subscript[β, i1]),(Subscript[y, i1]) (Subscript[η, i1])+(Subscript[x, i2]) (Subscript[ξ, i2]),1])

((Subscript[R, 1,4])//(Subscript[R, 2,3])//(Subscript[(OverBar[dS]), 3])//(Subscript[dm, 1,2->1])//(Subscript[dm, 3,4->2]))≡((Subscript[𝔼, {}->{1,2}])[0,0,1])

((Subscript[R, 1,4])//(Subscript[R, 2,3])//(Subscript[(OverBar[dS]), 4])//(Subscript[dm, 1,2->1])//(Subscript[dm, 3,4->2]))≡((Subscript[𝔼, {}->{1,2}])[0,0,1])

((Subscript[R, 1,4])//(Subscript[R, 2,3])//(Subscript[dS, 1])//(Subscript[dm, 1,2->1])//(Subscript[dm, 3,4->2]))≡((Subscript[𝔼, {}->{1,2}])[0,0,1])

((Subscript[R, 1,4])//(Subscript[R, 2,3])//(Subscript[dS, 2])//(Subscript[dm, 1,2->1])//(Subscript[dm, 3,4->2]))≡((Subscript[𝔼, {}->{1,2}])[0,0,1])

(Subscript[R, a1,a2])//(Subscript[R, b1,b2])//(Subscript[dS, a2])//(Subscript[dm, b2,a2->2])//(Subscript[dS, 1])//(Subscript[dm, b1,a1->1])

((Subscript[R, a1,a2])//(Subscript[R, 1,2])//(Subscript[dm, a1,1->1]))≡((Subscript[R, 1,2])//(Subscript[dΔ, 2->a2,2]))

((Subscript[R, a1,a2])//(Subscript[R, 1,2])//(Subscript[dm, a2,2->2]))≡((Subscript[R, 1,2])//(Subscript[dΔ, 1->1,a1]))

((Subscript[R, 1,2])//(Subscript[(OverBar[bS]), 1])//(Subscript[P, 1,i]))≡((Subscript[(OverBar[aS]), i])//(Subscript[𝔼, {i}->{2}])[(Subscript[a, 2]) (Subscript[α, i]),(Subscript[x, 2]) (Subscript[ξ, i]),1])

{((Subscript[R, 1,2])//(Subscript[(OverBar[bS]), 1])//(Subscript[P, i,2]))≡(((Subscript[(OverBar[bS]), i]))//(Subscript[𝔼, {i}->{1}])[(Subscript[b, 1])(Subscript[β, i]),(Subscript[y, 1])(Subscript[η, i]),1])}

(Subscript[(OverBar[R]), 1,2])≡((Subscript[R, 1,2])//(Subscript[aS, 2]))

((Subscript[(OverBar[dS]), 1])//(Subscript[(OverBar[dS]), 2])//(Subscript[dm, 1,2->1]))≡((Subscript[dm, 2,1->1])//(Subscript[(OverBar[dS]), 1]))

{((Subscript[dΔ, 1->1,2])//(Subscript[(OverBar[dS]), 1])//(Subscript[(OverBar[dS]), 2])),((Subscript[(OverBar[dS]), 1])//(Subscript[dΔ, 1->2,1]))}

(Subscript[dΔ, i->j,k])//(Subscript[𝔼, {j}->{j}])[((Subscript[a, j]))(Subscript[α, j]),((Subscript[x, j])) (Subscript[ξ, j]),1]

(Subscript[dΔ, i->j,k])//(Subscript[(OverBar[dS]), j])//(Subscript[dm, k,j->i])

Finding the right integral (no pun intended)

We begin with the naïve guess that the left integral we have found is also a right integral, and also checking the rest of the options:

Block[{$k=0},Table[
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->i,j])//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
Echo@HL@TrueQ[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint],
{RR,{(*(Subscript[R, 3,4]),*)(Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4]),(Subscript[R, 3,4])//(Subscript[dS, 3])//(Subscript[dS, 3])}},{AM,{(Subscript[am, 2,4->2]),(Subscript[am, 4,2->2])}},{BM,{(Subscript[bm, 1,3->1]),(Subscript[bm, 3,1->1])}}
]]

Not surprising. Given that papers cite left integrals and right integrals being related by the antipode, which is a more complicated beast, we can expect the formula for a right integral to be a bit more involved.

Block[{$k=0},Table[
pint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])//SS//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
pΔint=Simplify/@(
(Subscript[𝔼, {}->{1}])[μ (Subscript[a, 1])(Subscript[b, 1]),ν (Subscript[x, 1])(Subscript[y, 1]),1]//(Subscript[dm, i,1->i])// (Subscript[dΔ, i->i,j])//SS//((Subscript[𝔼, {i}->{1,2}])[(Subscript[β, i])(Subscript[b, 1])+(Subscript[α, i])(Subscript[a, 2]),(Subscript[η, i])(Subscript[y, 1])+(Subscript[ξ, i])(Subscript[x, 2]),1]RR)//BM//AM//(Subscript[P, 1,2])
);
Echo@HL@TrueQ[pint (Subscript[𝔼, {}->{j}])[0,0,1]≡pΔint],
{RR,{(Subscript[R, 3,4])//(Subscript[dS, 4])//(Subscript[dS, 4]),(Subscript[R, 3,4])//(Subscript[dS, 3])//(Subscript[dS, 3])}},{AM,{(Subscript[am, 2,4->2]),(Subscript[am, 4,2->2])}},{BM,{(Subscript[bm, 3,1->1]),(Subscript[bm, 1,3->1])}},{SS,{(Subscript[dS, i]),(Subscript[(OverBar[dS]), i])(*(Subscript[aS, i]),*)(*(Subscript[(OverBar[aS]), i]),*)(*(Subscript[bS, i]),*)(*(Subscript[(OverBar[bS]), i])*)}}
]]

Now it is time to actually review what the literature says on this matter.

The antipode on (SuperStar[H])should be given by ϕ|->ϕ∘S, where S denotes the antipode on H, yet the above computation suggests this is still not correct.

Aside: why are these not equal?

Simplify@((((((x))^(-ℏ/μ))))^(-2 μ/ℏ)) ≡(x^2)