let F be Field; for a, c being Element 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 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 b, d be Element of NonZero F; ( (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
F ;
assume A2:
(omf F) . (
a,
((revf F) . b))
= (omf F) . (
c,
((revf F) . d))
;
(omf F) . (a,d) = (omf F) . (b,c)
A3:
c =
c * (1. F)
by REALSET2:21
.=
(omf F) . (
c,
(d * revfd))
by REALSET2:def 6
.=
c * (revfd * d)
.=
(c * revfd) * d
by REALSET2:19
;
a =
a * (1. F)
by REALSET2:21
.=
(omf F) . (
a,
(b * revfb))
by REALSET2:def 6
.=
a * (revfb * b)
.=
(a * revfb) * b
by REALSET2:19
.=
b * crevfd
by A2
.=
(omf F) . (
b,
((omf F) . (c,((revf F) . d))))
;
hence (omf F) . (
a,
d) =
(b * (c * revfd)) * d
.=
b * ((c * revfd) * d)
by REALSET2:19
.=
(omf F) . (
b,
c)
by A3
;
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 A4:
(omf F) . (
a,
d)
= (omf F) . (
b,
c)
;
(omf F) . (a,((revf F) . b)) = (omf F) . (c,((revf F) . d))
a =
a * (1. F)
by REALSET2:21
.=
(omf F) . (
a,
(1. F))
.=
a * (d * revfd)
by REALSET2:def 6
.=
(a * d) * revfd
by REALSET2:19
.=
(b * c) * revfd
by A4
.=
b * (c * revfd)
by REALSET2:19
.=
crevfd * b
;
hence (omf F) . (
a,
((revf F) . b)) =
(crevfd * b) * revfb
.=
crevfd * (b * revfb)
by REALSET2:19
.=
((omf F) . (c,revfd)) * (1. F)
by REALSET2:def 6
.=
(omf F) . (
c,
((revf F) . d))
by REALSET2:21
;
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; verum