set F = multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #);
P1:
for h being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds
( h * (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) = h & (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) * h = h & ex g being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) st
( h * g = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) & g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ) )
proof
let h be
Element of
multMagma(#
(EC_SetAffCo (z,p)),
(addell_AffCo (z,p)) #);
( h * (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) = h & (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) * h = h & ex g being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) st
( h * g = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) & g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ) )
thus
(
h * (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) = h &
(1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) * h = h )
by GROUP_1:def 4;
ex g being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) st
( h * g = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) & g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) )
reconsider h1 =
h as
Element of
EC_SetAffCo (
z,
p) ;
reconsider g1 =
(compell_AffCo (z,p)) . h1 as
Element of
EC_SetAffCo (
z,
p) ;
reconsider g =
g1 as
Element of
multMagma(#
(EC_SetAffCo (z,p)),
(addell_AffCo (z,p)) #) ;
set O =
[0,1,0];
reconsider O =
[0,1,0] as
Element of
multMagma(#
(EC_SetAffCo (z,p)),
(addell_AffCo (z,p)) #)
by ThAffCoZero;
take
g
;
( h * g = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) & g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) )
thus h * g =
0_EC (
z,
p)
by ThAddCompAffCo
.=
1_ multMagma(#
(EC_SetAffCo (z,p)),
(addell_AffCo (z,p)) #)
by GP0
;
g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)
thus g * h =
(addell_AffCo (z,p)) . (
h1,
g1)
by ThCommutativeAffCo
.=
0_EC (
z,
p)
by ThAddCompAffCo
.=
1_ multMagma(#
(EC_SetAffCo (z,p)),
(addell_AffCo (z,p)) #)
by GP0
;
verum
end;
for x, y being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds x * y = y * x
by BINOP_1:def 2;
hence
( multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is commutative & multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is Group-like & not multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is empty )
by P1, GROUP_1:def 2, GROUP_1:def 12; verum