let p be Prime; ( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )
set Zp = multMagma(# (Segm0 p),(multint0 p) #);
A1:
not 1 in {0}
by TARSKI:def 1;
A2:
1 < p
by INT_2:def 4;
then
1 in Segm p
by NAT_1:44;
then
1 in (Segm p) \ {0}
by A1, XBOOLE_0:def 5;
then
1 in Segm0 p
by A2, Def2;
then reconsider e = 1. (INT.Ring p) as Element of multMagma(# (Segm0 p),(multint0 p) #) by A2, INT_3:14;
A3:
multMagma(# (Segm0 p),(multint0 p) #) is associative
A5:
now for h being Element of multMagma(# (Segm0 p),(multint0 p) #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )let h be
Element of
multMagma(#
(Segm0 p),
(multint0 p) #);
( h * e = h & e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )
h in Segm0 p
;
then A6:
h in (Segm p) \ {0}
by A2, Def2;
then reconsider hp =
h as
Element of
(INT.Ring p) by XBOOLE_0:def 5;
thus h * e =
hp * (1_ (INT.Ring p))
by Lm12
.=
h
;
( e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )thus e * h =
(1_ (INT.Ring p)) * hp
by Lm12
.=
h
;
ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e )
not
h in {0}
by A6, XBOOLE_0:def 5;
then A7:
hp <> 0
by TARSKI:def 1;
0 in Segm p
by NAT_1:44;
then
hp <> 0. (INT.Ring p)
by A7, SUBSET_1:def 8;
then consider hpd being
Element of
(INT.Ring p) such that A8:
hpd * hp = 1. (INT.Ring p)
by VECTSP_1:def 9;
hpd <> 0. (INT.Ring p)
by A8;
then
hpd <> 0
;
then
not
hpd in {0}
by TARSKI:def 1;
then
hpd in (Segm p) \ {0}
by XBOOLE_0:def 5;
then reconsider g =
hpd as
Element of
multMagma(#
(Segm0 p),
(multint0 p) #)
by A2, Def2;
A9:
g * h = e
by A8, Lm12;
h * g = e
by A8, Lm12;
hence
ex
g being
Element of
multMagma(#
(Segm0 p),
(multint0 p) #) st
(
h * g = e &
g * h = e )
by A9;
verum end;
multMagma(# (Segm0 p),(multint0 p) #) is commutative
hence
( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )
by A5, A3; verum