let p be Nat; :: thesis: for G being finite Group

for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

let G be finite Group; :: thesis: for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

let x, d be Element of G; :: thesis: ( ord d = p & p is prime & x in gr {d} & not x = 1_ G implies gr {x} = gr {d} )

assume A1: ( ord d = p & p is prime ) ; :: thesis: ( not x in gr {d} or x = 1_ G or gr {x} = gr {d} )

assume x in gr {d} ; :: thesis: ( x = 1_ G or gr {x} = gr {d} )

then X1: gr {x} is strict Subgroup of gr {d} by GRCY212;

X2: card (gr {d}) = p by A1, GR_CY_1:7;

( gr {x} = (1). (gr {d}) implies x = 1_ G )

for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

let G be finite Group; :: thesis: for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds

gr {x} = gr {d}

let x, d be Element of G; :: thesis: ( ord d = p & p is prime & x in gr {d} & not x = 1_ G implies gr {x} = gr {d} )

assume A1: ( ord d = p & p is prime ) ; :: thesis: ( not x in gr {d} or x = 1_ G or gr {x} = gr {d} )

assume x in gr {d} ; :: thesis: ( x = 1_ G or gr {x} = gr {d} )

then X1: gr {x} is strict Subgroup of gr {d} by GRCY212;

X2: card (gr {d}) = p by A1, GR_CY_1:7;

( gr {x} = (1). (gr {d}) implies x = 1_ G )

proof

hence
( x = 1_ G or gr {x} = gr {d} )
by GR_CY_1:12, A1, X1, X2; :: thesis: verum
assume X3:
gr {x} = (1). (gr {d})
; :: thesis: x = 1_ G

x in the carrier of (gr {x}) by GR_CY_2:2, STRUCT_0:def 5;

then x in {(1_ (gr {d}))} by X3, GROUP_2:def 7;

then x = 1_ (gr {d}) by TARSKI:def 1;

hence x = 1_ G by GROUP_2:44; :: thesis: verum

end;x in the carrier of (gr {x}) by GR_CY_2:2, STRUCT_0:def 5;

then x in {(1_ (gr {d}))} by X3, GROUP_2:def 7;

then x = 1_ (gr {d}) by TARSKI:def 1;

hence x = 1_ G by GROUP_2:44; :: thesis: verum