let D be non empty set ; :: thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp holds
the_inverseOp_wrt F is_distributive_wrt F
let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp implies the_inverseOp_wrt F is_distributive_wrt F )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is commutative and
A4: F is having_an_inverseOp ; :: thesis: the_inverseOp_wrt F is_distributive_wrt F
let d1 be Element of D; :: according to BINOP_1:def 20 :: thesis: for b₁ being Element of D holds (the_inverseOp_wrt F) . (F . (d1,b₁)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . b₁))
let d2 be Element of D; :: thesis: (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2))
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;
F . ((F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2))),(F . (d1,d2))) = F . (((the_inverseOp_wrt F) . d1),(F . (((the_inverseOp_wrt F) . d2),(F . (d1,d2))))) by A2
.= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (((the_inverseOp_wrt F) . d2),d1)),d2))) by A2
.= F . (((the_inverseOp_wrt F) . d1),(F . ((F . (d1,((the_inverseOp_wrt F) . d2))),d2))) by A3
.= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(F . (((the_inverseOp_wrt F) . d2),d2))))) by A2
.= F . (((the_inverseOp_wrt F) . d1),(F . (d1,(the_unity_wrt F)))) by A1, A2, A4, Th59
.= F . ((F . (((the_inverseOp_wrt F) . d1),d1)),(the_unity_wrt F)) by A2
.= F . ((the_unity_wrt F),(the_unity_wrt F)) by A1, A2, A4, Th59
.= the_unity_wrt F by A1, SETWISEO:15 ;
hence (the_inverseOp_wrt F) . (F . (d1,d2)) = F . (((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2)) by A1, A2, A4, Th60; :: thesis: verum