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, BINOP_1:def 3
.= F . ((the_inverseOp_wrt F) . d1),(F . (F . ((the_inverseOp_wrt F) . d2),d1),d2) by A2, BINOP_1:def 3
.= F . ((the_inverseOp_wrt F) . d1),(F . (F . d1,((the_inverseOp_wrt F) . d2)),d2) by A3, BINOP_1:def 2
.= F . ((the_inverseOp_wrt F) . d1),(F . d1,(F . ((the_inverseOp_wrt F) . d2),d2)) by A2, BINOP_1:def 3
.= F . ((the_inverseOp_wrt F) . d1),(F . d1,(the_unity_wrt F)) by A1, A2, A4, Th63
.= F . (F . ((the_inverseOp_wrt F) . d1),d1),(the_unity_wrt F) by A2, BINOP_1:def 3
.= F . (the_unity_wrt F),(the_unity_wrt F) by A1, A2, A4, Th63
.= the_unity_wrt F by A1, SETWISEO:23 ;
hence (the_inverseOp_wrt F) . (F . d1,d2) = F . ((the_inverseOp_wrt F) . d1),((the_inverseOp_wrt F) . d2) by A1, A2, A4, Th64; :: thesis: verum