let ADG be Proper_Uniquely_Two_Divisible_Group; for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for o being Element of (AV ADG) st ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 holds
for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
let f be Function of the carrier of ADG, the carrier of ADG; for o9 being Element of ADG
for o being Element of (AV ADG) st ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 holds
for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
let o9 be Element of ADG; for o being Element of (AV ADG) st ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 holds
for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
let o be Element of (AV ADG); ( ( for x being Element of ADG holds f . x = o9 + x ) & o = o9 implies for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) ) )
assume that
A1:
for x being Element of ADG holds f . x = o9 + x
and
A2:
o = o9
; for a, b being Element of ADG holds
( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
let a, b be Element of ADG; ( f . (a + b) = (Padd o) . ((f . a),(f . b)) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )
set a9 = f . a;
set b9 = f . b;
A3:
AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #)
by TDGROUP:def 3;
then reconsider a99 = f . a, b99 = f . b as Element of (AV ADG) ;
thus
f . (a + b) = (Padd o) . ((f . a),(f . b))
( f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = (Pcom o) . (f . a) )proof
A4:
(Padd o) . (
(f . a),
(f . b))
= Padd (
o,
a99,
b99)
by Def6;
then reconsider c99 =
(Padd o) . (
(f . a),
(f . b)) as
Element of
(AV ADG) ;
reconsider c9 =
c99 as
Element of
ADG by A3;
o,
a99 // b99,
c99
by A4, Def5;
then
[[o9,(f . a)],[(f . b),c9]] in CONGRD ADG
by A2, A3, ANALOAF:def 2;
then A5:
o9 + c9 = (f . a) + (f . b)
by TDGROUP:def 2;
(
f . a = o9 + a &
f . b = o9 + b )
by A1;
then o9 + c9 =
o9 + ((a + o9) + b)
by A5, RLVECT_1:def 3
.=
o9 + (o9 + (a + b))
by RLVECT_1:def 3
;
then c9 =
o9 + (a + b)
by RLVECT_1:8
.=
f . (a + b)
by A1
;
hence
f . (a + b) = (Padd o) . (
(f . a),
(f . b))
;
verum
end;
f . (0. ADG) =
o9 + (0. ADG)
by A1
.=
0. (GroupVect ((AV ADG),o))
by A2, RLVECT_1:4
;
hence
f . (0. ADG) = 0. (GroupVect ((AV ADG),o))
; f . (- a) = (Pcom o) . (f . a)
thus
f . (- a) = (Pcom o) . (f . a)
verumproof
A6:
(Pcom o) . (f . a) = Pcom (
o,
a99)
by Def7;
then reconsider c99 =
(Pcom o) . (f . a) as
Element of
(AV ADG) ;
reconsider c9 =
c99 as
Element of
ADG by A3;
a99,
o // o,
c99
by A6, Lm1;
then
[[(f . a),o9],[o9,c9]] in CONGRD ADG
by A2, A3, ANALOAF:def 2;
then
(f . a) + c9 = o9 + o9
by TDGROUP:def 2;
then A7:
o9 + o9 =
(o9 + a) + c9
by A1
.=
o9 + (a + c9)
by RLVECT_1:def 3
;
f . (- a) =
o9 + (- a)
by A1
.=
(c9 + a) + (- a)
by A7, RLVECT_1:8
.=
c9 + (a + (- a))
by RLVECT_1:def 3
.=
c9 + (0. ADG)
by RLVECT_1:5
.=
c9
by RLVECT_1:4
;
hence
f . (- a) = (Pcom o) . (f . a)
;
verum
end;