Shorten this lemma!

[igblan]

I have

h1::iscycgi.1 |- G e. Grp
h2::iscycgi.2 |- X = ran G
h3::iscycgi.3 |- U = ( Id ` G )
h4::iscycgi.4 |- N e. NN
h5::iscycgi.5 |- F : ( 0 ... ( N - 1 ) ) -1-1-onto-> X
h6::iscycgi.6 |- ( n e. ( 1 ... ( N - 1 ) ) -> ( F ` n ) = ( ( F
` 1 ) G ( F ` ( n - 1 ) ) ) )
...
128:127,123:ax-mp |- ( F ` 0 ) = U

128 steps seems excessive.

The proof has to be broken into 2 parts: 1 < N and 1 = N. The former
relies on the last hyp, while the latter uses the fact that the only
element in a group of order 1 is the identity element.

I don't use grpsn.

Anyone want to try to do better?

Cheers, Paul

[Jeff Hoffman]

Yes, I'd like to try. My metamath chops are probably rustier than
yours, so I doubt I can trim your approach. Perhaps a different
approach will yield a shorter proof. What were the key steps in your
128? Was f1fveq one of them? My thinking is:
1-1 => n e (2...N-1) -> F(n-1) != U
onto => F(n-1)=U -> n e. (1...N-1)
=> F(1-1)=U

Another idea is to define a one variable function G1 s.t F(n) = G1(F
(n-1)), but I'm not sure what to do with a generalized suc(). Most of
the metamath definitions for < are customized for the domain and the
juicy ordering properties we want are for ordinals. It's always bugged
me how many NN properties are re-derived instead of using some isom
with ordinals.

As you can see, I often get sidetracked. So much interesting stuff
out there. I'd like to hear your expertise on what's probably useful
here.

Thanks,
Jeff