let ADG be Proper_Uniquely_Two_Divisible_Group; for o9 being Element of ADG
for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o9 be Element of ADG; for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
let o be Element of (AV ADG); ( o = o9 implies ADG, GroupVect ((AV ADG),o) are_Iso )
assume A1:
o = o9
; ADG, GroupVect ((AV ADG),o) are_Iso
set AS = AV ADG;
set X = the carrier of ADG;
set Z = GroupVect ((AV ADG),o);
set T = the carrier of (GroupVect ((AV ADG),o));
deffunc H1( Element of the carrier of ADG) -> Element of the carrier of ADG = o9 + $1;
consider g being UnOp of the carrier of ADG such that
A2:
for a being Element of the carrier of ADG holds g . a = H1(a)
from FUNCT_2:sch 4();
the carrier of ADG = the carrier of (GroupVect ((AV ADG),o))
by TDGROUP:4;
then reconsider f = g as Function of the carrier of ADG, the carrier of (GroupVect ((AV ADG),o)) ;
A3:
now for a, b being Element of ADG holds
( f . (a + b) = (f . a) + (f . b) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )let a,
b be
Element of
ADG;
( f . (a + b) = (f . a) + (f . b) & f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )reconsider fa =
f . a as
Element of
(AV ADG) ;
thus
f . (a + b) = (f . a) + (f . b)
by A1, A2, Th52;
( f . (0. ADG) = 0. (GroupVect ((AV ADG),o)) & f . (- a) = - (f . a) )thus
f . (0. ADG) = 0. (GroupVect ((AV ADG),o))
by A1, A2, Th52;
f . (- a) = - (f . a)thus f . (- a) =
(Pcom o) . fa
by A1, A2, Th52
.=
- (f . a)
by Th44
;
verum end;
( f is one-to-one & rng f = the carrier of (GroupVect ((AV ADG),o)) )
by A2, Th53, Th54;
then
f is_Iso_of ADG, GroupVect ((AV ADG),o)
by A3;
hence
ADG, GroupVect ((AV ADG),o) are_Iso
; verum