Proof of Proposition 3.10:

(*We establish the multiplication for SW. We set the variable l to be sw. The bar denotes inverse. *) 
vars={s,w,l};
(Subscript[m, i_,j_->k_])[Z_]:=Expand[Z]/.{(Subscript[s, i])(Subscript[s, j])->1,(Subscript[w, i])(Subscript[w, j])->0,(Subscript[s, i])(Subscript[w, j])->(Subscript[l, k]), (Subscript[w, i])(Subscript[s, j])->-(Subscript[l, k]),(Subscript[l, i])(Subscript[s, j])->-(Subscript[w, k]),(Subscript[s, i])(Subscript[l, j])->(Subscript[w, k]),(Subscript[l, i])(Subscript[w, j])->0,(Subscript[w, i])(Subscript[l, j])->0,(Subscript[l, i])(Subscript[l, j])->0, (Subscript[x_, i ])  /; MemberQ[vars,x]  :>(Subscript[x, k]),(Subscript[x_, j])/; MemberQ[vars,x]:>(Subscript[x, k])}

(* We start by declaring the elements R and κ: *)
(Subscript[κ, i_]) := (Subscript[λ, 1])+(Subscript[λ, 2])(Subscript[s, i])+(Subscript[λ, 3])(Subscript[w, i])+(Subscript[λ, 4])(Subscript[l, i]);
(Subscript[(OverBar[κ]), i_]) :=  (Subscript[(OverBar[λ]), 1])+(Subscript[(OverBar[λ]), 2])(Subscript[s, i])+(Subscript[(OverBar[λ]), 3])(Subscript[w, i])+(Subscript[(OverBar[λ]), 4])(Subscript[l, i]);
(Subscript[R, i_,j_]):=(Subscript[μ, 1,1])+ (Subscript[μ, 1,2])(Subscript[s, i])+(Subscript[μ, 1,3])(Subscript[w, i])+(Subscript[μ, 1,4])(Subscript[l, i]) +(Subscript[μ, 2,1])(Subscript[s, j])+ (Subscript[μ, 2,2])(Subscript[s, i])(Subscript[s, j])+(Subscript[μ, 2,3])(Subscript[w, i])(Subscript[s, j])+(Subscript[μ, 2,4])(Subscript[l, i]) (Subscript[s, j])+(Subscript[μ, 3,1])(Subscript[w, j])+ (Subscript[μ, 3,2])(Subscript[s, i])(Subscript[w, j])+(Subscript[μ, 3,3])(Subscript[w, i])(Subscript[w, j])+(Subscript[μ, 3,4])(Subscript[l, i]) (Subscript[w, j])+(Subscript[μ, 4,1])(Subscript[l, j])+ (Subscript[μ, 4,2])(Subscript[s, i])(Subscript[l, j])+(Subscript[μ, 4,3])(Subscript[w, i])(Subscript[l, j])+(Subscript[μ, 4,4])(Subscript[l, i])(Subscript[l, j])
(Subscript[(OverBar[R]), i_,j_]):=(Subscript[(OverBar[μ]), 1,1])+ (Subscript[(OverBar[μ]), 1,2])(Subscript[s, i])+(Subscript[(OverBar[μ]), 1,3])(Subscript[w, i])+(Subscript[(OverBar[μ]), 1,4])(Subscript[l, i]) +(Subscript[(OverBar[μ]), 2,1])(Subscript[s, j])+ (Subscript[(OverBar[μ]), 2,2])(Subscript[s, i])(Subscript[s, j])+(Subscript[(OverBar[μ]), 2,3])(Subscript[w, i])(Subscript[s, j])+(Subscript[(OverBar[μ]), 2,4])(Subscript[l, i]) (Subscript[s, j])+(Subscript[(OverBar[μ]), 3,1])(Subscript[w, j])+ (Subscript[(OverBar[μ]), 3,2])(Subscript[s, i])(Subscript[w, j])+(Subscript[(OverBar[μ]), 3,3])(Subscript[w, i])(Subscript[w, j])+(Subscript[(OverBar[μ]), 3,4])(Subscript[l, i]) (Subscript[w, j])+(Subscript[(OverBar[μ]), 4,1])(Subscript[l, j])+ (Subscript[(OverBar[μ]), 4,2])(Subscript[s, i])(Subscript[l, j])+(Subscript[(OverBar[μ]), 4,3])(Subscript[w, i])(Subscript[l, j])+(Subscript[(OverBar[μ]), 4,4])(Subscript[l, i])(Subscript[l, j])
(*We also implement the element ν :*)
(Subscript[ν, i_]):=(Subscript[R, 1,3])(Subscript[(OverBar[κ]), 2])//(Subscript[m, 1,2->1])//(Subscript[m, 1,3->i])
(Subscript[(OverBar[ν]), i_]):=(Subscript[(OverBar[R]), 3,1])(Subscript[(OverBar[κ]), 2])//(Subscript[m, 1,2->1])//(Subscript[m, 1,3->i])

(*By the previous lemma, we simply set the values of the bar variables: *)
{(Subscript[(OverBar[λ]), 1]),(Subscript[(OverBar[λ]), 2]),(Subscript[(OverBar[λ]), 3]),(Subscript[(OverBar[λ]), 4])}={((Subscript[λ, 1])/((Subscript[λ, 1]^2)-(Subscript[λ, 2]^2))),-((Subscript[λ, 2])/((Subscript[λ, 1]^2)-(Subscript[λ, 2]^2))),-((Subscript[λ, 3])/((Subscript[λ, 1]^2)-(Subscript[λ, 2]^2))),-((Subscript[λ, 4])/((Subscript[λ, 1]^2)-(Subscript[λ, 2]^2)))};
rulesRinv={(Subscript[(OverBar[μ]), 1,1])->-((-(Subscript[μ, 1,1]^3)+(Subscript[μ, 1,1]) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,1]) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])+(Subscript[μ, 1,1]) (Subscript[μ, 2,2]^2))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 1,2])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 1,2])-(Subscript[μ, 1,2]^3)+(Subscript[μ, 1,2]) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])+(Subscript[μ, 1,2]) (Subscript[μ, 2,2]^2))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 1,3])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 1,3])-(Subscript[μ, 1,2]^2) (Subscript[μ, 1,3])+(Subscript[μ, 1,3]) (Subscript[μ, 2,1]^2)-(Subscript[μ, 1,3]) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,1]) (Subscript[μ, 2,3])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,2]) (Subscript[μ, 2,3]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 1,4])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 1,4])-(Subscript[μ, 1,2]^2) (Subscript[μ, 1,4])+(Subscript[μ, 1,4]) (Subscript[μ, 2,1]^2)-(Subscript[μ, 1,4]) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,1]) (Subscript[μ, 2,4])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,2]) (Subscript[μ, 2,4]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 2,1])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 2,1])+(Subscript[μ, 1,2]^2) (Subscript[μ, 2,1])-(Subscript[μ, 2,1]^3)-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,2])+(Subscript[μ, 2,1]) (Subscript[μ, 2,2]^2))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 2,2])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1])+(Subscript[μ, 1,1]^2) (Subscript[μ, 2,2])+(Subscript[μ, 1,2]^2) (Subscript[μ, 2,2])+(Subscript[μ, 2,1]^2) (Subscript[μ, 2,2])-(Subscript[μ, 2,2]^3))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 2,3])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,3]) (Subscript[μ, 2,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,3]) (Subscript[μ, 2,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 2,3])-(Subscript[μ, 1,2]^2) (Subscript[μ, 2,3])+(Subscript[μ, 2,1]^2) (Subscript[μ, 2,3])-(Subscript[μ, 2,2]^2) (Subscript[μ, 2,3]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 2,4])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,4]) (Subscript[μ, 2,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,4]) (Subscript[μ, 2,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 2,4])-(Subscript[μ, 1,2]^2) (Subscript[μ, 2,4])+(Subscript[μ, 2,1]^2) (Subscript[μ, 2,4])-(Subscript[μ, 2,2]^2) (Subscript[μ, 2,4]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 3,1])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 3,1])+(Subscript[μ, 1,2]^2) (Subscript[μ, 3,1])-(Subscript[μ, 2,1]^2) (Subscript[μ, 3,1])-(Subscript[μ, 2,2]^2) (Subscript[μ, 3,1])-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 3,2])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,2]) (Subscript[μ, 3,2]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 3,2])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 3,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,2]) (Subscript[μ, 3,1])+(Subscript[μ, 1,1]^2) (Subscript[μ, 3,2])+(Subscript[μ, 1,2]^2) (Subscript[μ, 3,2])-(Subscript[μ, 2,1]^2) (Subscript[μ, 3,2])-(Subscript[μ, 2,2]^2) (Subscript[μ, 3,2]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 3,3])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,3]) (Subscript[μ, 3,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,3]) (Subscript[μ, 3,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,3]) (Subscript[μ, 3,2])-2 (Subscript[μ, 2,2]) (Subscript[μ, 2,3]) (Subscript[μ, 3,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 3,3])-(Subscript[μ, 1,2]^2) (Subscript[μ, 3,3])-(Subscript[μ, 2,1]^2) (Subscript[μ, 3,3])+(Subscript[μ, 2,2]^2) (Subscript[μ, 3,3])+2 (Subscript[μ, 1,4]) (Subscript[μ, 2,2]) (Subscript[μ, 4,1])-2 (Subscript[μ, 1,2]) (Subscript[μ, 2,4]) (Subscript[μ, 4,1])-2 (Subscript[μ, 1,4]) (Subscript[μ, 2,1]) (Subscript[μ, 4,2])+2 (Subscript[μ, 1,1]) (Subscript[μ, 2,4]) (Subscript[μ, 4,2])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 4,4])-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,2]) (Subscript[μ, 4,4]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 3,4])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,4]) (Subscript[μ, 3,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,4]) (Subscript[μ, 3,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,4]) (Subscript[μ, 3,2])-2 (Subscript[μ, 2,2]) (Subscript[μ, 2,4]) (Subscript[μ, 3,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 3,4])-(Subscript[μ, 1,2]^2) (Subscript[μ, 3,4])-(Subscript[μ, 2,1]^2) (Subscript[μ, 3,4])+(Subscript[μ, 2,2]^2) (Subscript[μ, 3,4])+2 (Subscript[μ, 1,3]) (Subscript[μ, 2,2]) (Subscript[μ, 4,1])-2 (Subscript[μ, 1,2]) (Subscript[μ, 2,3]) (Subscript[μ, 4,1])-2 (Subscript[μ, 1,3]) (Subscript[μ, 2,1]) (Subscript[μ, 4,2])+2 (Subscript[μ, 1,1]) (Subscript[μ, 2,3]) (Subscript[μ, 4,2])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 4,3])-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,2]) (Subscript[μ, 4,3]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 4,1])->-(((Subscript[μ, 1,1]^2) (Subscript[μ, 4,1])+(Subscript[μ, 1,2]^2) (Subscript[μ, 4,1])-(Subscript[μ, 2,1]^2) (Subscript[μ, 4,1])-(Subscript[μ, 2,2]^2) (Subscript[μ, 4,1])-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 4,2])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,2]) (Subscript[μ, 4,2]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 4,2])->-((-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 4,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,2]) (Subscript[μ, 4,1])+(Subscript[μ, 1,1]^2) (Subscript[μ, 4,2])+(Subscript[μ, 1,2]^2) (Subscript[μ, 4,2])-(Subscript[μ, 2,1]^2) (Subscript[μ, 4,2])-(Subscript[μ, 2,2]^2) (Subscript[μ, 4,2]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 4,3])->-((2 (Subscript[μ, 1,4]) (Subscript[μ, 2,2]) (Subscript[μ, 3,1])-2 (Subscript[μ, 1,2]) (Subscript[μ, 2,4]) (Subscript[μ, 3,1])-2 (Subscript[μ, 1,4]) (Subscript[μ, 2,1]) (Subscript[μ, 3,2])+2 (Subscript[μ, 1,1]) (Subscript[μ, 2,4]) (Subscript[μ, 3,2])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 3,4])-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,2]) (Subscript[μ, 3,4])-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,3]) (Subscript[μ, 4,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,3]) (Subscript[μ, 4,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,3]) (Subscript[μ, 4,2])-2 (Subscript[μ, 2,2]) (Subscript[μ, 2,3]) (Subscript[μ, 4,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 4,3])-(Subscript[μ, 1,2]^2) (Subscript[μ, 4,3])-(Subscript[μ, 2,1]^2) (Subscript[μ, 4,3])+(Subscript[μ, 2,2]^2) (Subscript[μ, 4,3]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4))),(Subscript[(OverBar[μ]), 4,4])->-((2 (Subscript[μ, 1,3]) (Subscript[μ, 2,2]) (Subscript[μ, 3,1])-2 (Subscript[μ, 1,2]) (Subscript[μ, 2,3]) (Subscript[μ, 3,1])-2 (Subscript[μ, 1,3]) (Subscript[μ, 2,1]) (Subscript[μ, 3,2])+2 (Subscript[μ, 1,1]) (Subscript[μ, 2,3]) (Subscript[μ, 3,2])+2 (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 3,3])-2 (Subscript[μ, 1,1]) (Subscript[μ, 2,2]) (Subscript[μ, 3,3])-2 (Subscript[μ, 1,1]) (Subscript[μ, 1,4]) (Subscript[μ, 4,1])+2 (Subscript[μ, 2,1]) (Subscript[μ, 2,4]) (Subscript[μ, 4,1])+2 (Subscript[μ, 1,2]) (Subscript[μ, 1,4]) (Subscript[μ, 4,2])-2 (Subscript[μ, 2,2]) (Subscript[μ, 2,4]) (Subscript[μ, 4,2])+(Subscript[μ, 1,1]^2) (Subscript[μ, 4,4])-(Subscript[μ, 1,2]^2) (Subscript[μ, 4,4])-(Subscript[μ, 2,1]^2) (Subscript[μ, 4,4])+(Subscript[μ, 2,2]^2) (Subscript[μ, 4,4]))/((Subscript[μ, 1,1]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 1,2]^2)+(Subscript[μ, 1,2]^4)-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,1]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,1]^2)+(Subscript[μ, 2,1]^4)+8 (Subscript[μ, 1,1]) (Subscript[μ, 1,2]) (Subscript[μ, 2,1]) (Subscript[μ, 2,2])-2 (Subscript[μ, 1,1]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 1,2]^2) (Subscript[μ, 2,2]^2)-2 (Subscript[μ, 2,1]^2) (Subscript[μ, 2,2]^2)+(Subscript[μ, 2,2]^4)))};
Scan[Set@@#&,rulesRinv]

(*Sanity check:*)
(Subscript[κ, 1])(Subscript[(OverBar[κ]), 2])//(Subscript[m, 1,2->1])//Simplify
(Subscript[κ, 1])(Subscript[(OverBar[κ]), 2])//(Subscript[m, 2,1->1])//Simplify
(Subscript[R, 1,2])(Subscript[(OverBar[R]), 3,4])//(Subscript[m, 1,3->1])//(Subscript[m, 2,4->1])//Simplify
(Subscript[R, 1,2])(Subscript[(OverBar[R]), 3,4])//(Subscript[m, 3,1->1])//(Subscript[m, 4,2->1])//Simplify

(*Let us now analyse the commutators. We start with [R, κ⊗1 ] :*)

vari={(Subscript[s, 1]),(Subscript[w, 1]),(Subscript[l, 1]),(Subscript[s, 2]),(Subscript[w, 2]),(Subscript[l, 2])};
variL={"(Subscript[s, 1])","(Subscript[w, 1])","(Subscript[l, 1])","(Subscript[s, 2])","(Subscript[w, 2])","(Subscript[l, 2])"};
p=((Subscript[R, 1,2])(Subscript[κ, 3])//(Subscript[m, 1,3->1]))-((Subscript[R, 1,2])(Subscript[κ, 3])//(Subscript[m, 3,1->1]));
cr=CoefficientRules[p,vari];
convert[{v___Integer}]:=StringJoin@Pick[variL,{v},1];
(convert[First[#]]->Last[#])&/@cr

(*We have indicated the monomial to which each coefficient corresponds to.  All one has to show is that the coefficients not in J⊗J are zero,for instance "2 (Subscript[γ, 4]) (Subscript[μ, 2, 2])-2 (Subscript[γ, 2]) (Subscript[μ, 2, 4]) =0" for (Subscript[w, 1])(Subscript[s, 2]). The strategy of the proof is to show that these must be consequences of the XC-axioms. We will show that these are consequences of only XC0c. For this we will compute a Groebner basis for the coefficients of the relation XC0c.*)

vari={(Subscript[s, 1]),(Subscript[w, 1]),(Subscript[l, 1]),(Subscript[s, 2]),(Subscript[w, 2]),(Subscript[l, 2])};
variL={"(Subscript[s, 1])","(Subscript[w, 1])","(Subscript[l, 1])","(Subscript[s, 2])","(Subscript[w, 2])","(Subscript[l, 2])"};
p=(((Subscript[κ, 1])(Subscript[κ, 2])(Subscript[R, 3,4])(Subscript[(OverBar[κ]), 5])(Subscript[(OverBar[κ]), 6])//(Subscript[m, 1,3->1])//(Subscript[m, 1,5->1])//(Subscript[m, 2,4->2])//(Subscript[m, 2,6->2]))-(Subscript[R, 1,2]));
cr=CoefficientRules[p,vari]//Simplify//Expand;
convert[{v___Integer}]:=StringJoin@Pick[variL,{v},1];
(convert[First[#]]->Last[#])&/@cr
eqs=Thread[Values[cr]]//Simplify//Expand;

(*We compute a Groebner Basis A and the transformation matrix B:*)

{A,B}=ResourceFunction["ExtendedGroebnerBasis"][eqs,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])},CoefficientDomain->RationalFunctions,MonomialOrder->DegreeReverseLexicographic]

(*Checking that the calculation is correct:*)
(A//Simplify//Expand)===(B.eqs//Simplify//Expand)

(*We observe that in fact the elements of the Groebner basis do not have denominators:*)
A//Simplify

(*In order to decompose the coefficients of [R, κ⊗1 ] not in J⊗J as combination of the elements of A, we use PolynomialReduce. We start with 2 (Subscript[λ, 4]) (Subscript[μ, 1,2])-2 (Subscript[λ, 2]) (Subscript[μ, 1,4]), ie the coefficient of w⊗1 : *)
F= PolynomialReduce[2 (Subscript[λ, 4]) (Subscript[μ, 1,2])-2 (Subscript[λ, 2]) (Subscript[μ, 1,4]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify

(*Indeed this is exactly one of the polynomials in the Groebner basis: *)

Pick[A,Unitize[F[[1]]],1]//Simplify//Factor

(*Let us see, for this case in particular, how the polynomial 2 ((Subscript[λ, 4]) (Subscript[μ, 1,2])-(Subscript[λ, 2]) (Subscript[μ, 1,4])) is obtained from XC0 :*)

pos=Flatten[Position[F[[1]],1]];
B[[pos]].eqs
B[[pos]].eqs//Simplify

(*We now check the remaining coefficients of [R, κ⊗1 ] not in J⊗J :*)

PolynomialReduce[2 (Subscript[λ, 3]) (Subscript[μ, 1,2])-2 (Subscript[λ, 2]) (Subscript[μ, 1,3]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify
PolynomialReduce[2 (Subscript[λ, 4]) (Subscript[μ, 2,2])-2 (Subscript[λ, 2]) (Subscript[μ, 2,4]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify
PolynomialReduce[2 (Subscript[λ, 3]) (Subscript[μ, 2,2])-2 (Subscript[λ, 2]) (Subscript[μ, 2,3]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify

(*Now we turn into [R, 1⊗κ ] :*)

vari={(Subscript[s, 1]),(Subscript[w, 1]),(Subscript[l, 1]),(Subscript[s, 2]),(Subscript[w, 2]),(Subscript[l, 2])};
variL={"(Subscript[s, 1])","(Subscript[w, 1])","(Subscript[l, 1])","(Subscript[s, 2])","(Subscript[w, 2])","(Subscript[l, 2])"};
p=((Subscript[R, 1,2])(Subscript[κ, 3])//(Subscript[m, 2,3->2]))-((Subscript[R, 1,2])(Subscript[κ, 3])//(Subscript[m, 3,2->2]));
cr=CoefficientRules[p,vari];
convert[{v___Integer}]:=StringJoin@Pick[variL,{v},1];
(convert[First[#]]->Last[#])&/@cr
eqs=Thread[Values[cr]==0];

(*We check the coefficients that do not belong to J ⊗ J:*)

PolynomialReduce[2 (Subscript[λ, 4]) (Subscript[μ, 2,2])-2 (Subscript[λ, 2]) (Subscript[μ, 4,2]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify
PolynomialReduce[2 (Subscript[λ, 3]) (Subscript[μ, 2,2])-2 (Subscript[λ, 2]) (Subscript[μ, 3,2]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify
PolynomialReduce[2 (Subscript[λ, 4]) (Subscript[μ, 2,1])-2 (Subscript[λ, 2]) (Subscript[μ, 4,1]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify
PolynomialReduce[2 (Subscript[λ, 3]) (Subscript[μ, 2,1])-2 (Subscript[λ, 2]) (Subscript[μ, 3,1]),A,{(Subscript[λ, 3]),(Subscript[λ, 4]) ,(Subscript[μ, 1,1]),(Subscript[μ, 1,2]),(Subscript[μ, 1,3]),(Subscript[μ, 1,4]),(Subscript[μ, 2,1]),(Subscript[μ, 2,2]),(Subscript[μ, 2,3]), (Subscript[μ, 2,4]) ,(Subscript[μ, 3,1]), (Subscript[μ, 3,2]),(Subscript[μ, 3,3]),(Subscript[μ, 3,4]), (Subscript[μ, 4,1]),(Subscript[μ, 4,2]), (Subscript[μ, 4,3]), (Subscript[μ, 4,4])}]//Simplify

(*This concludes the proof.*)