let AFV be strict AffVect; for o being Element of AFV holds AFV = AV (GroupVect (AFV,o))
let o be Element of AFV; AFV = AV (GroupVect (AFV,o))
set X = GroupVect (AFV,o);
now for x, y being object holds
( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV )let x,
y be
object ;
( [x,y] in CONGRD (GroupVect (AFV,o)) iff [x,y] in the CONGR of AFV )set xy =
[x,y];
A1:
now ( [x,y] in the CONGR of AFV implies [x,y] in CONGRD (GroupVect (AFV,o)) )set V = the
carrier of
AFV;
assume A2:
[x,y] in the
CONGR of
AFV
;
[x,y] in CONGRD (GroupVect (AFV,o))set VV =
[: the carrier of AFV, the carrier of AFV:];
[x,y] `2 = y
;
then A3:
y in [: the carrier of AFV, the carrier of AFV:]
by A2, MCART_1:10;
then A4:
y = [(y `1),(y `2)]
by MCART_1:21;
[x,y] `1 = x
;
then A5:
x in [: the carrier of AFV, the carrier of AFV:]
by A2, MCART_1:10;
then reconsider x1 =
x `1 ,
x2 =
x `2 ,
y1 =
y `1 ,
y2 =
y `2 as
Element of
AFV by A3, MCART_1:10;
reconsider x19 =
x1,
x29 =
x2,
y19 =
y1,
y29 =
y2 as
Element of
(GroupVect (AFV,o)) ;
A6:
x = [(x `1),(x `2)]
by A5, MCART_1:21;
then A7:
x1,
x2 // y1,
y2
by A2, A4, ANALOAF:def 2;
x19 # y29 = x29 # y19
proof
reconsider z1 =
x19 # y29,
z2 =
x29 # y19 as
Element of
AFV ;
z1 = Padd (
o,
x1,
y2)
by Def6;
then
o,
x1 // y2,
z1
by Def5;
then
x1,
o // z1,
y2
by Th7;
then A8:
o,
x2 // y1,
z1
by A7, Th12;
z2 = Padd (
o,
x2,
y1)
by Def6;
hence
x19 # y29 = x29 # y19
by A8, Def5;
verum
end; hence
[x,y] in CONGRD (GroupVect (AFV,o))
by A6, A4, TDGROUP:def 2;
verum end; now ( [x,y] in CONGRD (GroupVect (AFV,o)) implies [x,y] in the CONGR of AFV )set V = the
carrier of
(GroupVect (AFV,o));
assume A9:
[x,y] in CONGRD (GroupVect (AFV,o))
;
[x,y] in the CONGR of AFVset VV =
[: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):];
[x,y] `2 = y
;
then A10:
y in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):]
by A9, MCART_1:10;
then A11:
y = [(y `1),(y `2)]
by MCART_1:21;
[x,y] `1 = x
;
then A12:
x in [: the carrier of (GroupVect (AFV,o)), the carrier of (GroupVect (AFV,o)):]
by A9, MCART_1:10;
then reconsider x19 =
x `1 ,
x29 =
x `2 ,
y19 =
y `1 ,
y29 =
y `2 as
Element of
(GroupVect (AFV,o)) by A10, MCART_1:10;
set z19 =
x19 # y29;
set z29 =
x29 # y19;
reconsider x1 =
x19,
x2 =
x29,
y1 =
y19,
y2 =
y29 as
Element of
AFV ;
reconsider z1 =
x19 # y29,
z2 =
x29 # y19 as
Element of
AFV ;
A13:
z2 = Padd (
o,
x2,
y1)
by Def6;
z1 = Padd (
o,
x1,
y2)
by Def6;
then A14:
o,
x1 // y2,
z1
by Def5;
A15:
x = [(x `1),(x `2)]
by A12, MCART_1:21;
then
x19 # y29 = x29 # y19
by A9, A11, TDGROUP:def 2;
then
o,
x2 // y1,
z1
by A13, Def5;
then
x1,
x2 // y1,
y2
by A14, Th12;
hence
[x,y] in the
CONGR of
AFV
by A15, A11, ANALOAF:def 2;
verum end; hence
(
[x,y] in CONGRD (GroupVect (AFV,o)) iff
[x,y] in the
CONGR of
AFV )
by A1;
verum end;
then
( the carrier of (AV (GroupVect (AFV,o))) = the carrier of AFV & CONGRD (GroupVect (AFV,o)) = the CONGR of AFV )
by RELAT_1:def 2, TDGROUP:4;
hence
AFV = AV (GroupVect (AFV,o))
by TDGROUP:4; verum