let AFV be strict AffVect; :: thesis: for o being Element of AFV holds AFV = AV (GroupVect AFV,o)
let o be Element of AFV; :: thesis: AFV = AV (GroupVect AFV,o)
set X = GroupVect AFV,o;
A1:
the carrier of (AV (GroupVect AFV,o)) = the carrier of AFV
by TDGROUP:9;
CONGRD (GroupVect AFV,o) = the CONGR of AFV
proof
now let x,
y be
set ;
:: thesis: ( [x,y] in CONGRD (GroupVect AFV,o) iff [x,y] in the CONGR of AFV )set xy =
[x,y];
A2:
now assume A3:
[x,y] in CONGRD (GroupVect AFV,o)
;
:: thesis: [x,y] in the CONGR of AFVset V = the
carrier of
(GroupVect AFV,o);
set VV =
[:the carrier of (GroupVect AFV,o),the carrier of (GroupVect AFV,o):];
(
[x,y] `1 = x &
[x,y] `2 = y )
by MCART_1:7;
then A4:
(
x in [:the carrier of (GroupVect AFV,o),the carrier of (GroupVect AFV,o):] &
y in [:the carrier of (GroupVect AFV,o),the carrier of (GroupVect AFV,o):] )
by A3, MCART_1:10;
then A5:
(
x = [(x `1 ),(x `2 )] &
y = [(y `1 ),(y `2 )] &
x `1 in the
carrier of
(GroupVect AFV,o) &
x `2 in the
carrier of
(GroupVect AFV,o) &
y `1 in the
carrier of
(GroupVect AFV,o) &
y `2 in the
carrier of
(GroupVect AFV,o) )
by MCART_1:10, MCART_1:23;
reconsider x1' =
x `1 ,
x2' =
x `2 ,
y1' =
y `1 ,
y2' =
y `2 as
Element of
(GroupVect AFV,o) by A4, MCART_1:10;
reconsider x1 =
x1',
x2 =
x2',
y1 =
y1',
y2 =
y2' as
Element of
AFV ;
set z1' =
x1' # y2';
set z2' =
x2' # y1';
A6:
x1' # y2' = x2' # y1'
by A3, A5, TDGROUP:def 4;
reconsider z1 =
x1' # y2',
z2 =
x2' # y1' as
Element of
AFV ;
(
z1 = Padd o,
x1,
y2 &
z2 = Padd o,
x2,
y1 )
by Def7;
then
(
o,
x1 // y2,
z1 &
o,
x2 // y1,
z1 )
by A6, Def5;
then
x1,
x2 // y1,
y2
by Th13;
hence
[x,y] in the
CONGR of
AFV
by A5, ANALOAF:def 2;
:: thesis: verum end; now assume A7:
[x,y] in the
CONGR of
AFV
;
:: thesis: [x,y] in CONGRD (GroupVect AFV,o)set V = the
carrier of
AFV;
set VV =
[:the carrier of AFV,the carrier of AFV:];
(
[x,y] `1 = x &
[x,y] `2 = y )
by MCART_1:7;
then A8:
(
x in [:the carrier of AFV,the carrier of AFV:] &
y in [:the carrier of AFV,the carrier of AFV:] )
by A7, MCART_1:10;
then A9:
(
x = [(x `1 ),(x `2 )] &
y = [(y `1 ),(y `2 )] &
x `1 in the
carrier of
AFV &
x `2 in the
carrier of
AFV &
y `1 in the
carrier of
AFV &
y `2 in the
carrier of
AFV )
by MCART_1:10, MCART_1:23;
reconsider x1 =
x `1 ,
x2 =
x `2 ,
y1 =
y `1 ,
y2 =
y `2 as
Element of
AFV by A8, MCART_1:10;
reconsider x1' =
x1,
x2' =
x2,
y1' =
y1,
y2' =
y2 as
Element of
(GroupVect AFV,o) ;
A10:
x1,
x2 // y1,
y2
by A7, A9, ANALOAF:def 2;
x1' # y2' = x2' # y1'
proof
reconsider z1 =
x1' # y2',
z2 =
x2' # y1' as
Element of
AFV ;
A11:
(
z1 = Padd o,
x1,
y2 &
z2 = Padd o,
x2,
y1 )
by Def7;
then
(
o,
x1 // y2,
z1 &
o,
x2 // y1,
z2 )
by Def5;
then
(
x1,
o // z1,
y2 &
o,
x2 // y1,
z2 )
by Th8;
then
o,
x2 // y1,
z1
by A10, Th13;
hence
x1' # y2' = x2' # y1'
by A11, Def5;
:: thesis: verum
end; hence
[x,y] in CONGRD (GroupVect AFV,o)
by A9, TDGROUP:def 4;
:: thesis: verum end; hence
(
[x,y] in CONGRD (GroupVect AFV,o) iff
[x,y] in the
CONGR of
AFV )
by A2;
:: thesis: verum end;
hence
CONGRD (GroupVect AFV,o) = the
CONGR of
AFV
by RELAT_1:def 2;
:: thesis: verum
end;
hence
AFV = AV (GroupVect AFV,o)
by A1, TDGROUP:9; :: thesis: verum