let F be Field; :: thesis: for a, c being Element of the carrier of F
for b, d being Element of NonZero F holds
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
let a, c be Element of the carrier of F; :: thesis: for b, d being Element of NonZero F holds
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
let b, d be Element of NonZero F; :: thesis: ( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
A1:
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) implies (omf F) . a,d = (omf F) . b,c )
proof
reconsider revfb =
(revf F) . b,
revfd =
(revf F) . d as
Element of
NonZero F ;
reconsider crevfd =
c * revfd as
Element of the
carrier of
F ;
assume A2:
(omf F) . a,
((revf F) . b) = (omf F) . c,
((revf F) . d)
;
:: thesis: (omf F) . a,d = (omf F) . b,c
A3:
a =
a * (1. F)
by REALSET2:25
.=
(omf F) . a,
(b * revfb)
by REALSET2:def 18
.=
a * (revfb * b)
.=
(a * revfb) * b
by REALSET2:23
.=
b * crevfd
by A2
.=
(omf F) . b,
((omf F) . c,((revf F) . d))
;
A4:
c =
c * (1. F)
by REALSET2:25
.=
(omf F) . c,
(d * revfd)
by REALSET2:def 18
.=
c * (revfd * d)
.=
(c * revfd) * d
by REALSET2:23
;
thus (omf F) . a,
d =
(b * (c * revfd)) * d
by A3
.=
b * ((c * revfd) * d)
by REALSET2:23
.=
(omf F) . b,
c
by A4
;
:: thesis: verum
end;
( (omf F) . a,d = (omf F) . b,c implies (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) )
proof
reconsider revfd =
(revf F) . d,
revfb =
(revf F) . b as
Element of
NonZero F ;
reconsider crevfd =
(omf F) . c,
revfd as
Element of
F ;
assume A5:
(omf F) . a,
d = (omf F) . b,
c
;
:: thesis: (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d)
a =
a * (1. F)
by REALSET2:25
.=
(omf F) . a,
(1. F)
.=
a * (d * revfd)
by REALSET2:def 18
.=
(a * d) * revfd
by REALSET2:23
.=
(b * c) * revfd
by A5
.=
b * (c * revfd)
by REALSET2:23
.=
crevfd * b
;
hence (omf F) . a,
((revf F) . b) =
(crevfd * b) * revfb
.=
crevfd * (b * revfb)
by REALSET2:23
.=
((omf F) . c,revfd) * (1. F)
by REALSET2:def 18
.=
(omf F) . c,
((revf F) . d)
by REALSET2:25
;
:: thesis: verum
end;
hence
( (omf F) . a,((revf F) . b) = (omf F) . c,((revf F) . d) iff (omf F) . a,d = (omf F) . b,c )
by A1; :: thesis: verum