This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cycsubmcl

Description: The set of nonnegative integer powers of an element A contains A . Although this theorem holds for any class G , the definition of F is only meaningful if G is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023)

Ref Expression
Hypotheses cycsubm.b 
|- B = ( Base ` G )
cycsubm.t 
|- .x. = ( .g ` G )
cycsubm.f 
|- F = ( x e. NN0 |-> ( x .x. A ) )
cycsubm.c 
|- C = ran F
Assertion cycsubmcl 
|- ( A e. B -> A e. C )

Proof

Step Hyp Ref Expression
1 cycsubm.b 
 |-  B = ( Base ` G )
2 cycsubm.t 
 |-  .x. = ( .g ` G )
3 cycsubm.f 
 |-  F = ( x e. NN0 |-> ( x .x. A ) )
4 cycsubm.c 
 |-  C = ran F
5 1nn0 
 |-  1 e. NN0
6 5 a1i 
 |-  ( A e. B -> 1 e. NN0 )
7 oveq1 
 |-  ( i = 1 -> ( i .x. A ) = ( 1 .x. A ) )
8 7 eqeq2d 
 |-  ( i = 1 -> ( A = ( i .x. A ) <-> A = ( 1 .x. A ) ) )
9 8 adantl 
 |-  ( ( A e. B /\ i = 1 ) -> ( A = ( i .x. A ) <-> A = ( 1 .x. A ) ) )
10 1 2 mulg1 
 |-  ( A e. B -> ( 1 .x. A ) = A )
11 10 eqcomd 
 |-  ( A e. B -> A = ( 1 .x. A ) )
12 6 9 11 rspcedvd 
 |-  ( A e. B -> E. i e. NN0 A = ( i .x. A ) )
13 1 2 3 4 cycsubmel 
 |-  ( A e. C <-> E. i e. NN0 A = ( i .x. A ) )
14 12 13 sylibr 
 |-  ( A e. B -> A e. C )